# Flowcharts and Transition Graphs

## General

For each of the 3 flowcharts below you are required to:

- Transform the flowchart into a transition graph.
- Choose a set of cutpoints.
- Identify the resulting set of verification paths.
- Define the "summary guarded command" for each verification path.
- Define an assertion (invariant) for each of the cutpoints.
- Prove partial correctness with respect to the specification.

## I. Factorial

Specification:

- Phi(x) : x >= 0
- Psi(x,z): z = x!

All program variables are over the integers.

## II. Is prime

Specification:

- Phi(x) : x >= 2
- Psi(x,z): z =
*true* if x is prime number; z =* false*
otherwise.

All program variables are over the integers.

## III. Minimum of an array

X is a given array of real numbers: X[1], X[2], ... X[n+1], n>=0.

Specification:

- Phi(n,X) : n >=0
- Psi(n,X,z): z = min(X[1], X[2], ... X[n+1]).

## Hand-in and due date

Thursday 20/3/2003
at 11:00 (hand-in in class).