Applications of Summation and Product Operators in the Refinement
Calculus
Applications of Summation and Product Operators in the Refinement
Calculus
Ralph-Johan Back
Michael J. Butler
In 6th
NWPT, pages 96-111
Abstract:
Product and summation operators for predicate transformers were
introduced by Naumann and by Martin using category theoretic considerations.
In this paper, we formalise these operators in the higher order logic
approach to the refinement calculus, look at various algebraic properties of
these operators, and examine several of their applications. We look at how
the product operator provides a model of simultaneous execution of
statements, while the summation operator provides a simple model of late
binding. We also generalise the product operator slightly to form an operator
that corresponds to conjunction of specifications. We show how the product
operator may be used to model extension and modification operators for
programs, and how a combination of the product and summation operators may be
used to model inheritance in an object-oriented programming
language.
Comments
Dept. of Computer Science, Åbo Akademi, Finland.
Available as PostScript,
DVI.
![[BRICS symbol]](http://www.daimi.aau.dk/BRICS/GIF/BRICS/msymbol8mm.GIF)
BRICS WWW home page