PLP: Lecture 31
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}