Specifications
From Textbook: Specifications and Abstractions
Specification of Functions¶
(** [f x] is ...
Example: ...
Requires: ...
Raises: ...
*)
let f x = - Returns: Don’t write
Returns: ..., instead, just use[f x] is ... - Requires: specific conditions on input
Requires: [x >=0] - Raises: what the program will do if a bad input is given
Raises: xxx Exception if [x<0] - Examples: give an example input and output of the function to better explain what it does
Specification of Modules¶
What to document in a module:
- functions not specified in the interface
- abstraction function
- representation invariant
(* Implementation of sets as lists without duplicates.
* Includes rep_ok checks. *)
module ListSetNoDupsRepOk : Set = struct
(* Abstraction function: the list [a1; ...; an] represents the
* set {a1, ..., an}. [] represents the empty set {}.
*
* Representation invariant: the list contains no duplicates.
*)
type 'a set = 'a list
let rep_ok (l : 'a set) : 'a set =
List.fold_right
(fun x t -> assert (not (List.mem x t)); x :: t)
l []
let empty = []
let mem x l = List.mem x (rep_ok l)
let add x l = rep_ok (if mem x (rep_ok l) then l else x :: l)
let rem x l = rep_ok (List.filter ((<>) x) (rep_ok l))
let size l = List.length (rep_ok l)
let union l1 l2 =
rep_ok (List.fold_left
(fun a x -> if mem x l2 then a else x :: a)
(rep_ok l2) (rep_ok l1))
let inter l1 l2 = rep_ok (List.filter (fun h -> mem h l2) (rep_ok l1))
endnote that the above code keeps representation invariant, abstraction function, and other spec about implementation details inside the module definition, because when we generate the docs of this module, everything outside the definition of the module will be come “public” specs for clients and everything inside will become “private” spec for maintainers.
Abstraction Function¶
Abstraction function maps valid concrete values to abstract values
(** AF: ... *)
module ListSetDups : Set = struct
(* AF: the list [a1; ...; an] represents the
* smallest set containing all the elements a1, ..., an.
* The list may contain duplicates.
* [] represents the empty set.
*)
type 'a set = 'a list
...
module ListSetNoDups : Set = struct
(* AF: the list [a1; ...; an] represents the set
* {a1, ..., an}. [] represents the empty set.
*)
type 'a set = 'a list
...Representation Invariant¶
Representation Invariant distinguishes valid concrete values and from invalid concrete values and is the implicit part of all the precondition and postcondition.
(** RI: ... *)
module ListSetNoDupsRepOk : Set = struct
(* RI: the list contains no duplicates.
*)
type 'a set = 'a list
...Common Mistakes¶
Some common mistakes include not stating enough in preconditions, failing to identify when exceptions will be thrown, failing to specify behavior at boundary cases, writing operational specifications instead of definitional and stating too much in postconditions.
Long Variable Name¶
let number_of_zeros_in_the_list =
fold_left (fun (accumulator:int) (list_element:int) ->
accumulator + (if list_element=0 then 1 else 0)) 0 the_list
in ...Code using such long names is verbose and hard to read. Instead of trying to embed a complete description of a variable in its name, use a short and suggestive name (e.g., zeroes), and if necessary, add a comment at its declaration explaining the purpose of the variable.