Showing 1–4 of 4 results for author: van der Zwaag, M B

Mechanistic Behavior of Single-Pass Instruction Sequences

Authors: Jan A. Bergstra, Mark B. van der Zwaag

Abstract: Earlier work on program and thread algebra detailed the functional, observable behavior of programs under execution. In this article we add the modeling of unobservable, mechanistic processing, in particular processing due to jump instructions. We model mechanistic processing preceding some further behavior as a delay of that behavior; we borrow a unary delay operator from discrete time process… ▽ More Earlier work on program and thread algebra detailed the functional, observable behavior of programs under execution. In this article we add the modeling of unobservable, mechanistic processing, in particular processing due to jump instructions. We model mechanistic processing preceding some further behavior as a delay of that behavior; we borrow a unary delay operator from discrete time process algebra. We define a mechanistic improvement ordering on threads and observe that some threads do not have an optimal implementation. △ Less

Submitted 26 September, 2008; originally announced September 2008.

Comments: 12 pages

ACM Class: D.1.4; F.3.2; F.3.3

Tuplix Calculus Specifications of Financial Transfer Networks

Authors: J. A. Bergstra, S. Nolst Trenite, M. B. van der Zwaag

Abstract: We study the application of Tuplix Calculus in modular financial budget design. We formalize organizational structure using financial transfer networks. We consider the notion of flux of money over a network, and a way to enforce the matching of influx and outflux for parts of a network. We exploit so-called signed attribute notation to make internal streams visible through encapsulations. Final… ▽ More We study the application of Tuplix Calculus in modular financial budget design. We formalize organizational structure using financial transfer networks. We consider the notion of flux of money over a network, and a way to enforce the matching of influx and outflux for parts of a network. We exploit so-called signed attribute notation to make internal streams visible through encapsulations. Finally, we propose a Tuplix Calculus construct for the definition of data functions. △ Less

Submitted 13 May, 2008; originally announced May 2008.

Report number: PRG0807

Towards a formalization of budgets

Authors: Jan A. Bergstra, Sanne Nolst Trenité, Mark B. van der Zwaag

Abstract: We go into the need for, and the requirements on, a formal theory of budgets. We present a simple algebraic theory of rational budgets, i.e., budgets in which amounts of money are specified by functions on the rational numbers. This theory is based on the tuplix calculus. We go into the importance of using totalized models for the rational numbers. We present a case study on the educational budg… ▽ More We go into the need for, and the requirements on, a formal theory of budgets. We present a simple algebraic theory of rational budgets, i.e., budgets in which amounts of money are specified by functions on the rational numbers. This theory is based on the tuplix calculus. We go into the importance of using totalized models for the rational numbers. We present a case study on the educational budget of a university department offering master programs. △ Less

Submitted 25 February, 2008; originally announced February 2008.

Report number: PRG0712

Tuplix Calculus

Authors: J. A. Bergstra, A. Ponse, M. B. van der Zwaag

Abstract: We introduce a calculus for tuplices, which are expressions that generalize matrices and vectors. Tuplices have an underlying data type for quantities that are taken from a zero-totalized field. We start with the core tuplix calculus CTC for entries and tests, which are combined using conjunctive composition. We define a standard model and prove that CTC is relatively complete with respect to it… ▽ More We introduce a calculus for tuplices, which are expressions that generalize matrices and vectors. Tuplices have an underlying data type for quantities that are taken from a zero-totalized field. We start with the core tuplix calculus CTC for entries and tests, which are combined using conjunctive composition. We define a standard model and prove that CTC is relatively complete with respect to it. The core calculus is extended with operators for choice, information hiding, scalar multiplication, clearing and encapsulation. We provide two examples of applications; one on incremental financial budgeting, and one on modular financial budget design. △ Less

Submitted 20 December, 2007; originally announced December 2007.

Comments: 22 pages

Report number: PRG0713

Journal ref: Scientific Annals of Computer Science, 18:35--61, 2008