Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:homework02 [2008/03/04 16:54] vkuncak |
sav08:homework02 [2015/04/21 17:30] (current) |
||
|---|---|---|---|
| Line 30: | Line 30: | ||
| Your interpreter should take an abstract syntax tree of the program and keep executing the program until it terminates (if it does not terminate, the interpreter should also not terminate). If the program terminates, your interpreter should print the final state of the program. | Your interpreter should take an abstract syntax tree of the program and keep executing the program until it terminates (if it does not terminate, the interpreter should also not terminate). If the program terminates, your interpreter should print the final state of the program. | ||
| - | Here is an example abstract syntax tree that you may wish to use. | + | Here is an example abstract syntax tree that you may wish to use. There is no need to write a parser for this language, you can start from syntax trees. |
| <code> | <code> | ||
| sealed abstract class Term | sealed abstract class Term | ||
| Line 56: | Line 56: | ||
| case class WhileLoop( cond: BoolExpr, val com: Command) extends Command | case class WhileLoop( cond: BoolExpr, val com: Command) extends Command | ||
| </code> | </code> | ||
| + | |||
| ===== Problem 4 ===== | ===== Problem 4 ===== | ||
| Line 79: | Line 80: | ||
| the resulting symbolic state is | the resulting symbolic state is | ||
| map: {"x"->Plus(Var("x0"),Var("y0")), "y"->Plus(Plus(Var("x0"),Var("y0")),Constant(1))} | map: {"x"->Plus(Var("x0"),Var("y0")), "y"->Plus(Plus(Var("x0"),Var("y0")),Constant(1))} | ||
| - | constraint: GreaterThan(Plus(Var("x0"),Var("y0"),Constant(0)) | + | constraint: GreaterThan(Plus(Var("x0"),Var("y0")),Constant(0)) |
| 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 | 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 | ||
| Line 85: | 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) ===== | ||
| - | 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]]. | + | (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]]. | ||