Rigorous programming

Video lectures

Rigorous specifications (25min)
Formal specifications (11min)
Examples of specifications (14min)
A computer language for formal specifications (13min)

Total 1:03hr.

Rigorous specifications

rigour
/ˈrɪɡə/
noun
    the quality of being extremely thorough and careful

From pre-rigorous to rigorous programming

We write programs and we have an intuitive idea of what they are intended to do. We test them to make sure.

Example. Write a program to reverse a list. Sample solution:

rev :: [a] -> [a]
rev [] = []
rev (x:xs) = rev xs ++ [x]

We may test this and see that rev [1,2,3] evaluates to [3,2,1], and take this as sufficient evidence of the correctness of our implementation of rev.

For this programming task, the pre-rigorous stage is perfectly fine and sufficient. It is easy to understand what is asked, and it is easy to see that the sample solution does do what is asked.

Moreover, for students without training in writing and reading rigorous proofs, such a proof will probably not be very enlightening. It will add little, if anything, to the understanding. It is only for more complex tasks that we need more rigour.

Program specifications

At the rigorous stage, we do proofs as suggested above, and we train students to read and write them. But before doing proofs, we need to understand rigorously what we are going to prove. This is the program specification. We want to give a convincing argument that the program satisfies its specification.

In the pre-rigorous stage, we still need to understand the program specification, which in the above example is the description of the task to be performed: to reverse a list.

If one doesn't know what "to reverse a list" means, an explanation is needed. One may give examples,

rev [] = []
rev [1,2,3] = [3,2,1]

and sometimes this is enough. If we want to be a little bit more precise, we may write the specification as

rev [a₀, a₁, ⋯, aₙ₋₂, aₙ₋₁] = [aₙ₋₁, aₙ₋₂, ⋯, a₁, a₀]

with the convention that when n=0, the expression [a₀, a₁, ⋯, aₙ₋₂, aₙ₋₁] stands for []. (This is a common convention that is often not made explicit.)

If we want to be even more precise, we may say that what is required is that for all i in the range [0 .. length xs - 1], we have that

(rev xs) !! i = xs !! (length xs - 1 - i)

where (!! i) picks the ith element of a list.

We may also give a partial specification, such as e.g.

rev (rev xs) = xs

which says that reversing a list twice gives the original list. This specification is partial (or ambiguous) because there are functions other than rev that satisfy this specification, like the identity function

id xs = xs

Another example of a partial specification is "find an element of a list satisfying a given property". The specification is partial because it doesn't say which element should be returned when there is more than one, or what should be done when there is none (should we use the Maybe type? should we give an error? or what?).

We can use types as parts of a specification, such as

find :: (a -> Bool) -> [a] -> a
find :: (a -> Bool) -> [a] -> Maybe a

Types by themselves, as in this example, also give partial specifications. More examples are

position  :: (a -> Bool) -> [a] -> Int
position  :: (a -> Bool) -> [a] -> Maybe Int
positions :: (a -> Bool) -> [a] -> [Int]

But the type alone is often not enough information of what is required, of course. We may add, e.g.

Given a property of elements of a list, find a position where the element occurs in the list, giving an error if it doesn't occur.
Given a property of elements of a list, find a position where the element occurs in the list, returning -1 if it doesn't occur.
This is probably a bad idea, but, good or bad, it is a specification.
Given a property of elements of a list, find a position where the element occurs, using Maybe to account for the possibility that no element satisfying the property occurs in the list.
Given a property of elements of a list, find the first position where the element occurs, using Maybe to account for the possibility that no element satisfying the property occurs in the list.
Given a property of elements of a list, find the last position where the element occurs, using Maybe account for the possibility that no element satisfying the property occurs in the list.
Given a property of elements of a list, find all positions where the element occurs, and collect them in a list (which will be empty if no element satisfying the property occurs in the given list).

Sometimes the name of a function may act as a partial specification, as in the above examples, but function names are not always wisely chosen and hence are not reliable in general. At best, function names act as reminders of what the functions specifications (to be found elsewhere) are, if the names are wisely chosen.

Example. The Hoogle specifications are usually stated in a pre-rigorous language. They are usually ambiguous, but often by accident rather than by explicit intent. And often they are not clear enough. The Hoogle specifications are still very useful. But often I find myself trying examples to attempt to clarify (seemingly undeliberate) ambiguities that matter for what I want to do.

One reason to give as precise specifications as possible is to avoid unwanted ambiguities. For example, the above two kinds of specifications find and position try to find something, but they are fundamentally different.

A third, also different, but related function is

occurs :: (a -> Bool) -> [a] -> Bool

with the specification that it tells whether or not an element satisfying a given property occurs in a given list

Formal specifications

All the above specifications are in the pre-rigorous stage, getting increasingly more rigorous. The ultimate stage of rigour is formalism, where we use a precisely defined language to write down computer program specifications, and also proofs that these specifications are satisfied.

Such formalisms were invented by mathematical logicians, and include first-order logic, set theory, Martin-Löf type theory, among others.

