LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sav08:homework02 [2008/03/05 01:50]
david
sav08:homework02 [2015/04/21 17:30]
Line 1: Line 1:
-====== Homework 02 ====== 
  
-Deadlines: 
-  * Problem 1 and Problem 2 are due 5 March 2008 at 11:00am 
-  * Problem 3 and Problem 4 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 [[Hoare logic#​postcondition_of_inverse_versus_wp|postcondition of inverse versus wp]] 
-  - the equivalence of the [[Hoare logic#​three_forms_of_hoare_triple|Three Forms of Hoare Triple]]. 
- 
- 
-===== Problem 2 ===== 
- 
-We call relation $r \subseteq S \times S$ functional if $\forall s,s_1,s_2 \in S$, if $(s,s_1) \in r$ and $(s,s_2) \in r$ then $s_1 = s_2$.  For each of the following statements either give a counterexample or prove it: 
-  - for any $r$, $wp(r,S \setminus Q) = S \setminus wp(r,Q)$ 
-  - if $r$ is functional, $wp(r,S \setminus Q) = S \setminus wp(r,Q)$ 
-  - for any $r$, $wp(r,Q) = sp(Q,​r^{-1})$ 
-  - if $r$ is functional, $wp(r,Q) = sp(Q,​r^{-1})$ 
-  - for any $r$, $wp(r,Q_1 \cup Q_2) = wp(r,Q_1) \cup wp(r,Q_2)$ 
-  - if $r$ is functional, $wp(r,Q_1 \cup Q_2) = wp(r,Q_1) \cup wp(r,Q_2)$ 
- 
-===== 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.  There is no need to write a parser for this language, you can start from syntax trees. 
-<​code>​ 
-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 
-</​code>​ 
- 
- 
-===== Problem 4 ===== 
- 
-Extend the previous interpreter with elements of symbolic execution. ​ A symbolic execution engine computes the formula $F_c(c_1)$ that represents the relation associated with the command $c_1$. ​ 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 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]].