While loops

It can be shown (domain theory) that if the loop terminates, the function has a fixed point. Further, there is a partial order on the fixed points, the one that we want is the least fixed point.

Scopes

The environment models the binding between an identifier and its location (address). The store function maps the location to the value it contains.

Axiomatic Semantics

Describe programming language semantics in a way that can be used by programmers to develop correct programs. Denotational semantics is mainly of interest to program language designers.

  • java -ea -esa myprog enables your assertions and system assertions

Hoare triple:

{precondition} program {postcondition}