| |
Introduction to Eiffel.NET
Part Three: Design by Contract
In Part One I introduced Eiffel and talked about is basic language constructs. In Part Two we explored some more advanced language features. It's now time for the big bucks: Design by Contract (DbC).
Intended audience. In order to make the most of these tutorials, you should not only know how to code in some Object Oriented programming language (like C#), but also understand the basic theory of OO design (inheritance, polymorphism, and so on). Make sure you brush up on that before you begin. Reading the tutorials in order also helps :)
In this tutorial I will talk about software correctness and how it can be more easily achieved in Eiffel using assertions and contracts.
References. Like the other times, I've used the documentation in Eiffel ENViSioN! to get examples and ideas. There's more detail there if you wish to continue you Eiffel development days.
Software Correctness
Ok, so no one likes bugs. The problem with writing correct software is that a piece of software is correnct if, and only if, it does exactly what it is supposed to. The problem is one of details. If you are 100% exact, you almost end up writing the software, and if you handwave, you'll miss important cases. How then to make correctness feasible?
Many formal ways of specifying correctness (or, equivalently, functionality) have been devised, but the problem is that once you write your code, they are in their nice binder and if you didn't respect them no one may notice any soon. Pre- and post- conditions inserted in comments cannot be enforced, so if you want to make sure they hold you have to check them at BOTH and the client and the supplier. This makes your code inefficient and prone to even more errors.
The solution is adding these details in the code itself, so the compiler will enforce them for you. And not as normal code, but recognized as such, which also makes them easy to disable once you trust that your software works. You want to do this module-by-module because you want each module to be correct within itself (respect its postcondition) AND being able to trust its clients (because they are respecting their pre-conditions). For more details on the motivation and theory behind this, as well as for becoming an expert in everything object-oriented, I highly recommend Betrand Meyer's classic book Object-Oriented Software Construction (no, they're not paying me to say this, they don't even know I'm doing this :).
So, DbC is this: a formal way to tell the Eiffel compiler what are your expectations and guarantees regarding a module (always a class in Eiffel), and having the compiler enforce them. The model is still based around preconditions and postconditions, but now you have a way to express these in mathematical (so also logical) notation.
In case you're rusty about this, a precondition is a statement (about something like a parameter) that has to be true when a routine is entered (like that x is positive before calling sqrt(x)). The postcodintion is a statement about what the return value (or side-effect, but that's hard to pin down) should be (like sqrt(x)*sqrt(x) = x). Also of notice, the class invariant is a statement always true about the class (doesn't apply to routines, you need data for it to make sense); this is of course the "stable state" of the class, so it must be true at the end of your methods (or when your class is available to be used) not while you're playing around within them (for example if you have an array with an iterator, the iterator position is always >0). If you studied Abstract Data Structures, you may know that specifying these properties is enough to define the behavior of a class, for example you can write, say, a stack in Prolog just by coding these logic rules. So Eiffel turns out as a great language for BOTH designing and programming.
Let's see how to do this in practice.
Assertions
Each routine in Eiffel can contain an assertion for a precondition and one for a postcondition. Assertions are boolean statements (i.e. they are either true or false), and are composed by boolean clauses that are ANDed togheter (in logic jargon, they are in conjunctive normal form, or CNF).
Assertions give you the power of both a if-then statement (which you would need to verify them) and a try-catch block (which you will need to handle errors). We saw last time how the "rescue" keyword can be used to recover from a false assertion.
In Eiffel preconditions are introduced by the require keyword, and postcondition by the ensure keyword. As most the keywords in Eiffel, these do a lot to improve readability. Each line after the keyword is a clause, and each clause has two parts separated by a colon: an identifier with a name for the clause (again at least for readibility, but also to reference to it), and the boolean expression iself. For example:
ensure
item_count_increased: item_count = old item_count + 1
|
This also introduces us to the "old" keyword. You can use to talk about the value of a variable before the function was called. Here assertions add another facility we'd have to code every time.
Let's look at a small example. Suppose you're writing a time class and need to set the second as an integer. You want to range-check the input and ensure the client that the data as been applied:
set_second (s: INTEGER) is
-- Set the second from `s'
require
valid_argument_for_second: 0 <= s and s <= 59
do
second := s
ensure
second_set: second = s
end
|
As you can see, this is clearer and shorted than if-then and try-catch blocks. Now, look at the "do" block. What if our internal storage was something like the number of seconds since midnight? The implementation would be different, but the assertions would not be. So you could give a class with only feature declarations with assertions to a developer, and get back an implementation that is guaranteed by the compiler to do exactly what you want no matter the implementation. The above (without do) is called the contract for a routine, and we'll talk about those in the next section.
Now let's look at one last assertion, which is about classes instead
of just routines. You may remember from above that this must be the class invariant. Class invariants are assertions like the above (in CNF), and there's one per class. Let's look at the assertion for the time class above:
invariant
hour_valid: 0 <= hour and hour <= 23
minute_valid: 0 <= minute and minute <= 59
second_valid: 0 <= second and second <= 59
|
This block will be placed in the class like a feature, usually as the last element of your class (so after all the features). As I mentioned above, then, every clause of the above must be true at all times when the class is in a stable state. The names above (hour, minute, and second) could be attributes or even function calls for the class.
Now a note on non-strict booleans. The idea is to avoid exeptions during assertion-checking by not trying to evaluate void pointers. You can use short-circuited evaluation (i.e. stop evaluating as soon as a decision can be made) by using the keywords "and then" and "or else". Example:
require
name_not_empty: a_nm /= Void and then not a_nm.is_empty
|
Contracts
A contract is specified in Eiffel by assertions, and is defined as follows in the docs:
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.
So, in Eiffel a class contract is the text of a class without implementation (do blocks) but with all the features and assertions about them, plus the class invariant. This is the basic unit of design in Eiffel.
As I mentioned, contract in Eiffel are enforce by generating code, but this can be disabled to make our code run faster (and just have great documentation left). The switches are very detailed, covering each class and each type of assertions in it. Some advice from the Eiffel docs on this matter:
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.
Now, think about inheritance. There's the classic problem that someone may subclass your class and do nasty things with your methods, using their names the wrong way. What's there to stop them except a little type comformace? Nothing. Well, you saw this coming, but in Eiffel contracts are. In Eiffel assertions are inherited, using an extension of type comformace:
- A deferred base class can make a great contract and can be compiled. The implementors must respect the contract, and can change the assertions if:
- The preconditions are weaker than in the inherited contract.
- The postconditions are stronger than in the inherited contract.
The docs give us a great business analogy to understand this constraint, which I report in full: Suppose a contractor (representing a parent class) makes a deal with a client (representing a client class) to do certain work (representing the postcondition). Part of the deal might be that the client agrees to have a site ready by a certain date (representing the precondition). 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.)
This also means, for simpler cases:
- If you're using effected feautures leaving them unchanged, all the assertions apply.
- Class invariants are inherited, and the new class invariant is the parent one "and then" (non-strict and, like above) the child's new additions.
- 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.
Final thoughts
Now for some icing on the cake. Both in stardard Eiffel, and even more easily in Eiffel.NET, you can reference an external routine in the body of the feature, so you can eventually (i.e. by disabling assertion checking after testing) compile a fast C (or IL) program after you designed it as a high-level object oriented software! Of course Eiffel either generates C code or IL (depending which one you use), so you could just use Eiffel for everything.
Before we finish, I have some homework of sorts for you.
Pick a class of your choice (a simple but uncommmon data structure will do). Now write an Eiffel class contract for it, and give it to someone that has never seen Eiffel before (there's plenty of them, just say it's your notation, and assume they know object-oriented terminology, like what an invariant is) and ask for some code back to fill in the features in any language. For extra credit, also give a paragraph in English describing the same class to someone else, and compare the quality of the results. You'll understand how great the readibility and power of Eiffel's Design by Contract are.
Ok, it's more like a thought experiment (or an experiment for thought), but you get the idea :)
In these three tutorials I've introduced you to the basics of the language (there's more, but this is not a reference!). Next time I will talk about how to use Eiffel in the real world using the Visual Studio .net plug-in ENViSioN! If you have ideas on topics I should cover send me an email or post a comment below.
|
|