Design by Contract and Assertions

Motivation: Concerning Correctness

When you produce an element of software, how do you know that what you produced is correct?

This is a difficult question for anyone to answer. Informally speaking, correct software is software that does what it is supposed to do. That is what makes answering the question so tricky. Before you can have any idea whether the software is correct, you must be able to express what it is supposed to do ... and that proves to be quite difficult itself.

In conventional software engineering, a document called a software specification is written in order to describe what it is that a piece of software is supposed to do. Writers of software specifications tend to pursue one of two approaches: the informal or the formal.

Informal specifications attempt to describe software behavior in the natural languages with which humans communicate on a daily basis. There are problems with this approach. Natural language is not precise. Informal specifications are subject to interpretation and affected by the ambiguities, noise, and contradiction inherent in natural language.

In order to avoid these problems, proponents of formal methods of specification turn to the most precise language they know: mathematics. It may be no exaggeration that the study of formal methods has produced more PhD's in Computer Science than it has well-specified software systems. Still the idea that the precision of mathematics can be brought to bear on the problem of specifying software is quite appealing. But, problems lurk here as well. Formal specifications are difficult and time-consuming to construct and verify against themselves, and most software engineers do not have a working knowledge of the mathematics required to work with formal specifications.

There is one more significant problem with both of these approaches. Even if you have a very precise specification, expressed in elegant text and graphics, and placed carefully in an expensive ring binder, how do you know that the software product actually reflects that specification and vice versa? If either is changed, the other must be as well. This is the document synchronization problem.

Design by Contract to the Rescue

Design by Contract (DbC) begins as an implementation of some of the ideas from formal methods and matures into a powerful way of thinking about software. And it does it in a way that is easy for programmers and managers to understand. DbC also puts the software specification into the software document itself which makes it checkable at runtime and eliminates the document synchronization problem.

Model for Software Correctness

Design by Contract is built around a model for software correctness that is really pretty simple.

Suppose there is software routine called s. If we were going to test s, we would probably devise some test inputs or test values to be in place when s starts and then observe what things look like after s completes. If they look the way we think they should then that leads us to believe that S is working correctly for those test inputs.

We can generalize and formalize that process a bit, taking it back from testing an into design. If indeed we know what it means for s to be correct, then we should be able to make a statement of any conditions that must be true prior to executing s. That is, we will state the conditions required for it to be possible for s to run correctly. We call this statement of preconditions for success s's precondition.

Likewise we should be able to make a statement of the conditions that will be true always if s works correctly. This we call s's postcondition.

As an example, suppose s accepted an argument of type REAL and returned another REAL which was the square root of the argument. The precondition for s would be that the argument could not be less that zero, as there is no real square root for negative numbers. s's postcondition would be that the result multiplied by itself would yield the value of the original argument (give or take a little to allow for floating point error).

Assertions in Eiffel

Each Eiffel feature which is a routine, i.e. a function or procedure, can support one assertion for a precondition and one for a postcondition. We saw where precondition and postcondition fit into the structure of the routine in Adding Class Features . An assertion is expressed as one or more assertion clauses which are logically and-ed together to produce the assertion. Assertions clauses are boolean expressions that evaluate to true or false.

Let's look at another example. Assume you need to produce a class to model a time of day. Each instance of TIME_OF_DAY would hold some particular time of day accurate to the second between 00:00:00 and 23:59:59 inclusive.

As a producer, you would be faced with a decision concerning how to maintain the time internally in each instance. For the purpose of our example, let us consider two alternatives:

1. Keep three instance of INTEGER. One each for hour, minute, and second.
2. Keep one instance of INTEGER representing the time of day as the number of seconds since 00:00:00.

This would be an implementation issue for the producer, because it would not affect the services that TIME_OF_DAY could offer clients. If we have a query called minute the first alternative allows us simply to provide the value from storage. Whereas the second alternative will likely cause us to compute minute each time it is requested. But the service looks and works the same for the client in either alternative.

For now let us assume that we are using the first design alternative. In that case we would code class features for hour, minute, and second. feature -- Access hour: INTEGER -- Hour expressed as 24-hour value minute: INTEGER -- Minutes past the hour second: INTEGER -- Seconds past the minute

Below is the code for a procedure set_second which receives an argument of type INTEGER and sets the value of the second feature to the argurment. set_second (s: INTEGER) -- Set the second from `s'. do second := s end

The routine is simple enough, but there is a problem with it. Suppose a client calls set_second with an argument whose value is invalid, say 3574. Our routine would just stuff this value into second and we would end up with an instance of TIME_OF_DAY which is invalid. In the days before Design by Contract, as soon as we recognized that this problem exists, we would go into "defensive programming" mode and code some "if" statements inside the routine to validate the argument, before acting.

Consider though what we can do with Design by Contract. We will add a precondition assertion to set_second that expresses the need for valid arguments. set_second (s: INTEGER) -- Set the second from `s'. require valid_argument_for_second: 0 <= s and s <= 59 do second := s end

