Let's look at the pieces of our specification
Here's a hypothetical specification for List.hd, which returns the head of a list:
(** [hd lst] is the head of [lst]
Requires: [lst] is non-empty *)
val hd : 'a list -> 'a
The "requires" clause can also be called the "precondition." It's the client's fault if they aren't following these rules. Note, we don't write "[lst] is a list," or something like that, because OCaml is statically typed, you cannot pass something that isn't a list to OCaml.
Asserting the precondition isn't required in 3110, as it is in 1110, 2110, or other introductory programming languages. The training wheels are off. In the theory of program correctness), nothing is guaranteed if the precondition isn't met (if that sounds interesting to you, take CS 4110 - Programming Languages and Logics or CS 4160 - Formal Verification).
Note that it's a fantastic defensive programming technique. Everyone would prefer an exception than the computer bursting into flames. It's a trade off, sometimes, checking a precondition increases the computational complexity. Maybe check only the "cheap" parts.
Here's a hypothetical specification to sort an int list:
(** [sort lst] contains the same
elements as [lst], but sorted
in ascending order *)
val sort : int list -> int list
Here, we know to blame the implementer if something goes wrong
Here's a hypothetical specification to sort an int list:
(** Examples:
- [sort [1;3;2;3]] is [[1;2;3;3]].
- [sort []] is [[]].
*)
val sort : int list -> int list
This is super helpful to other humans! It gives examples of input and output, in case abstract words aren't helping them. This is really helpful at clarifying edge cases, in this example, one with duplications (shows that they're preserved), and one with the empty list (shows that it returns the empty list)
Here's a hypothetical specification for List.hd, which returns the head of a list:
(** [hd lst] is the head of [lst]
Requires: [lst] is non-empty
Raises: [Failure "hd" if [lst]
is empty*)
val hd : 'a list -> 'a
This raises clause makes the exception part of the post condition. It is on the part of the implementer to make sure the exception is raised.