They also ease the communication of your programs to others, such as the instructor and assistants who grade them.

All exercise solutions, whether for an assignment or an exam, are expected to be specified, as described below.

Specifications

(* functionIdentifier argument
   TYPE: argumentType -> resultType
   PRE:  ... pre-condition on the argument ...
   POST: ... post-condition on the result ...
   SIDE EFFECTS: ... if any, including exceptions ...
   EXAMPLES: ... especially if useful to highlight delicate issues;
             also include counter-examples ...
*)

The names of the components of the argument need not be consistent between the specification and the program.

Under PRE, note that the pre-condition should also apply to recursive calls. For example, the accumulator of a help function (as sumListAux below) may be equal to the empty list in the first call, but in future calls it is not.

Under PRE and POST, there is no need to repeat the types of the argument and result, as they are already indicated under TYPE.

Under POST, it is sufficient to give the returned expression e, so that the actual post-condition implicitly is "the returned expression is equal to e". Under this convention, writing "this function returns e" is also unnecessarily long.

A function specification can only be useful if all its argument components appear in the post-condition or side effects.

Every value in an abstract datatype or module shall be commented with its specification, as follows:

(* valueIdentifier
   TYPE:  type
   VALUE: ... description of the provided value ...
*)

Specifications are usually written independently of the programming language, to the extent possible. A suitable combination of natural language and rather standard mathematical notation is usually best. Hence write 0 instead of 0.0, prefer ≠ over <>, use · rather than ∗ for multiplications, etc, to the extent possible.

Identifiers

Examples:

   maxValue
   endOfTheGame

Recursive Functions

(* VARIANT: ... *)

Like the pre- and post-conditions, the variant must refer to the parameter names in the specification, but not to the possibly different parameter names in the program. Note that the variant is not part of the specification, but rather part of the verification outline of why the program is believed correct. For a given specification, many programs can be written, and the recursive ones usually have different variants.

Representation Conventions and Invariants

(* REPRESENTATION CONVENTION:
   ... description of how the modelled objects are represented by
   values of the type ...

   REPRESENTATION INVARIANT:
   ... property, if any, that must always hold (as an implicit
   pre-condition and post-condition) ...  *) 

Examples

(* fact n
   TYPE: int -> int
   PRE:  n ≥ 0
   POST: the factorial of n
   EXAMPLES: fact 0 = 1
             fact 3 = 6
*)
(* VARIANT: n *)

fun fact 0 = 1
  | fact n = n * fact (n-1)

(* select n L
   TYPE: int -> int list -> int list
   PRE:  (none)
   POST: the list of the elements in L that are larger than n,
         in the same order as they occur in L
   EXAMPLES: select 2 [1,3,2,4,3] = [3,4,3]
             select 3 [1,3,1]     = []
             select 0 []          = []
*)
(* VARIANT: the length of L *)

fun select _ [] = []
  | select n (x::L) =
    let
      val L' = select n L
    in
      if x>n then x::L' else L'
    end

(* sumList l
   TYPE: int list -> int
   PRE:  (none)
   POST: sum of the elements of l
   EXAMPLES: sumList [1,2,3] = 6
   
   sumListAux (l, acc)
   TYPE: (int list * int) -> int
   PRE:  (none)
   POST: acc + sum of elements of l
   EXAMPLES: sumListAux([1,2,3], 4) = 10

   VARIANT: The length of l
*)


fun sumList l =
    let fun sumListAux ([], acc) = acc
	  | sumListAux (x::l, acc) = sumListAux (l, acc+x)
    in
	sumListAux (l, 0)
    end

abstype 'b bsTree = Void
                  | Bst of (int * 'b) * 'b bsTree * 'b bsTree
(* REPRESENTATION CONVENTION:
   a binary search tree with key-value pair (k,s) in the root,
   left subtree L, and right subtree R is represented by Bst((k,s),L,R)
   REPRESENTATION INVARIANT:
   for Bst((k,s),L,R):
    - every element of L has a key smaller than k
    - every element of R has a key  larger than k
*)
with
  (* emptyBsTree
     TYPE:  'b bsTree
     VALUE: the empty binary search tree
  *)
  val emptyBsTree = Void
  ...
  (* exists k T
     TYPE: int -> 'b bsTree -> bool
     PRE:  (none)
     POST: true if T contains a node with key k, and false otherwise
  *)
  (* VARIANT: the number of nodes of T *)
  fun exists k Void = false
    | exists k (Bst((key,s),L,R)) =
      if k = key then
	  true
      else
	  if k < key then
	      exists k L
	  else
	      exists k R
  ...
end