Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:homework02 [2008/03/04 15:46] vkuncak |
sav08:homework02 [2008/03/04 16:54] vkuncak |
||
---|---|---|---|
Line 3: | Line 3: | ||
Deadlines: | Deadlines: | ||
* Problem 1 and Problem 2 are due 5 March 2008 at 11:00am | * Problem 1 and Problem 2 are due 5 March 2008 at 11:00am | ||
- | * Problem 3 and Problem 3 are due 6 March 2008 at 08:00am | + | * Problem 3 and Problem 4 are due 6 March 2008 at 08:00am |
===== Problem 1 ===== | ===== Problem 1 ===== | ||
Line 81: | Line 81: | ||
constraint: GreaterThan(Plus(Var("x0"),Var("y0"),Constant(0)) | constraint: GreaterThan(Plus(Var("x0"),Var("y0"),Constant(0)) | ||
- | Write a program that starts from the symbolic state, executes a givn loop-free program (containing sequential composition, if-then-else assume, and assignments), and prints the resulting symbolic state. | + | Write a program that executes a givn loop-free command (containing sequential composition ";", if-then-else, assume, and assignments ":="). The program should start from the initial symbolic state and prints the resulting final symbolic state. Given a command "c" with two variables x,y, if the final symbolic state is |
+ | map: {x->e1, y->e2} | ||
+ | constraint: F | ||
+ | then the relation representing the meaning of $c$ should be given by the relation | ||
+ | \[ | ||
+ | \{("x" \rightarrow x0,"y" \rightarrow y0),("x" \rightarrow x,"y" \rightarrow y)) | x = e1 \land y = e2 \land F \} | ||
+ | \] | ||
+ | The final formula $F$ may or may not use additional existentially quantified variables. | ||
+ | |||
+ | ===== Problem 5 (optional alternative to Problem 4) ===== | ||
+ | |||
+ | 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]]. | ||