(*
 * This example illustrates the definition of an auxiliary function that sums
 * the elements of a list.  Such a function can be used in a postcondition that
 * specifies that the output of an operation is based on the sum of elements in
 * a list structure.
 *
 * The recursive definition of the SumList function uses the following
 * strategy:
 *
 *     (a) If the list contains no elements, then the sum is 0
 *     (b) Otherwise, recursively compute the sum of the first list element
 *         with the sum of the rest of the elements
 *
 * The "rest of" a list is denoted by the expression
 *
 *     l[2..#l]
 *
 * The expression between the square brackets denotes a sublist of the form
 *
 *     start..end
 *
 * where 'start' and 'end' are the index positions of the sublist.  The '#'
 * operator is list length.  Hence, the sublist [2..#l] extends from the second
 * position of the list to the last position.  I.e., it's the "rest of" a list
 * beyond position 1.
 *
 *)

function SumList(l:integer*) =
    if (#l = 0) then 0
--  else if (#l = 1) then l[1]		-- This line gets rid of the 
					-- "2 is out of bounds" error message.
					-- See LOG entires of 8apr09 regarding
					-- the possibility a "silent failure"
					-- version of the [2..#l] cdr idiom
    else l[1] + SumList(l[2..#l]);

(*
 * This is an error-free imlementation of cdr, for what it's worth.
 *)
function tail(l:integer*) =
    if (#l = 0) or (#l = 1) then nil
    else l[2..#l];