Consider the following problem:

Given integers `a` and `b`, compute the sum `a+(a+1)+...+b`.

This function is easy to implement:

fun sum a b = if a > b then 0 else a + sum (a+1) b

The post-condition is simply

`POST: a+(a+1)+...+b`

What about the pre-condition? It might be tempting to rule out the
case when `a>b` and write

PRE: a <= b

but note that the function `sum` is defined for all integers `a` and
`b`. Further, the expression `a+(a+1)+...+b` has a well-defined meaning
even when `a>b` (the sum of an empty sequence is zero).

The variant may not be completely obvious, but is simply `b-a`. It is
easy to verify that the variant decreases at each recursive call and
that there is no recursive call where the variant is less than `-1`.

The complete specification becomes

sum a b TYPE: int -> int -> int PRE: none POST: a+(a+1)+...+b Examples: sum 1 4 = 10; sum 100 0 = 0; Variant: b-a

Suppose now thar we instead choose to implement the function using a
*tail-recursive* help function:

fun sumAux a b acc = if a > b then acc else sumAux (a+1) b (a+acc) fun sum a b = sumAux a b 0;

The specification of `sum` is unchanged (but it no longer needs a
variant, since its implementation is not recursive).

The help function will always be called with `acc=0`, but
in the recursive calls `acc` will have a different value, so it is **NOT**
acceptable to make any assumptions about the value of `acc`. The
specification of `sumAux` should be such that the intended behaviour of
every call (even recursive ones) is captured.

For example:

sum 1 3 -> sumAux 1 3 0 -> sumAux 2 3 1 -> sumAux 3 3 3 -> sumAux 4 3 6 -> 6

So `sumAux 1 3 0 = sumAux 2 3 1 = sumAux 3 3 3 = sumAux 4 3 6 = 6`.
The specification of `sumAux` should reflect this.

Note that `acc` may take virtually any value, so there is no reason to
restrict `acc` in the pre-condition.

The post-condition of `sumAux` should be something like:

`acc + a+(a+1)+...+b`,

i.e., the sum of the values from `a` to `b`, plus `acc`.

The reader is encouraged to check that the calls to `sumAux` listed
above all evaluate to the value given in the post-condition.

sumAux a b acc TYPE: int -> int -> int -> int PRE: none POST: acc + a+(a+1)+...+b Examples: sumAux 1 4 0 = 10; sumAux 100 0 12345 = 12345; sumAux 1 3 0 = sumAux 2 3 1 = sumAux 3 3 3 = sumAux 4 3 6 = 6 Variant: b-a

Assignment 1 defines what it means for a string to be "balanced", and lists the set of left parentheses and right parentheses.

When writing function specifications you can of course assume concepts defined in the assignment, so there is no need to specify (for example) what it means for a string to be balanced.