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
sav08:homework02 [2008/03/05 01:50]
david
sav08:homework02 [2015/04/21 17:30] (current)
Line 86: Line 86:
   constraint: F   constraint: F
 then the relation representing the meaning of $c$ should be given by the relation ​ then the relation representing the meaning of $c$ should be given by the relation ​
-\[+\begin{equation*}
     \{("​x"​ \rightarrow x0,"​y"​ \rightarrow y0),​("​x"​ \rightarrow x,"​y"​ \rightarrow y)) | x = e1 \land y = e2 \land F \}     \{("​x"​ \rightarrow x0,"​y"​ \rightarrow y0),​("​x"​ \rightarrow x,"​y"​ \rightarrow y)) | x = e1 \land y = e2 \land F \}
-\]+\end{equation*}
 The final formula $F$ may or may not use additional existentially quantified variables. The final formula $F$ may or may not use additional existentially quantified variables.
  
 ===== Problem 5 (optional alternative to Problem 4) ===== ===== Problem 5 (optional alternative to Problem 4) =====
 +
 +(See also [[homework03]].)
  
 Extend the interpreter of Problem 3 with a verification-condition generator based on symbolic execution. ​ Verification condition generator should produce verification conditions where '​assume'​ becomes an assumption and where '​assert'​ becomes an assertion to be checked. ​ It should emit one verification condition for each '​assert'​. ​ It should also check that all loop invariants are preserved. ​ To prove the verification conditions, your verification-condition generator can feed them into the formDecider.opt prover from the [[:Jahob system]]. Extend the interpreter of Problem 3 with a verification-condition generator based on symbolic execution. ​ Verification condition generator should produce verification conditions where '​assume'​ becomes an assumption and where '​assert'​ becomes an assertion to be checked. ​ It should emit one verification condition for each '​assert'​. ​ It should also check that all loop invariants are preserved. ​ To prove the verification conditions, your verification-condition generator can feed them into the formDecider.opt prover from the [[:Jahob system]].