Axiomatic semantics
The axiomatic semantics of computer science describes the meaning of programs by means of inference rules that allow conclusions to be drawn from a desired property of the input to properties of the output. The axiomatic semantics abstracts further than the denotational semantics . No concrete memories are transformed, only logical statements about memories, more precisely about values of program variables in them.
The axiomatic semantics correspond to the view of the programmer. In contrast to operational semantics, it only seems to be suitable for imperative languages .
There are two main forms, the Hoare calculus and the wp calculus .
literature
- Hanne Riis Nielson, Flemming Nielson: Semantics With Applications - A Formal Introduction. John Wiley & Sons 1992