Yao Lirong's Blog

Specifications

CS3110
2020/02/18

From Textbook: Specifications and Abstractions

Specification of Functions

1
2
3
4
5
6
(** [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:

  1. functions not specified in the interface
  2. abstraction function
  3. representation invariant
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
(* 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))
end

note 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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
(** 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. 

1
2
3
4
5
6
7
(** 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

1
2
3
4
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.

Author：Yao Lirong

Link：https://yao-lirong.github.io/blog/2020-02-18-Specifications/

Publish date：February 18th 2020, 12:00:00 am

Update date：June 9th 2022, 3:28:32 am

License：本文采用 Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0) 进行许可

CATALOG
  1. 1. Specification of Functions
  2. 2. Specification of Modules
    1. 2.1. Abstraction Function
    2. 2.2. Representation Invariant
  3. 3. Common Mistakes
    1. 3.1. Long Variable Name
Total : 66
2023
2022
2021
2020
2019
NOI CS2112 Logistics Cornell Review CS3110 Manual Journal Tsinghua Book