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.