LARA

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

\{((x_0,y_0),(x,y)) \mid F \} 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