Copenhagen Programming Language Seminar

Symbolic continuation for axiomatic semantics

Jørgen Steensgaard-Madsen
Technical University of Denmark

Friday, May 23, 2008, 11:00-12:00
ITU, Rued Langgaards Vej 7, 2300 Copenhagen S. Auditorium 3


Hoare and Dijkstra's pioneering work on axiomatic semantics depends on an identity of mathematical expressions and (side-effect free) program expressions. A notion of symbolic continuations provides means to handle the differences, expand the notion of predicate transformers to expression transformers, and deal with side-effects that arise as assignment to simple variables, including variables that represent a hidden state. I will introduce a notion of indirect semantics and relate it to a standard mathematical construction. An indirect semantics transforms a symbolic continuation to a mathematical expression going backwords in state-transitions compared to program evaluation. An example will illustrate handling of side-effects on a hidden state. The reflection in a mathematical expression of the side-effects viewed in a state prior to introduction of the hidden state characterise a possible role of word models of universal algebra in program verification.

Scientific host: Peter Sestoft. Administrative host: Annette Enggaard. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org