LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
Next revision Both sides next revision
sav07_lecture_3_skeleton [2007/03/20 14:42]
vkuncak
sav07_lecture_3_skeleton [2007/03/20 14:48]
vkuncak
Line 22: Line 22:
 In our simple language, basic statements are assignment, havoc, assume, assert. In our simple language, basic statements are assignment, havoc, assume, assert.
  
-R(x=t) = (x=t & y=y_0 & error=error_0)+  ​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**: 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.
Line 28: Line 28:
 **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. **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(havoc x) = frame(x) 
-R(assume F) = F[x:=x_0, y:=y_0, error:​=error_0] +  R(assume F) = F[x:=x_0, y:=y_0, error:​=error_0] 
-R(assert F) = (F -> frame)+  R(assert F) = (F -> frame)
  
 **Note**: **Note**:
  
-x=t  is same as  havoc(x);​assume(x=t)+  ​x=t  is same as  havoc(x);​assume(x=t)
  
-assert false = crash  (stops with error)+  ​assert false = crash  (stops with error)
  
-assume true  = skip   (does nothing)+  ​assume true  = skip   (does nothing)
  
  
Line 48: Line 48:
 Non-deterministic choice is union of relations, that is, disjunction of formulas: Non-deterministic choice is union of relations, that is, disjunction of formulas:
  
-CR(c1 [] c2) = CR(c1) | CR(c2)+  ​CR(c1 [] c2) = CR(c1) | CR(c2)
  
 In sequential composition we follow the rule for composition of relations. ​ We want to get again formula with free variables x_0,​y_0,​x,​y. ​ So we need to do renaming. ​ Let x_1,​y_1,​error_1 be fresh variables. In sequential composition we follow the rule for composition of relations. ​ We want to get again formula with free variables x_0,​y_0,​x,​y. ​ So we need to do renaming. ​ Let x_1,​y_1,​error_1 be fresh variables.
  
-CR(c1 ; c2) = exists x_1,​y_1,​error_1. ​ CR(c1)[x:​=x_1,​y:​=y_1,​error:​=error_1] & CR(c2)[x:​=x_1,​y:​=y_1,​error:​=error_1]+  ​CR(c1 ; c2) = exists x_1,​y_1,​error_1. ​ CR(c1)[x:​=x_1,​y:​=y_1,​error:​=error_1] & CR(c2)[x:​=x_1,​y:​=y_1,​error:​=error_1]
  
-otherwise+The base case is
  
-CR(c)=R(c)     (base case)+  ​CR(c)=R(c)
  
 +when c is a basic command.
  
-==== Accumulation ​of equalities ====+ 
 + 
 +==== Avoiding accumulation ​of equalities ====
  
 This approach generates many variables and many frame conditions.  ​ This approach generates many variables and many frame conditions.  ​
  
-Ignoring error for the moment:+Ignoring error for the moment, we have, for example:
  
   R(x=3) = (x=3 & y=y_0)   R(x=3) = (x=3 & y=y_0)
Line 72: Line 75:
 But if a variable is equal to another, it can be substituted using the substitution rules But if a variable is equal to another, it can be substituted using the substitution rules
  
-(exists x_1. x_1 = t & F(x_1)) ​    <​-> ​   F(t) +  ​(exists x_1. x_1=t & F(x_1)) ​    <​-> ​   F(t) 
-(forall x_1. x_1 = t -> F(x_1) ​    <​-> ​   F(t)+  (forall x_1. x_1=t -> F(x_1) ​    <​-> ​   F(t)
  
 +We can apply these rules to reduce the size of formulas.
  
 ==== Papers ==== ==== Papers ====