Computer scientists then implemented some such formal systems so that computers can check not only mathematics but also computer programs for correctness.

Formal specification and proof is an extreme form of rigour, where we not only give the specification in a formal language, but also prove that programs satisfy their intended specifications, with the proofs written also in this language, checked by the computer.

Learning objective of these lecture notes

Here our emphasis will be on specifications rather than proofs. That is, the question we address here is "how do we say rigorously, and even formally, what we intend our programs to do".

We emphasize that mathematics is usually done rigorously but not formally with computer checked proofs, although some people have formalized quite complicated mathematical proofs and checked them with computers.

Similarly, proofs of correctness of computer programs are usually done with paper and pencil (or even just in our heads) rather than formally on a computer, although again people have formally proved with computers the correctness of some tricky algorithms or of large pieces of software, including e.g. programming language compilers (whose correctness is definitely rather important).

Examples of rigorous computer-program specifications

We now discuss the problem of finding elements satisfying a given property in a list in order to illustrate the importance of clear specifications.

occurs    :: (a -> Bool) -> [a] -> Bool
find      :: (a -> Bool) -> [a] -> a
find      :: (a -> Bool) -> [a] -> Maybe a
position  :: (a -> Bool) -> [a] -> Int
position  :: (a -> Bool) -> [a] -> Maybe Int
positions :: (a -> Bool) -> [a] -> [Int]

As discussed above, the types already give an indication of what the functions are intended to do (that is, they give a partial or ambiguous specifications, in the sense discussed above).