The precondition is introduced by the keyword "require". The text "valid_argument_for_second" is the label for the assertion clause. The boolean expression "0 <= s and s <= 59" says that a good value for s will be between 0 and 59 inclusive.

Remember that the precondition specifies those things that must be true if set_second has a chance of working correctly. As such, upon execution, the body of this routine will never be executed if an attempt is made to call it in a state that does not meet its precondition. Instead, the caller will incur a precondition violation exception. We will investigate more about what exceptions mean further in Exception Mechanism .

So, what about a postcondition? We noted earlier that a postcondition should make a statement of what will be true in the case that the routine does its work correctly. For set_second this means that after it finishes, the query second should have the same value as the argument that was received from the caller. Below is the feature with the postcondition added. set_second (s: INTEGER) -- Set the second from `s'. require valid_argument_for_second: 0 <= s and s <= 59 do second := s ensure second_set: second = s end

The postcondition is introduced by the keyword "ensure". Here the expression "second = s" makes certain that the routine did actually do the necessary work to ensure that the value of second matches the value of the argument received.

As you look at the postcondition, you may be tempted to think that the one-line body of the routine is so simple as to make the postconditon unnecessary. To answer this concern we need to look again for a moment at software specification.

Specification of a Routine

If we remove the instructions from a routine and leave its signature, header comment and assertions, we have a specification for the routine. set_second (s: INTEGER) -- Set the second from `s'. require valid_argument_for_second: 0 <= s and s <= 59 ensure second_set: second = s end

This specification of set_second tells us what is required of reuse consumers if they wish to use set_second and what set_second promises to do for them. Importantly, it does that without revealing how it does it does what it does.

So, this specification view, officially called the contract view, is how consumers of class TIME_OF_DAY would view the feature.

If this is the specification, then haven't we put the cart before the horse? The answer is yes. We have done so to illustrate the problems that assertion-based specification can help solve.

Instead of starting with a routine and adding a specification, we really want to start in accepted software engineering fashion with specification first, and then add implementation. Therefore, the specification you see above would exist before the implementation.

Now back to the concern over whether the postcondition is redundant for this simple one-line routine. Obviously, if this specification exists first, then the postcondition must be there, and it would be silly to remove it later. But, more importantly, suppose that when the producer of the class decided on an implementation, he or she chose the second design alternative we mentioned above. This would mean that the internal state of an instance of TIME_OF_DAY would be only one INTEGER with the number of seconds since midnight. That would mean that the query second would probably be a function that computed seconds from that one INTEGER instead of an attribute.

What would change in the specification of set_second? Nothing. The implementation for the routine would be more complex, but what it does, setting the second in an instance of TIME_OF_DAY, would stay the same.

In summary, the precondition and postcondition ensure for use that the routine will only execute if called in a state in which the precondition is true, and then will either complete in a state in which the postcondition is true, or cause a postcondition violation exception.

The Contract for a Routine

Having assertions on its routines forms a contract between the TIME_OF_DAY class and all potential reuse consumers. The contract is much like a contract in business, with obligations and benefits for both parties.

• The client's benefits are outlined in the postcondition.
• The client's obligations come from the precondition.
• The supplier's obligations are in the postcondition.
• The supplier's benefits come from the precondition.

We can see the specifics of these by using set_second as an example.

• The client gets the desired value for seconds set in the instance.
• The client must provide an argument that is valid for seconds.
• The supplier must update the instance successfully.
• The supplier need not risk disaster attempting to process in an invalid state nor waste time validating the argument received from the client.

Valid State for Instances

Assertions on TIME_OF_DAY's routines gives us specification for each routine and guarantees that if the specification of a routine gets violated at runtime we will be served immediately with an exception. This will go a long way toward preventing invalid instances from going unnoticed in a running system and fouling up lots of other stuff.

What will help even more is something called a class invariant. Using the class invariant we are able to state what it means for an instance of a class to be valid, or as it is sometimes put, in a stable state.

The class invariant is an assertion like precondition and postcondition, but there is only one per class. Check Eiffel Classes to see how the class invariant fits into the class structure.

How would we code the class invariant for TIME_OF_DAY? An instance would be valid if its hour were between 0 and 23 inclusive, minute were between 0 and 59 inclusive, and its second were between 0 and 59 inclusive. We can code the invariant as shown below. invariant hour_valid: 0 <= hour and hour <= 23 minute_valid: 0 <= minute and minute <= 59 second_valid: 0 <= second and second <= 59

