This post was originally published in my blog

Specs, specs and specs. The often forgotten aspect of software design. Defining the specification of the project is the first step in any successful software project. And yet it is often overlooked. It gives us not only the opportunity to understand the need of the client, but also to synchronize the work inside a team of developers more easily and avoid any negative side effects.

My goal here today is not to talk about what is their importance or why are they so useful. But it is about showing some key aspect to have in one's mind during the specification design phase.

N.B: To make things simpler, I am going to focus here on method specification, but a generalization can be applied to more advanced structures like classes or modules.

What are specifications

the specification of a method is the definition of the following:

• The prototype of the method to define the parameters of the method and their type.
• The preconditions are what conditions should be fulfilled before the method procedure could start.
• The postconditions are what conditions are guaranteed on the outputs of the method.

By convention the preconditions follow the keyword requires, while the postconditions follow the effects's keyword.

The importance of the specification can be felt at the implementation phase. it forces us to agree on the method and its side effects, and by then have no disappointment after the development phase from the its client (The client here refers to the user of the method).

Deterministic vs Non-deterministic specifications

You can find two types of specs: deterministic and non-deterministic.

A deterministic specification is a specification that is precise enough so that any implementation of that specification from the implementation space will yield the same results. That means that regardless of how the method was developed, or the person that have developed it, we can trust that the client will get from all of the implementations the same result.

A non-deterministic specification, on the contrary, gives more freedom to the implementer, since in the implementation space of the method, we can have implementations that won't give the same results. So the client can't trust these different implementations since he is not sure that they will converge on the same results.

A small example to understand. Let's consider the following spec.

int find(vector<int> arr, int val)
requires: the val exists at least once in the array
effects: returns the index i such as arr[i] = val

This is a non-deterministic specification. In this case we cannot be sure if the index that will be returned is the smallest or the biggest one found for example. An implementation may start from the lower bound, another one from the higher bound.

To make a deterministic specification we can say:

int find(vector<int> arr, int val)
requires: the val exists at least once in the array
effects: returns the lowest index i such as arr[i] = val

The goal of any determinization is to remove the ambiguity. And it is the same goal here: Removing the ambiguity from the statement, so that the implementers can agree.

Stronger vs weaker specifications

Now that we have our specification in place, what if we want to make a stronger or weaker one. Well the answer to that question is very tricky, since we need to understand first what do we mean by a stronger specification or weaker one.

A weaker specification is a specification that demands more from on the client and put less responsibility on the method, while a stronger one puts more strains on itself, and relieves the client from some of the task's responsibilities. Mathematically speaking, in a given implementation space for a method, the more stronger the specification is, the more smaller the space is, while on the contrary, the weaker the specification, the bigger that space. In other words, a weaker specification asks more of the inputs (A.K.A the client), and less from outputs, whereas a stronger reverse this statement.

For a given specification, to make it weaker (or stronger), you need either to put more (less) preconditions, or less (more) postconditions.

This may sound counter intuitive, but if we take into account the definition above, the weaker the preconditions, the more responsibility we put on the method since it has to handle the test cases it did not before. While the more postconditions we put, the less headaches the client will have with the effects of the method.

For illustration let's take the example we used earlier:

int find(vector<int> arr, int val)
requires: the val exists at least once in the array
effects: returns the index i such as arr[i] = val

To make this specification weaker, we can ask from the client more efforts. To do so, we can write it as such:

int find(vector<int> arr, int val)
requires: the val exists once and only once in the array
effects: returns the index i such as arr[i] = val

While to make it stronger, we can impose more conditions from the outputs. For example, we can do:

int find(vector<int> arr, int val)
effects: returns the index i such as arr[i] = val or -1 if the val is not found

Writing good specifications

Good specification is crucial, specially in the context a team work. It provides the developers with the necessary tools for them to be on the same page and not diverge in their implementations. It is mandatory for a specification designer to take into account these two key concept, to pay attention to what specification is he writing, and to ask the good questions. Is it all right if this specifications is non-deterministic, or it may put the integration of the modules at risk ? Do we need a stronger specification on this class, or this weak one shall do it ? These are some of the most important questions that he shall bare in mind during the whole process.

There are other key aspects in designing a specification that were not mentioned in this post, like defining exceptions, but still it is already enough for now I guess. Maybe I will write about them in another piece.

Happy coding, and stay safe !