Excursion: Mathematics of Software Engineering

Introduction

One reason why we studied Hoare logic is that its basic principles (pre/postconditions, invariants, separation of termination and partial correctness, …) are useful to the practice of writing code.

Another reason is that Hoare logic is one of the earliest examples of a successful attempt of developing mathematics of software engineering.

In this lecture, we take another look at this, starting from an idea we only touched upon in the previous lecture, namely Hoare's rule for assignment.

The interesting idea we discovered when discussing the rule is that it works backwards on predicates, from the postcondition backward to the precondition.

One thing I want to show you is that this is not a strange quirk, but rather a general principle.

To do this, let us first insert an excursion on discrete maths. Bear with me, you will be rewarded.

Powersets and inverse image

We reviewed the basic notation about sets and function in a previous lecture. But back then, we just gave the definition but didn't have time to talk more about the inverse image of a function.

If

$$f:X\to Y$$

is a function,^[1] then we think of it as working "forwards",

$$x\mapsto f(x)$$

taking an element

$x\in X$ to an element

$f(x)$ of

$Y$.^[2]

But while a function is working forwards on elements, it is working backwards on subsets.

To see how this works, let

$B$ be a subset of

$Y$, that is,

$B\subseteq Y$.

Exercise: Think of ways of defining a subset of

$X$ using the data

$f$ and

$B$.

There may be different ways of doing this, but the one I am after is what we may call the "weakest pre-condition of

$B$

$$\{x\in X\mid f(x)\in B\}$$

The terminology of "weakest precondition" is appropriate since a subset

$B\subseteq Y$ is a predicate on

$Y$ if we think of

$B$ being true for all

$y\in B$ and false for all

$y\notin B$. Then

$\{x\in X\mid f(x)\in B\}$ is the weakest precondition we need to put on elements of

$X$ in order to guarantee that

$f(x)\in B$. ^[3]

The next question is a bit of a distraction, so you can skip it.

Question: What is the strongest precondition? [^strongest]

Notation: If

$f:X\to Y$ and

$B\subseteq Y$, then we define the inverse image of

$B$ under

$f$ to be

$$f^{-1}(B)=\{x\in X\mid f(x)\in B\}$$

The next question one should address is the following. If

$f^{-1}$ is itself a function, then what are its domain and codomain?

$f^{-1}$ maps subsets of

$Y$ to subsets of

$X$. For convenience, we agree on the

Notation: We define

$\mathcal{P}X=\{A\mid A\subseteq X\}$. The set of subsets

$\mathcal{P}X$ is also called the powerset of

$X$.

Exercise: We collect some useful facts about

$\mathcal{P}X$ for finite

$X$. Recall the notation

$|A|$ for the cardinality (=number of elements) of a finite (or infinite) set

$A$. We also write

$2$ for both the number and the set

$\{0,1\}$.

• $|\mathcal{P}X|=2^{|X|}$
• Elements of
  $\mathcal{P}X$ are in bijection with functions
  $X\to 2$.
• $|\mathcal{P}X|>|X|$

We can use this notation to state succinctly that if we have

$$f:X\to Y$$

"going forward" then we also have

$$f^{-1}:\mathcal{P}Y\to \mathcal{P}X$$

"going backwards".

The second item of the exercise says that subsets "are the same thing" as functions into the Booleans. We explore this a bit more in the following

Remark: There is an important alternative to understand what a subset is. Instead of saying

$B\subseteq Y$ we can also consider its so-called characteristic function

${\chi }_B:Y\to 2$, which is defined as

${\chi }_B(b)=1$ if and only if

$b\in B$. Here we use again our convention that

$2=\{0,1\}$. A little thought shows that there is a bijective correspondence between subsets of

$Y$ and functions

$Y\to 2$. And now we can understand better why functions work backwards on predicates (=subsets). Indeed, given a function

$$X\to Y$$

and a subset

$$Y\to 2$$

we can put them together (using sequential composition) as

$$X\to Y\to 2$$

That is, a subset on

$Y$ gives a subset on

$X$.

More Notation (not so important now, but useful later): If you look at

$|\mathcal{P}X|=2^{|X|}$ and also at the fact that elements of

$\mathcal{P}X$ are in one-to-one correspondence with functions

$X\to 2$, it is tempting to write

$$2^X$$ for the set of functions

$X\to 2$. Because then we can summarise what we learned in the first two bullet points of the previous exercise by the short and elegant

$$|2^X|=2^{|X|}$$

And, in fact, this notation for sets of functions is widely used. So we often find the set of functions

$A\to B$ denoted by

$$B^A$$

and again we have an elegant formula to compute the number of functions

$A\to B$ in terms of the number of elements of

$A$ and

$B$. The formula is

$$|B^A|=|B{|}^{|A|}$$

Duality of state and predicate transformers