The name invariant implies that the assertion can never be false ... and that's true up to a point. It's really more like, "it must be true at times when it really counts".

At runtime the invariant must be true for an instance at anytime that the instance is available to clients. In general, this means that the invariant must be true before and after the execution of every exported routine.

As with the assertions on routines, if ever the invariant is not true when it should be, then a class invariant violation occurs.

Remember in the example above, that the features hour, minute, and second are queries, but they could be either attributes or functions.

The Contract for a Class

Earlier we saw the contract for a routine. Now we can define the contract for a class as the aggregation of the contracts for all its exported features, plus its class invariant.

In Design by Contract we design based on these contracts. They are the specifications for the modules in our system. We work in a reuse-oriented world. Whenever we produce a class, we produce it with a comprehensive contract which serves as its specification. We build each class with the thought that it may eventually become reusable.

When we are in our reuse consumer role, using existing classes, we tend not to look at the implementations for the classes we use. Instead we look at their contract views. It is there that we find the obligations and benefits of using each class.

Contracts and Debugging

We saw earlier that having contracts in the code tends to expose bugs at an early stage of development. It is possible selectively to turn off and on the runtime checking of assertions by changing project settings. Checking assertions does involve processing. More about turn off assertion checking in a moment.

Having contracts on a class gives another advantage when the contract gets broken. The contract tells us whose fault it is. Whenever there is a violation of a precondition, postcondition, or class invariant then the software is out of specification. This situation is called a defect, or bug.

Whose fault is it? If a precondition was violated, then a client class attempted to call a routine in a supplier, but made the call in a state that did not satisfy the supplier's precondition. Therefore the bug is in the client.

If a postcondition was violated, then a client made a call in a state that did satisfy the supplier's precondition, but the supplier was unable to complete the work as agreed. Therefore the fault lies with the supplier.

If a class invariant was violated, then the instance has been placed in an invalid state during the execution of a routine, and left that way when the processing completed. This caused the invariant violation. As with the postcondition violation, because the problem occurred while executing routines in the supplier, preconditions must have been met. The supplier then is to blame.

Based on this knowledge, we can say that it is most practical first to turn off runtime checking of postconditions and invariants as we gain confidence in a class. Meaning of course, that we feel confident that any calls that meet preconditions will be properly processed. Then our only worry is that some deranged client will, with total disregard for our carefully crafted preconditions, make calls to our routines from invalid states. So, maybe we will leave precondition checking turned on for a while.

Contracts and Inheritance

In the section titled Inheritance you saw that it was possible through inheritance to produce a new class that has all the features of an existing one. This is a very powerful notion, and could be dangerous. What would keep descendants from redefining inherited features with semantics that were totally different from those intended by the producer of the original class? Nothing if it were not for the contract.

Simply speaking assertions on a parent class, preconditions, postconditions, and class invariants, all are inherited by the class's proper descendants.

For class invariants, if any new invariants are coded in an heir, they will be added to those inherited from the parent, using a non-strict version of logical "and" (We will define non-strict booleans in Writing Assertions below).

That is simple enough. And the situation is also simple for effective routines inherited and left unchanged ... the contracts stand as written.

