# Assignment 2

## 1. Independence on the Cut-Set

Consider program II ("is prime") in assignment 1. After transforming
the flowchart to a transition graph we get 4 nodes, and we need 3 cut-points to
prove partial correctness.

- Add a new cut-point and formulate its assertion using backwards
propagation. Prove partial correctness using the full cut-set.
- Same as above using forward propagation.
- Remove a cut-point (other than the one added) from the full cut-set, and prove partial
correctness.

Your claims can depend on your proven claims from assignment 1 (part II) -
you don't have to copy them. Example: "seeing that verification condition VC_{23}
holds (proved in assignment 1), we get...". Make sure that your references are
**clear and readable**. When in doubt - copy.

## 2. Verifying Success

Consider program III ("min of array") in assignment 1 after
transformed to a transition graph.

- Add safety conditions on every access to array S (ignore access to
X). Conditions should prevent access to an out-of-range index.
Range of S is [1...2n+1].
- Prove that the resulting program is fault-free.

## 3. Finding Inductive Assertions

The following program takes an array X of n+1, n>=0 elements X[0], X[1], ...,
X[n] as input, and output an array Z of n+1 elements Z[0], Z[1], ..., Z[n] where
the elements of Z are the elements of X in reverse order. This means: Z[0] = X[n],
Z[1] = X[n-1], ..., Z[n] = X[0].

Specification:

- Phi(n,X): n >=0
- Psi(n,X,Z): for all k (where 0 =< k =< n), Z[x] = X[n-k].

Transform the flowchart into a transition graph. Use the heuristics studied in class to find the invariants
for the cut-points. For each
invariant specify which heuristics was used. Specify if invariants
obtained using the heuristics were strong enough, or you had to
strengthen them to be able to prove partial correctness.

## Hand-in and due date

Sunday 30/3/2003 (hand-in in my box #108).