03 Function Specification

Let's review our template for specifying functions:

(** [f x] is ...
    Example: ...
    Requires: ...
    Raises: ... *)
val f : t -> u

(from Abstraction and Speciication in Program Development, later Program Development in Java: Abstraction, Specification, and Object-Oriented Design by Barbra Liskov and John Guttag)

By the way, Barbara won the 2008 turing award, and was one of the first women to recieve a Ph.D. in Computer Science. She also wrote the programming language CLU.

From her Turing Laureate:

For contributions to practical and theoretical foundations of programming language and system design, especially related to data abstraction, fault tolerance, and distributed computing.

(emphasis added)

Let's go through the List.sort definition specification in the OCaml standard library:

val sort : ('a -> 'a -> int) -> 'a list -> 'a list
(** Sort a list in increasing order according to a comparison
   function.  The comparison function must return 0 if its arguments
   compare as equal, a positive integer if the first is greater,
   and a negative integer if the first is smaller (see Array.sort for
   a complete specification).  For example,
   {!Stdlib.compare} is a suitable comparison function.
   The resulting list is sorted in increasing order.
   [List.sort] is guaranteed to run in constant heap space
   (in addition to the size of the result list) and logarithmic
   stack space.
   The current implementation uses Merge Sort. It runs in constant
   heap space and logarithmic stack space.
*)

(source)

Let's break this definition apart!

• "Sort a list in increasing order according to a comparison function" – one line summary of behavior (not written exactly the same way that we do it in this class, but that's okay! We all generally understand what a sort is)
• "The comparison function must return 0 if its arguments compare as equal, a positive integer if the first is greater, and a negative integer if the first is smaller (see Array.sort for a complete specification)." – Precondition, what the parameter has to do!
• "The resulting list is sorted in increasing order." – Postcondition, what the function promises to do
• "The current implementation uses Merge Sort. It runs in constant heap space and logarithmic stack space." – promise about complexity, also included in the specification here