Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:homework02 [2008/03/04 17:05] vkuncak |
sav08:homework02 [2008/03/05 01:50] david |
||
|---|---|---|---|
| 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 | ||