Our intended specification for occurs :: (a -> Bool) -> [a] -> Bool is easy to state rigorously:
Given a property p :: a -> Bool and a list xs :: [a], we want that
- occurs p xs = True if and only if there is i :: Int such that
  - 0 ≤ i < length xs and
  - p(xs !! i) = True.
    This requirement says that there is a valid index i for the list xs such that the ith element of xs satisfies the property p. (It doesn't hurt repeating what the specification says in different words.)
Even if this specification is precise, we may still give examples to aid understanding:
- occurs p [] = False for any p.
- occurs even [1,3,5] = False
- occurs even [1,2,3] = True
- occurs odd [1,2,3] = True
Our intended specification of find :: (a -> Bool) -> [a] -> a is almost as easy as that of occurs.
Given a property p :: a -> Bool and a list xs :: [a], we want that
- if there is i :: Int such that 0 ≤ i < length xs and p (xs !! i) = True
- then find p xs is some such element xs !! i of the list xs.
Notice that this is a conditional statement. If the condition is not satisfied, we are allowed to do anything we wish, such as giving an error, or returning any element of the list xs if the list is non-empty, etc.
Specifications are quite often conditional. In this case, the condition is often called the pre-condition. If the pre-condition is not satisfied, we are allowed to do anything we wish (compatible with the required type of the function, if a type is given as part of the specification).
An equivalent specification is the following:
Given a property p :: a -> Bool and a list xs :: [a], we want that
- if there is i :: Int with 0 ≤ i < length xs and p (xs !! i) = True,
- then p (find p xs) = True and also find p xs is an element of the list xs.
Our intended specification of find :: (a -> Bool) -> [a] -> Maybe a is similar.
We want that find p xs = Just x implies that x occurs in the list xs and p x = True.
We also want that find p xs = Nothing implies that there is no x that occurs in the list xs such that p x = True.
Examples:
- find p [] = Nothing for any p.
- find even [1,3,5] = Nothing.
- find even [1,2,3] = Just 2
- find odd [1,2,3] = Just 1
- find odd [1,2,3] = Just 3
The reason the last two equations are possible (although not simultaneously, of course), is that our specification is ambiguous, or partial in the sense discussed above.
When a specification is ambiguous, there may be different implementations satisfying the same specification. One implementation may satisfy find odd [1,2,3] = Just 1 and another implementation may satisfy find odd [1,2,3] = Just 3. But, according to the specification we have given, even if it is ambiguous, any implementation must satisfy the first three equations.
There is nothing intrinsically wrong with ambiguous specifications. Often specifications are deliberately ambiguous. (Like word auto-completion in a text editor. Which auto-completions should we suggest, when there is more than one? We may leave the decision open for the implementation to decide, without invalidating the specification.)
But sometimes specifications are accidentally ambiguous. Not because we wanted to be deliberately ambiguous, but because we were not precise enough in what we tried to say. Or maybe because we forgot to write down something we had in mind.
Just as there may be incorrect programs (that is, programs that don't satisfy the intended specifications), there may be incorrect specifications (we had something in mind, but we didn't express it properly in words).
Our intended specification of position :: (a -> Bool) -> [a] -> Int.
With the above background, we'll be brief this time.
Given a property p :: a -> Bool and a list xs :: [a], we want that
- if there is i :: Int such that 0 ≤ i < length xs and p (xs !! i) = True,
- then position p xs is some such i.
We are not saying what position should do if this condition is not fulfilled. Our specification is (deliberately or accidentally) ambiguous.
Our intended specification of position :: (a -> Bool) -> [a] -> Maybe Int.
Given a property p :: a -> Bool and a list xs :: [a], we want that
- if there is i :: Int such that 0 ≤ i < length xs and p (xs !! i) = True,
- then position p xs = Just i for some such i.
- Otherwise, we intend that position p xs = Nothing.
We are not saying which such i should be returned in the case the pre-condition is fulfilled. Any such i is allowed (the first, the last, or an arbitrary one).
Our intended specification of positions :: (a -> Bool) -> [a] -> [Int].
Given a property p :: a -> Bool and a list xs :: [a], we want that
- If some given i :: Int is in the list positions p xs, then 0 ≤ i < length xs and p (xs !! i) = True.
- If some given i :: Int with 0 ≤ i < length xs satisfies the condition p (xs !! i) = True, then i is in the list positions p xs.
Remark. The list positions xs p will be empty precisely when for all x in the list xs we have p x = False.
I would say that this specification is pre-rigorous or post-rigorous, in the sense that when we read it we understand precisely what "is in the list" means.
If we want to be fully rigorous, we can say:
- For any j :: Int with 0 ≤ j < length (positions p xs) we have that p (xs !! (positions p xs !! j)) = True.
- If some given i :: Int with 0 ≤ i < length xs satisfies the condition p (xs !! i) = True, then there is j with 0 ≤ j < length (positions p xs) such that positions p xs !! j = i.

The language for rigorous specifications

It turns out that a limited logical vocabulary suffices, in practice, to write specifications.

for all, for some, and, or, not, implies, equals.

A computer language for formal specifications and proofs

We will use a notation close to the Agda language for writing such formal specifications.

Formal versions of the above specifications

Specification of occurs :: (a -> Bool) -> [a] -> Bool:

∀ (a : Type) (p : a -> Bool) (xs : List a)

 → occurs p xs ≡ True ⇔ Σ i ꞉ Int , (0 ≤ i)
                                  × (i < length xs)
                                  × (p(xs !! i) ≡ True)

Here ∀ means for all or for any given (universal quantification).
The symbol ≡ stands for mathematical equality.
The symbol ⇔ stands for logical equivalence if and only if.
Σ (sum) plays the role of there exists or for some (existential quantification).
× (cartesian product) plays the role of and (conjunction).

Specification of find :: (a -> Bool) -> [a] -> a

∀ (a : Type) (p : a -> Bool) (xs : List a)

 →  (Σ i ꞉ Int , (0 ≤ i)
               × (i < length xs)
               × (p (xs !! i) ≡ True))

       → (Σ i ꞉ Int , (0 ≤ i)
                    × (i < length xs)
                    × (p (xs !!  i) ≡ True)
                    × (find p xs ≡ xs !! i))

An equivalent specification is the following:

∀ (a : Type) (p : a -> Bool) (xs : List a)

 → (Σ i ꞉ Int , (0 ≤ i)
              × (i < length xs)
              × (p (xs !! i) ≡ True))

     → p (find p xs) ≡ True
     × (Σ i ꞉ Int , (0 ≤ i)
                  × (i < length xs)
                  × find p xs ≡ xs !! i)

Specification of find :: (a -> Bool) -> [a] -> Maybe a.

∀ (a : Type) (p : a -> Bool) (xs : List a)

 → (∀ (x : a) → find p xs ≡ Just x → (p x ≡ True)
                                   × (Σ i ꞉ Int , (0 ≤ i)
                                                × (i < length xs)
                                                × (xs !! i ≡ x)))

× (find p xs ≡ Nothing → ¬(Σ i ꞉ Int ,  (0 ≤ i)
                                     × (i < length xs)
                                     × p(xs !! i) ≡ True))

Here ¬ stands for not (negation).

Specification of position :: (a -> Bool) -> [a] -> Int.

∀ (a : Type) (p : a -> Bool) (xs : List a)

 →  (Σ i ꞉ Int , (0 ≤ i)
               × (i < length xs)
               × (p (xs !! i) ≡ True))

       → (Σ i ꞉ Int ,  (0 ≤ i)
                    × (i < length xs)
                    × (p (xs !! i) ≡ True)
                    × (position p xs ≡ i))

Specification of position :: (a -> Bool) -> [a] -> Maybe Int.
Have a go, based on the above.
Our intended specification of positions :: (a -> Bool) -> [a] -> [Int].
Have a go, based on the above.

The Game of Life

What do "periodic" and "eventually periodic" mean.

Trees

Specifications and correctness proofs of some of the programs we've seen in lectures.

The monad laws

Are here.

Rigorous programming

Video lectures​

Rigorous specifications​

From pre-rigorous to rigorous programming​

Program specifications​

Formal specifications​

Learning objective of these lecture notes​

Examples of rigorous computer-program specifications​

The language for rigorous specifications​

A computer language for formal specifications and proofs​

Formal versions of the above specifications​

The Game of Life​

Trees​

The monad laws​

Further reading​