This is an old revision of the document!
Lecture 3 (Skeleton)
Context
Recall that we can
- represent programs using guarded command language, e.g. desugaring of 'if' into non-deterministic choice and assume
- give meaning to guarded command language statements as relations
- we can represent relations using set comprehensions; if our program r has two state components, we can represent its meaning R® as
where F is some formula that has x,y,x_0,y_0 as free variables.
Our goal is to find rules for computing R® that are
- correct
- efficient
- create formulas that we can prove later
Formulas for basic statements
In our simple language, basic statements are assignment, havoc, assume, assert.
R(x=t) = (x=t & y=y_0 & error=error_0)
Note: all our statements will have the property that if error_0 = true, then error=true. That is, you can never recover from an error state. This is convenient: if we prove no errors at the end, then there were never errors in between.
Note: the condition y=y_0 & error=error_0 is called <b>frame condition</b>. There are as many conjuncts as there are components of the state. This can be annoying to write, so let us use shorthand frame(x) for it. The shorthand frame(x) denotes a conjunction of v=v_0 for all v that are distinct from x (in this case y and error). We can have zero or more variables as arguments of frame, so frame() means that nothing changes.
R(havoc x) = frame(x) R(assume F) = F[x:=x_0, y:=y_0, error:=error_0] R(assert F) = (F → frame)
Note:
x=t is same as havoc(x);assume(x=t)
assert false = crash (stops with error)
assume true = skip (does nothing)
Papers
- Verification condition generation in Spec#: http://research.microsoft.com/~leino/papers/krml157.pdf
- Loop invariant inference for set algebra formulas: hob-tcs.pdf
- Induction-iteration method for machine code checking: http://www.cs.wisc.edu/wpis/papers/pldi00.ps
- Presburger Arithmetic (PA) bounds: papadimitriou81complexityintegerprogramming.pdf
- Specializing PA bounds: http://www.lmcs-online.org/ojs/viewarticle.php?id=43&layout=abstract