Axiomatic semantics

The axiomatic semantics of computer science describes the importance of programs by inference rules that allow it to close on a desired property of the input to the output properties. The axiomatic semantics is abstracted further than the denotational semantics. There are no concrete memory transformed, but only logical statements about memory, more specifically about values ​​of program variables in them.

This corresponds to the axiomatic semantics of a programming perspective. She seems to be suitable in contrast to the operational semantics for imperative languages ​​.

There are two main styles, the Hoare - calculus and the wp- calculus.