Copenhagen Programming Language Seminar
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.
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 firstname.lastname@example.org with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org