This is an old revision of the document!
Homework 02
Deadlines:
- 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 1
Using definitions of Hoare triple, sp, wp in Hoare logic, prove the following:
- the law on the postcondition of inverse versus wp
- the equivalence of the Three Forms of Hoare Triple.
Problem 2
We call relation functional if
, if
and
then
. For each of the following statements either give a counterexample or prove it:
- for any
,
- if
is functional,
- for any
,
- if
is functional,
- for any
,
- if
is functional,
Problem 3
Write an interpreter for our simple programming language with the additional ability to state assume statements, assert statements, and loop invariants. The meaning of assignments and control structures is the same as in the usual programming language. For assume and assert statements, the interpreter should just check whether they are true in the current program state and emit a warning if they are not.
Use Scala integers to represent the unbounded integers in the language.
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.
sealed abstract class Term case class Constant(val c: Int) extends Term case class Variable(val v: String) extends Term case class Plus(val t1: Term, val t2: Term) extends Term case class Minus(val t1: Term, val t2: Term) extends Term case class Times(val c: Int, val t: Term) extends Term case class Divide(val t: Term, val c: Int) extends Term case class Modulo(val t: Term, val c: Int) extends Term sealed abstract class BoolExpr case class Equal(val t1: Term, val t2: Term) extends BoolExpr case class LessThan(val t1: Term, val t2: Term) extends BoolExpr case class GreaterThan(val t1: Term, val t2: Term) extends BoolExpr case class Negation(val F: BoolExpr) extends BoolExpr case class And(val f1: BoolExpr, val f2: BoolExpr) extends BoolExpr case class Or(val f1: BoolExpr, val f2: BoolExpr) extends BoolExpr sealed abstract class Command case class Assignment(val v: String, val t: Term) extends Command case class IfThenElse(val cond: BoolExpr, val ifcom: Command, val elsecom: Command) extends Command case class Block(val com1: Command, val com2: Command) extends Command case class WhileLoop( cond: BoolExpr, val com: Command) extends Command
Problem 4
Extend the previous interpreter with elements of symbolic execution. A symbolic execution engine computes the formula that represents the relation associated with the command
. It is similar to an interpreter but works with symbolic state containing two parts:
- mapping from each variable into an expression denoting its value as a function of the initial state, the initial state being denoted by symbolic variables.
- a constraint on the variables
For a program with variables x,y, the initial state of symbolic execution is a map with constraint true:
map: {"x"->Var("x0"), "y"->Var("y0")} constraint: True
After executing assignment
x = x + y
the resulting symbolic state is
map: {"x"->Plus(Var("x0"),Var("y0")), "y"->Var("y0")} constraint: True
If afterwards we execute
y = x + 1
the resulting symbolic state is
map: {"x"->Plus(Var("x0"),Var("y0")), "y"->Plus(Plus(Var("x0"),Var("y0")),Constant(1))} constraint: True
If after this we execute a statement
assume (x > 0)
the resulting symbolic state is
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))
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.