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.