Axiomatic semantics

from Wikipedia, the free encyclopedia

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