×

zbMATH — the first resource for mathematics

Side effects and aliasing can have simple axiomatic descriptions. (English) Zbl 0575.68011
We present a different style of axiomatic definition for programming languages. It is oriented toward imperative languages, such as Algol 68, that do not distinguish between statements and expressions. Rather than basing the logic on a notion of pre- or postcondition, we use the value of a programming language expression as the underlying primitive.
A number of language constructs are examined in this framework. We argue that this style of definition gives us a significantly different view of the notion of ”easy axiomatizability”. Side effects in expressions as well as aliasing between variables are shown to be ”easily axiomatizable” in our system.

MSC:
68N01 General topics in the theory of software
Software:
ALGOL 68
PDF BibTeX XML Cite
Full Text: DOI Link