# Refinement Coursework

## Simple Statistics Programs

The minimum of a set of real numbers S is written min(S) and satisfies:

`    ~(S={})  ==>  (min(S) in S) /\ (! x:S. min(S) <=  x)`

Let a be an array of reals:

`      a: ARRAY OF real`

An array ranges from a[0] to a[#a-1], where #a is the size of array a. The elements of such an array is written elems(a) and is defined as follows:

`      elems(a)  =  { x:real | ?i<#a . a[i]=x }`

A procedure which finds the minimum value of such an array may be specified as follows:

```      PROCEDURE Minimum( a : ARRAY OF real;
mn : real)
{ #a > 0 }
mn :=  min(elems(a))
```

Part 1: Use the refinement calculus to refine this specification into a program that doesn't use min or elems. The refined program should have a loop that traverses the array to determine the minimum element. Justify each derivation and sub-derivation by annotating it with the appropriate law. When writing the loop invariant you may find it convenient to use the notion of an array slice:

`        a[0..n]`

represents some initial segment of the array, where n < #a.

Part 2: The maximum of a set of reals is the opposite of minimum:

`    ~(S={})  ==>  (max(S) in S) /\ (! x:S. max(S) >=  x)`

A program that calculates the minimum and maximum of an array of reals may be specified as follows:

```      PROCEDURE MinMax( a : ARRAY OF real;
mn,mx : real;)
{ #a > 0 }
mn, mx :=  mn', mx' |
mn' = min(elems(a))  /\
mx' = max(elems(a))
```

Use the refinement calculus to refine this specification into a program that doesn't use min, max, or elems. The refined program should traverse the array only once to determine both the minimum and the maximum. Justify each derivation and sub-derivation by annotating it with the appropriate law.