From our example above you may have gotten the idea that contracts are really useful only for effective routines. Such is not the case. In fact, specifying a contract on a deferred routine is really a powerful notion. It says not only that effective descendants must provide an implementation for this routine, but also that there is a contract that must be satisfied. Effecting or redefining a routine in a descendant class will not make the contract go away. Here is an feature from the Base Library deferred class ACTIVE which models data structures with a current item, and is an ancestor to many effective container type classes. feature -- Element change replace (v: G) -- Replace current item by `v'. require writable: writable deferred ensure item_replaced: item = v end

Feature replace carries the semantics necessary for replacing an item in an ACTIVE. It does not, however provide an implementation. All implementers must produce versions of replace that satisfy the contract specified here.

It actually is possible to alter a feature assertion in an effected or redefined version(technically its a replacement of the original version):

• The precondition can only become weaker than in the inherited contract.
• The postcondition can only become stronger than in the inherited contract.

These rules are imposed as a consequence of the effect of effected or redefined routines on polymorphism and dynamic binding. But, you can understand them from an intuitive viewpoint, if you reconsider the business contract analogy. Suppose a contractor makes a deal with a client to do certain work (represented by the postcondition). Part of the deal might be that the client agrees to have a site ready by a certain date (represented by the precondition). The contractor represents the parent class in the analogy. Now suppose the contractor brings in a subcontractor (representing the heir class) to do a portion of the work. The subcontractor cannot force the client to change the date that the site is to be ready to an earlier date (no strengthing of the precondition). The deal with the client was made by the contractor and so no new or stronger requirements can be imposed by the subcontractor. Likewise the subcontractor must provide at least as much work as was bargained for by the contractor, but may promise to provide more if appropriate (strengthing of postcondition is allowed.)

In Writing Assertions below you will see the syntax for weaking preconditions and strengthening postconditions.

Unfinished Business

In the section Adding Class Features , we promised to explain two issues during this discussion of Design by Contract.

Short Routines

One of these is the tendency of mature Eiffel programmers to write routines that are quite short. It should be clear by now that we wish to build a contract on each routine. The contract describes the semantics of the routine in a declarative fashion. In other words, it tells what the routine does, without giving an indication of how it does it.

Try to imagine giving a declarative description of a routine that was 50 lines long. This could get ugly. So experienced Eiffel developers decompose complex computations into chunks small enough to be described through a clear, concise set of assertions.

Command/Query Separation

In Adding Class Features , we saw that we can categorize features as either queries or commands. A query will ask a question or make an observation about an instance. A command will tell the instance to take some action which may result in changing the instances internal state.

We said that when program routines, that those routines should either be commands or queries but not both. Importantly, asking a question about an instance should not change the instance. Likewise, taking an action that changes the state of an instance should not return a result.

Here's the rationale. In a routines postcondition we use boolean expressions to ensure that the routine has done its job properly. Likewise, class invariants, which define the valid state for instances, are written as boolean expressions. In both cases we may use the features of the class which are queries to ask about an instances current state.

If a query that we use in an assertion were to change the state of the instance, then the result we received would be invalid as soon as we received it.

Therein lies the primary reasoning behind command/query separation. You cannot reason about the integrity of an object if the act of asking a question changes the object.

Writing Assertions

You have seen fairly typical assertions written in the examples above. Study the classes in the libraries to see some excellent working examples. There are a couple of things that need to be covered.

Non-Strict Booleans

One is that, as you can probably imagine, it is not a good thing to cause an exception during the process of checking an assertion. One of the most common ways to cause such an exception is to apply a feature to a Void reference.

The way to avoid this is to use the non-strict booleans "and then" and "or else". These forms of "and" and "or" do not force the checking of all conditions. As soon as a determination can be made, they stop checking. It is typical to see "and then" used to avoid applying a feature to a void reference in preconditons. Below is a creation procedure that uses a non-strict boolean in its precondition. make (a_nm: STRING; a_offset: INTEGER) -- Initalize with name `a_nm' and utcoffset `a_offset'. require name_not_empty: a_nm /= Void and then not a_nm.is_empty offset_valid: a_offset >= -12 and a_offset <= 12 do name := a_nm.twin utcoffset := a_offset ensure name_initialized: name.is_equal (a_nm) utcoffset_initialized: utcoffset = a_offset end

Replacing Inherited Feature Assertions

To replace a precondition on a feature you are effecting or redefining, you use the "require else" keywords to introduce new conditions. These conditions will be logically "or-ed" with the original precondition to form an new one.

Likewise use "and then" to add conditions to a postcondition. The added conditions will be "and-ed" to the original.

Below is an example of weakening a precondition. The first feature shown is from class DYNAMIC_CHAIN in the Base Library. remove_left -- Remove item to the left of cursor position. -- Do not move cursor. require left_exists: index > 1 deferred ensure new_count: count = old count - 1 new_index: index = old index - 1 end

The next feature is from DYNAMIC_LIST, a proper descendant of DYNAMIC_CHAIN. DYNAMIC_LIST weakens the precondition it inherited from DYNAMIC_CHAIN. Originally in DYNAMIC_CHAIN, "index > 1" was required for remove_left. In DYNAMIC_LIST either "index > 1" or "not before" (or both) will suffice. remove_left -- Remove item to the left of cursor position. -- Do not move cursor. require else not_before: not before deferred end

Not Writing Assertions

Let's close this discussion of Design by Contract with one more interesting and point to make about assertions. The precondition and postcondition parts of a routine are optional, as you may remember from Adding Class Features . Suppose you write a routine and do not code either precondition or postcondition. You might be tempted to think that you have simply written a routine that has no contract. But, that would not be the case.

The contract exists, even though you do not code it explicitly. If it were written out, it would look as follows. my_routine -- My descriptive header comment require True ensure True end

What does this mean? It means that you have selected the weakest possible precondition and postcondition for your routine. Of course, this may be perfectly valid under some circumstances.

Just understand that if your routine could speak, it would be telling you, "I can always work successfully without any particular guarantees from you at all. On the other hand, I won't promise you any particular results when I get done."