(* functionIdentifier argument : argumentType -> resultType PRE: ... pre-condition on the argument ... POST: ... post-condition on the result ... SIDE-EFFECTS: ... if any ... EXAMPLES: ... if useful ... *)where the function identifier is unnecessary for anonymous functions.
Everything should preferably be in English, as practice for the exam, though standard mathematical notations are of course also allowed.
Note that a specification cannot possibly be useful if at least one of its argument components does not appear in the post-condition.
An exercise solution, whether for an assignment or an exam, where at least one function is not specified with the content (not necessarily the format) indicated above shall get a fail grade, and this without us actually looking at the program itself, even if it is totally correct (with respect to the missing specification)!
Every identifier shall begin with a lowercase letter. If there are several words in an identifier, then glue them together without using the underscore character (`_'), and start each new word with an uppercase letter.
(* INDUCTION PARAMETER: ... WELL-FOUNDED RELATION: ... *)
An exercise solution, whether for an assignment or an exam, where at least one recursive function is not commented with the content (not necessarily the format) indicated above shall get a fail grade, and this without us actually looking at the program itself, even if it is totally correct!
... if booleanExpression then expression1 else expression2 ...
Lay out and indent let declarations as follows:
... let declaration1 ... declarationM in expression end ...
Lay out and indent local declarations as follows:
... local declaration11 ... declaration1M in declaration21 ... declaration2N end ...
All indentations must be contextual, that is vertically aligned with the previous and following parts of the program, which are indicated by `...' above.
(* myMax (a,b) : int * int -> int PRE: (none) POST: the largest value among a and b SIDE-EFFECTS: (none) EXAMPLES: myMax ( 2, 5) = 5 myMax (~2,~5) = ~2 *) fun myMax (a,b) = if a > b then a else b
(* fact n : int -> int PRE: n >= 0 POST: the factorial of n SIDE-EFFECTS: (none) EXAMPLES: fact 0 = 1 fact 3 = 6 INDUCTION PARAMETER: n WELL-FOUNDED RELATION: < *) fun fact 0 = 1 | fact n = n * fact (n-1)