They also ease the communication of your programs to others, such as the instructor and assistants who grade them.
Shedding these good habits after this course would be doing yourself a great disservice. A competent programmer can of course do the specification and verification (or verification outline, as in this course) in her brain only, but that will be of no help if she herself reconsiders the program a few weeks later, or if somebody else has to call or modify or verify it. No engineer takes on a well-defined task without a specification.
(* 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 ... *)where the function identifier is unnecessary for anonymous functions. The only exception to the necessity of specifications is for an anonymous function that is passed as an argument to another function: you need not specify it if and only if it is very simple.
The names of the components of the argument need not be consistent between the specification and the program.
Under PRE, be careful not to require any accumulator to be equal to some constant. Indeed, this may be the case at the first call, but any recursive call will almost certainly be for a value different from that constant, and would thus violate such a pre-condition.
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 ... *)
Everything shall be in English. 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.
An exercise solution, whether for an assignment or an exam, where at least one function or value is not specified as above shall get a zero grade, and this without us actually looking at the program itself, even if it is totally correct (with respect to the missing specification)!
Examples:
maxValue endOfTheGame
(* 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. The reason for this is that the variant reflects a decision made before the program was written, according to the design methodology. Also, 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.
An exercise solution, whether for an assignment or an exam, where at least one recursive function is not commented as above shall get a zero grade, and this without us actually looking at the program itself, even if it is totally correct!
(* 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) ... *)
An exercise solution, whether for an assignment or an exam, where at least one (abstract) datatype is not commented as above shall get a zero grade, and this without us actually looking at the program itself, even if it is totally correct!
(* 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
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