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.