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 |