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.