EVOLVING ALGEBRA MODEL OF PROGRAMMING LANGUAGE SEMANTICS

We provide a simple evolving algebra (cf. [5] for relevant definitions) model of the language of while programs, based on an obvious flowchart scheme, similar to models used for C [4] and Occam [2]. A simple operational semantics then associates, to a program, a partial function, mapping environments to runs of the appropriate evolving algebra. Due to compositionality of the semantics, it allows simple, correct and complete interpretations of usual semantic descriptions-SOS, denotational semantics, Hoare logic-by straightforward formalization of their usual intuitive explanations, putting thus the evolving algebra model in the role of primary operational model of the language. The evolving algebra model smoothly generalizes to more complex (and more realistic) situations [4,2,1], where other semantical descriptions become unpractical in view of combinatorial explosion of formalism.