• English only

# Differences

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

 sav08:homework02 [2008/03/05 01:50]david sav08:homework02 [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2008/03/05 16:05 vkuncak 2008/03/05 01:50 david 2008/03/04 17:05 vkuncak 2008/03/04 16:54 vkuncak 2008/03/04 16:54 vkuncak 2008/03/04 16:54 vkuncak 2008/03/04 16:52 vkuncak 2008/03/04 15:59 vkuncak 2008/03/04 15:52 vkuncak 2008/03/04 15:46 vkuncak 2008/03/04 15:42 vkuncak 2008/03/04 15:39 vkuncak 2008/03/04 15:18 vkuncak 2008/03/04 15:17 vkuncak 2008/03/03 10:49 piskac 2008/02/28 08:23 vkuncak 2008/02/28 08:20 vkuncak 2008/02/28 07:55 vkuncak 2008/02/27 18:48 vkuncak created Next revision Previous revision 2008/03/05 16:05 vkuncak 2008/03/05 01:50 david 2008/03/04 17:05 vkuncak 2008/03/04 16:54 vkuncak 2008/03/04 16:54 vkuncak 2008/03/04 16:54 vkuncak 2008/03/04 16:52 vkuncak 2008/03/04 15:59 vkuncak 2008/03/04 15:52 vkuncak 2008/03/04 15:46 vkuncak 2008/03/04 15:42 vkuncak 2008/03/04 15:39 vkuncak 2008/03/04 15:18 vkuncak 2008/03/04 15:17 vkuncak 2008/03/03 10:49 piskac 2008/02/28 08:23 vkuncak 2008/02/28 08:20 vkuncak 2008/02/28 07:55 vkuncak 2008/02/27 18:48 vkuncak created 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]].

sav08/homework02.txt · Last modified: 2015/04/21 17:30 (external edit)

© EPFL 2018 - Legal notice