Reasoning: An Introduction to Logic, Sets, and Functions

Subsection 6.2.10 Specifications for a Sorting Program

Formal specifications of important programs do several things for us:

1. They force the writer to be completely clear about what the program is actually supposed to do. This means that the reader knows what the writer meant.

2. They may make it possible to match the current specification against specifications of programs that already exist. Maybe we don’t have to write code from scratch.

3. They may make it possible for an automated reasoning system to check to make sure that the program does what it is supposed to do.

So, while writing these specifications isn’t a trivial task, it is often worth it. Let’s see how we can do it.

When we work with large amounts of data, we often want to sort the items first, before we do anything else. That will make other things much easier. For example, would you want to look someone up in a phone book if the entries were arranged randomly?

So suppose that we want someone to write a sorting program for us. Can we write a logical statement that specifies what the program has to do? Notice that we’re not saying how the program should sort. Whole books have been written on that subject. We’re just specifying the result that we should be able to guarantee after the program has run.

This example is a little more involved than most of the others that we’ve done so far. So we have to set up several things before we can actually write our specification.

We’ll assume that we are working with lists of entries. So a list might be:

(Entry1, Entry2, Entry3, ….)

Each entry may have several fields (properties). To describe what a sorting program has to do, there are two properties that we care about. We’ll assume that there are functions (provided by someone) that can extract values for those properties when we need them. The functions are:

key(x): produces the value on which we’re sorting. So, for example, the record might be a phone book entry. Then key(x) returns the name associated with that entry (since we want to sort on name, not address or phone number).

position(x, list): produces the position of x in list. For example, if x is the first element in PhoneList, then position(x, PhoneList) will be 1.

Next, we need to define what we mean when we say that the list is sorted. If we’re working with a list of integers, then we want them sorted with the smallest number first, going up to the biggest one. So List1 here is sorted, while List2 is not:

List1: (5, 10, 15, 20, 25, 30)

List2: (10, 30, 5, 15, 10, 25)

How shall we capture, in a logical statement, how we want things ordered? When we’re working with a complex problem, we want to focus on one thing at a time, if we can. So let’s define a predicate that tells us whether one thing should come before another. We will hide the details of what determines that. So we’ll define:

ComesBefore(x, y): True if x comes before y in whatever order we have agreed we want to produce.

We will need a few other predicates as well:

List(x): True if x is a list of elements.

In(x, y): True if x is in y.

Permutation(x, y): True if x is a permutation of y. That means that x and y contain the same elements but not necessarily (although possibly) in the same order. Again, let us assume that, as a separate effort, we can define precisely what it means to be a permutation.

Let’s call the input to our desired program inlist and the output of our program outlist.

Now we’re ready to write our specification: