CS550 Exercises 4 Solution

Exercises 4
Exercise 1 (Weakest Precondition). Recall the definition of weakest precondition: wp(
1. Prove or disprove the following properties:
• wp(r1 ∪ r2,Q) = wp(r1,Q) ∪ wp(r2,Q)
• wp(r1 ∪ r2,Q) = wp(r1,Q) ∩ wp(r2,Q)
• wp(r,Q1 ∩ Q2) = wp(r,Q1) ∩ wp(r,Q2)
• wp(r,Q1 ∪ Q2) = wp(r,Q1) ∪ wp(r,Q2)
For those that are wrong, do any of them hold if r is restricted to
being functional, i.e. if r satisfies
∀x,y1,y2. ((x,y1) ∈ r ∧ (x,y2) ∈ r) → (y1 = y2)
2. Let r ⊆ S × S and Q ⊆ S. Give an expression defining weakest precondition wp(r,Q) using operations of inverse of a relation, ( −1), set difference (), and image of a relation under a set, ( [ ]). Prove that your expression is correct by expanding the definitions of wp as well as of relational and set operations.
Exercise 2 (Programing With Integers). Consider the following program:
1 case class Container(var x: INT, var y: INT):
2 def fun: Unit = {
3 require(x > 0 && y > 0)
4 if x > y then
5 x = x+y 6 y = x−y
7 x = x−y 8 else
9 y = y−x
10 }.ensuring(2∗old(this).x + old(this).y > 2∗x + y &&
11 x >= 0 && y >= 0)
12 end Container
• Compute R(fun) formally, by expressing all intermediate formulas corresponding to subprograms.
• Write the formula expressing the correctness of the ensuring clause. Is the formula valid when INT denotes mathematical integers with their usual operations (type INT = BigInt in Scala)?
• Is the the verification condition formula valid for machine integers,
Z232 = {−231,...,−1,0,1...,231 − 1}
and where operations are intepreted as the usual machine arithmetic (type INT = Int in Scala)?
Exercise 3 (Hoare Logic Proof). Give a complete Hoare logic proof for the following program:
{n >= 0 && d > 0} q = 0 r = n while ( r >= d ) {
q = q + 1 r = r - d
}
{n == q * d + r && 0 <= r < d}
Exercise 4 (Iterating a Relation). Let M = (S,I,r,A) be a transition system and ¯r = {(s,s0) | (s,a,s0) ∈ r}, as usual. Let ∆ = {(x,x) | x ∈ S}.
Let ¯rk denote the usual composition of relation ¯r with itself k times.
Define the sequence of relations rn, for all non-negative integers n, as follows:
• r0 = ∆ ∪ r¯
• rn+1 = rn ◦ rn
A) (2pt) Prove that rn ⊆ rn+1 for every n.
B) (3pt) Prove that for every n and every k where 0 ≤ k ≤ 2n we have r¯k ⊆ rn.
C) (2pt) Suppose that S is finite. Find a bound B as a function of |S| such that
Reach(M) ⊆ rB[I]
Aim to find as small bound as possible.
Exercise 5 (Approximating Relations). Consider a guarded command language whose meanings are binary relations on the set states U.
Let E(a1,...,an) denote an expression built from some atomic relations a1,...,an, as well as diagonal relations
∆P = {(x,x) | x ∈ P}
for various sets P ⊆ U. The expression E is built from these relations using union (to model non-deterministic choice, relation composition (to represent sequential composition) and transitive closure (to represent loops).
Let us call a relation s ⊆ U ×U an effect if it is reflexive (R) and transitive (T).
A) (2pt) Prove that if s is an effect and ai ⊆ s for all 1 ≤ i ≤ n, then
E(a1,...,an) ⊆ s
B) (2pt) Let U = Z2 denote pairs of integers, denoted by integer variables x,y. Let s be a specification relation given by the formula:
s = {((x,y),(x0,y0)) | y ≥ 0 → (x0 ≤ x ∧ y0 ≥ 0)}
Show that s is an effect.