This is an old revision of the document!
Lecture 4 Skeleton
The structure of this lecture is similar to the previous one:
Today, we extend the approach from last lecture (both generating and proving formulas) to support data structures such as references and arrays.
We use weakest preconditions, although you could also use strongest postconditions or any other variants of the conversion from programs to formulas.
More on wp
wp of conjunction and disjunction
- what holds, why, and when
wp of havoc
Can we derive wp(Q,havoc(x)?
- By consider havoc(x) as (… [] x=-1 [] x = 0 [] x = 1 [] …) ?
- From relational definition?
By wp semantics of havoc and assume
wp(Q, havoc(x); assume(x=t)) =
Desugaring loops with loop invariants
while [inv I] (F) c1
⇒
assert(I); havoc(x1,...,xn); (those that can be modified in the loop) assume(I); assume(~F);
Provided that I is inductive. We can check that I is inductive by proving:
assume(I); assume(F); c1; assert(I);
in isolation. Or proving
havoc(x1,...,xn) assume(I); assume(F); c1; assert(I);
at any point. If we combine these two, we get:
⇒
assert(I); havoc(x1,...,xn); assume(I); (assume(~F) [] assume(F); c1; assert I; assume(false));
Benefit: if there is x_{n+1} that is not changed, we do not need to write its properties in the loop invariant. This can make loop invariant shorter.
Modeling data structures
Semantics of global arrays
If then else expressions.
Desugaring if-then-else.
Avoiding exponential explosion using flattening.
Array bounds checking.
Semantics of references
Objects as references, null as an object.
Null checks.
Modeling dynamic allocation of objects
All objects exist.
The allocated object set.
Dynamically allocated arrays
Why we need so many arguments.
Proving formulas with uninterpreted functions
Again, the second part! More technical. But, often you can use these things as a black box.
Congruence closure algorithm
Properties of relations
- equivalence relation
- congruence; example from modular arithmetic
Equality is a congruence with respect to all function symbols.
More information on congruence closure algorithm:
- Gallier, Chapter 10.6
- The paper by Nelson and Oppen