The relationship between

$f$ and

$f^{-1}$ is called a duality because of the change of direction with

$f$ going forward and

$f^{-1}$ going backward.

Another feature one likes to have in a duality is that there is a bijective relationship between the "forward functions" and the "backward functions". This is can be made to work here and if you know about Boolean algebras you can try the following exercise.^[4]

Miniproject: The aim is to show that not only for every map

$f:X\to Y$ there is an inverse impage

$f^{-1}:\mathcal{P}Y\to \mathcal{P}X$, but to characterise those maps

$\mathcal{P}Y\to \mathcal{P}X$ that are inverse images.

• If
  $X$ is a set, then
  $\mathcal{P}X$ is a Boolean algebra.
• If
  $f:X\to Y$ is a function, then
  $f^{-1}:\mathcal{P}X\to \mathcal{P}Y$ is a Boolean algebra homomorphism.
• If
  $A$ is a finite Boolean algebra, then there is a finite set
  $X$ such that
  $\mathcal{P}X$ is isomorphic to
  $A$.
• If
  $X,Y$ are finite sets, then any Boolean algebra homomomorphism
  $\mathcal{P}Y\to \mathcal{P}X$ is of the form
  $f^{-1}$ for some
  $f:X\to Y$.

This observation above is one of the most important ones in all of mathematics, logic, and computer science.

In programming terms, we can think of elements of

$X,Y$ as states, of

$f$ as a computations, of elements of

$\mathcal{P}X,\mathcal{P}Y$ as specifications, and of

$f^{-1}$ as computing weakest preconditions of specifications.

Accordingly, then, we may call

$f$ a state transformer and

$f^{-1}$ the corresponding predicate transformer.

The importance of duality lies in part in the possibility of going from predicate transformers to state transformers, that is, from specifications to programs.

This idea has been turned into a whole field of study of how to derive programs systematically (and perhaps automatically) from specifications. For some references, look up predicate transformer semantics. A development of this is the Bird-Meertens formalism. If you like functional programming have a look at Bird, de Moor: Algebra of Programming .

Duality of algebra and geometry

Here I want to show you that you have seen a similar duality already in high-school when you used algebraic methods to solve geometric problems.

Recall how the equation

$$y=mx+b$$

describes a straight line with slope m intersecting the

$y$-axis at

$b$.

This equation defines a predicate on the plane of points

$(x,y)$.

Indeed, we

$(x,y)$ is a point on the line if and only if

$y=mx+b$ is true.

Note that there are infinitely many points on the line and that the totality of these infintely many points is completely described by the equation

$y=mx+b$ consisting only of 6 symbols.

To make the analogy with programming, the equation

$y=mx+b$ is a specification ("

$(x,y)$ is on the line of slope

$m$ andand any point

$(x,y)$ satisfying the equation is an implementation. ^[5]

On the mathematics of software engineering

Now let me come to the main point of the excursion into geometry. As we are all aware from high-school mathematics, equations such as

$y=mx+b$ are not only used to define geometric figures.

What is even more important is that there is a whole calculus, algebra and analysis, that allows to manipulate these equations and compute with them.

To develop similarly powerful mathematics in order to manipulate specifications and programs instead of geometric figures is the dream of software engineering.

One reason to spend quite a bit of time on Hoare logic is that Hoare logic is one of the earliest and most successful attempts in developing such a mathematics of software engineering.

Further Reading

(more to be added…)

Some further references can be found in the wikipedia articles on

predicate transformer semantics

and the

Bird-Meertens formalism.

If you like functional programming have a look at Bird, de Moor: Algebra of Programming .

---

1. For our purposes it may be helpful of thinking of

   $f$ as a program, but nothing in the following depends on this. ↩︎

2. Thinking about

   $f$ as a program, we can think about
   $X$ as the set of inputs and
   $Y$ as the set of outputs. Alternatively, we can also take
   $X=Y$ to be the set of all possible memories and think of
   $f$ as a program transforming the contents of the memory from an "input-memory" to an "output-memory". ↩︎

3. If we think of a "condition" as a subset, then a weaker condition is a larger subset and a stronger condition is a smaller subsets. More formally, a condition on

   $X$ is a subset of
   $X$. The condition
   $A\subseteq X$ is stronger than the condition
   $A^{\prime }\subseteq X$ if
   $A\subseteq A^{\prime }$. What are the strongest and weakest conditions on
   $X$? ↩︎

4. The technical notions are reviewed here (never got around writing this and we didnt need it for the course). ↩︎

5. The analogy is not perfect because we cannot explain here what really is the analogue of programs in geometry … this would require more time and lead too far away from where we want to go. But the main difference between computer science and geometry can be easily sloganized: In computer science we are interested in irreversible operations in time, in geometry we are interested in reversible transformations in space. ↩︎