====== Lecture 4 Skeleton ======

The structure of this lecture is similar to the previous one:

{{vcg-big-picture.png?500}}

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.



==== References about weakest precondition (under construction) ====
  * (some online references will come here)
  * Back, Wright: Refinement Calculus
  * Edsger W. Dijkstra: A Discipline of Programming
  * C. A. R. Hoare, He Jifeng: Unifying Theories of Programming


===== 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.

Program with class declaration

<code java>
class Node {
   Node left, right;
}
</code>

How can we represent fields?

Possible mathematical model: fields as functions from objects to objects.

  left : Node => Node
  right : Node => Node

What is the meaning of assignment?

  x.f = y

<latex>
f[x \mapsto y](z) = \left\{ \begin{array}{lr}
y, & z=x   \\
f(z), & z \neq x 
\end{array}\right.
</latex>

left, right - uninterpreted functions (can have any value, depending on the program, unlike arithmetic functions such as +,-,* that have fixed interpretation).

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 Logic Book]], Chapter 10.6
  * {{nelsonoppen80decisionprocedurescongruenceclosure.pdf|the original paper by Nelson and Oppen}}