Code Convention for the PM1 & PK Courses

Specifications

Every function, whether declared globally or locally, whether named or anonymous, whether curried or not, whether commissioned in the homework assignment or invented by you, shall be commented with its specification, say as follows:

(* 
  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)!

Identifiers

Every function identifier shall be descriptive of the performed function.

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.

Examples:

   maxValue
   endOfTheGame

Recursive Functions

Every recursive function shall be commented with the chosen induction parameter and the chosen well-founded relation, say as follows:

(* 
  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!

Indentation

Lay out and indent if-then-else expressions as follows:

   ...
   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.

Examples

(* 
  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)

Condition for Bonus Points

An assignment solution that does not comply with this code convention is not eligible for bonus points!

Prepared by Pierre Flener, with help from Goten Gutgesell
Last modified: 11:05 Thu Oct 24 2001