Design By Contract
Design By ContractDesign By Contract (DbC) is a software correctness methodology. It uses preconditions and postconditions to document (or programmatically assert) the change in state caused by a piece of a program. Design by Contract is a trademarked term of BertrandMeyer and implemented in his EiffelLanguage as assertions.
The pre- and postcondition technique originated with the work of TonyHoare, whose 1969 Communications of the ACM paper described program semantics using such assertions. Hoare's 1972 Acta Informatica paper described the use of representation invariants and abstraction functions to prove correctness of abstract data types.
Pre- and postconditions were first supported natively in a language in BarbaraLiskovs CLU (circa 1974 - 1977).
DbC has been explained in various Eiffel-related texts and papers. Some of them:
DbC Support in languages:
Some attributes of Design By Contract...
[please add more about what 'contract' is]
Classes should specify their invariants: what is true before and after executing any public method.
Methods should specify their pre- and post-conditions: what must be true before and what must be true after their execution, respectively. Pre-conditions may be weakened by subclasses and post-conditions may be strengthened.
The explicit definition of these "assertions" forces the designer to think deeply about what is a requirement of the specification and what is an artifact of a particular implementation. These assertions can and should influence the declaration of "throws" exceptions as well as the throwing of runtime exceptions and try/catch in general.
For example if a method has specified some pre-condition then the failure of that condition is the responsibility of the client of the method. The method should not have to declare a checked exception for that condition, it should not have to test and throw for that condition, and likewise the client should not have to try/catch for that condition.
The client *should* do whatever is necessary to ensure it will meet the pre-conditions. It may do runtime tests or it may assume some condition is satisfied based on its own specification.
This eliminates clutter and redundant checks. How many times have you seen call stacks of methods where the first thing each method in the stack does is to check for some condition that its caller already checked? How many times have you had to implement a try/catch for a condition you know will not occur? Pre- and post-conditions reduce the need for such clutter and inefficiency. (In this regard, maybe they are an "anti-idiom" because they enable the programmer not to use an idiom!) They also document more *precisely* what a method or class is supposed to *do*. -- PatrickLogan
How do you balance this with DefensiveProgramming? Take an account class that has a withdraw() method. Clients should probably check to make sure that there are enough funds:
if(account.hasEnough(fundsToWithdraw)) {
account.withdraw(fundsToWithdraw);
}
However the withdraw() method shouldn't blindly process the withdrawal. Sloppy client code would result in an inconsistent system. Shouldn't the withdraw() method do the check as well?
void withdraw(amount) {
if(!hasEnough(amount)) {
throw new InsufficientFundsException();
}
balance -= amount;
}
Of course now that we throw an exception the client doesn't have to do the check ahead of time. I definitely prefer this way, as the withdraw() method can't leave the system in an inconsistent state.
Isn't it better for a method to check that all the preconditions are met instead of assuming that client code will do it? -- PatrickMaddox?
See also the LiskovSubstitutionPrinciple. The LSP is definition of subtyping in terms of substitution; it says (roughly) that you can replace types with subtypes without affecting the meaning of programs that use them. The Contract part of DesignByContract makes explicit the part of the behaviour which we expect not to change. -- DaveHarris
Design By Contract can have a great effect on the definition and use of exceptions.
The Sather programming language has Design By Contract services. Visit http://www.gnu.org/software/sather/
Maintenance of Pre-Conditions and Post-Conditions
Every method has a pre-condition and a post-condition whether you specify it or not. Why would you not specify it?
At a minimum their specification even as comments improves code because it tells you what the client should make true before using it, and exactly what it can expect to be true afterwards.
Why would maintaining the definition of a method increase maintenance costs over and above not maintaining the definition of a method? Is guessing cheaper than knowing?
Specifying the contract of a method and which parts are the responsibility of a client and which the service actually *decreases* code volume. Haven't you ever seen code where there is boiler-plate-like preamble that checks some condition and then sends to another method which checks that same condition which then...
Knowing the responsibilities makes for efficient code, not unlike register saving policies when generating code for procedure calls. Is it callee saves or caller saves? That's part of the contract.
-- PatrickLogan
Here's another reply to RonJeffries' concerns about contracts.
First, the ideal environment for DesignByContract is when the language you use has support for them. (That is, Eiffel. Are there more?) This means that you can turn all (or part) of the contract checking off for release, and run with full contract checking using debugging and testing. That makes performance a non-issue. (See also EfficientContractsInJava.)
With the performance issue out of the way, let's look at the system's reliability. Ron says that a program "might go down in a more orderly way, but it still doesn't work." This is a big advantage of contracts. The program still does not work, but now you get a very good hint about the why. Because the program stops close to where the error is, instead of where you observe the error. In my experience those places are often far apart, and finding your way back to the source of the error takes most of the debugging time. Most bugs are simple bugs, meaning they are simple to fix. Many simple bugs manifest themselves in complex ways, and take ages to find.
Now for maintenance. Contracts have to be maintained too. But they are often obviously correct, and need not be changed often. And if you need to change a contract, you gained understanding about the software problem you're solving. For me that's the second advantage of contracts: they force me to think about the problem.
An example (one of the many). A couple of months ago we designed and implemented this complex data structure. (A tree with sharing and information that could be added in several places, and the tree could be manipulated in zillions of ways.) While we were implementing another part we suspected a bug in some part of the tree implementation. We searched for half an hour. Then we discovered a comment: "TODO: Add class invariant so-and-so". We did that, and then three minutes later the bug was found and fixed.
We also use contracts as documentation. (Basically, that is what contracts are: executable documentation.) This is a very useful aspect. For example, when I implement a limited version of a method that only works for integers in the range 0..255, I add a contract with the explanation 'implementation restriction'. When I run into this limit, or for the final release, I do a full implementation and change the contract so that all non-negative integers are accepted.
In ExtremeProgramming this is probably not a good argument, since there people seem to avoid documentation.
One might more accurately say that we think the code, properly crafted, is the best documentation.
By the way, I saw somewhere some test cases used in UnitTests in the C3 project. At least some of these were simply checking contracts: if I put this in, that must come out. [Can somebody put in a reference? I cannot find the test cases anymore.] So using contracts may decrease the number of test cases that have to be written.
Perhaps contracts are not needed for ExtremeProgramming, because UnitTests serve a similar function. But at least in our shop contracts pay off.
Ron, have you tried contracts within (or without) ExtremeProgramming? What were your experiences? Yes. See below.
I'll just add that in some application domains, the best thing that can happen is that your program asserts rather than being silently wrong.
I really think that many people in the Smalltalk and Java communities do not use contracts because there simply is no support, and it is hard to see the benefits when there are downsides to all native language attempts. Sure, you can kludge it together, but without conditional compilation you are going to incur some overhead in a production system and no one wants to consider doing that.
In C and C++, we have been able to do DesignByContract for a long while and we see the benefits. Here is a snippet that I used in CppUnit (a C++ port of KentBeck's framework for UnitTests):
#define assert(condition) (this->assertImplementation ((condition),(#condition), __LINE__, __FILE__))
This takes the text of the condition, the line number and the filename at the point of failure, and bundles them for an exception to throw. Note that we are able to get an obscene amount of information this way. And it is very easy to turn them off so that they compile into nothing. PreprocessorsAreNotEvil. -- MichaelFeathers
Just a question: does a class + it's UnitTest have twice as many places to have errors if we are relying on the test to prevent errors? Or, are you talking about expression side effects? -- MichaelFeathers
Assertions and UnitTests are both ways to specify the class's contract, so the people who say that without assertions the contract is unspecified have failed to understand the argument.
I see assertions as a poor man's program prover (this idea comes from Meyer, by the way). Although in Eiffel they are imperative, that's only because of limitations of that technology. We should try to think of a precondition like "x > 0" as meaning x is always positive; not just that this particular x is.
So, assertions are declarative while UnitTests are imperative. Assertions are for static reasoning about code while UnitTests are for dynamically testing a few examples. You need both. They complement each other.
Put it this way: could you generate the UnitTests from the assertions? Or vice versa? I think mostly not. To the extent you can, I'd prefer to write the assertions first and then have a tool generate some UnitTests from them.
-- DaveHarris
Assertions are for static reasoning about code while UnitTests are for dynamically testing a few examples. You need both. They complement each other.
I agree. The only problem I see with Assertions is that there is no way to reason about them. Let us say for example that you write a ClassInvariant for your class A and for another class B. Then class A uses class B. How do write a program that statically (without running the code) finds out that you have broken a ClassInvariant?
If that were possible I would use ClassInvariants? a lot. Otherwise you have to use it only as a complement to the dynamic verification the UnitTests do.
I agree. DBC isn't going to guarantee that you will have tests of boundary conditions.
Aside from actually doing DBC, I enjoy working with people who know what it is. The HeuristicRule of making the caller responsible for the precondition is useful even if you never litter code with little tests.
BTW, I like the tool idea a lot. -- MichaelFeathers
I've worked both ways and dropped assertions as wasteful of time and insufficiently helpful in increasing reliability or understanding. I believe but have not tested that the effect would be stronger in object languages with their smaller methods.
Do we know of any actual experiments comparing the effectiveness of assertions to alternatives? It seems to me that they are most often recommended because they seem good in principle, rather than based on actual experience. -- RonJeffries
P.S. I'm removing my comments elsewhere in this page: they don't seem to be helping. Owners of replies might want to do the same or re-justify your remarks.
Well, they are recommended because of actual experience, but I'd guess most of that experience is going to assertions from nothing at all. You've made some good points here - you've certainly made me re-evaluate the area. -- DaveHarris
The recommendations I've seen have been from academics and theoreticians, not based on experience in commercial development situations. (With all due respect to academics and theoreticians who may be passing by.)
I recommend them because of actual experience, then. (Note caveat about not having compared them with UnitTests.)
MichaelFeathers has a good point: at least some of the benefit is due to improved mental habits. In order to make the contract explicit you have to think about what the limitations of new code should be, what the limitations of old code you are calling actually are, how responsibilities should be split between caller and callee.
This is all undoubtedly good stuff; I'd expect commercial developers to recognize it. And it's all common to both assertions and UnitTests. With hindsight, it is a shame that the phrase "DesignByContract" has been high-jacked by assertion-based mechanisms. Is it too late to use it for UnitTests too? I expect I will anyway, at least when thinking about it. --- DaveHarris
DesignByContract was invented by Bertrand Meyer and implemented in his Eiffel programming language as assertions, so I don't think that any hi-jacking going on here. Besides, UnitTests don't enforce a contract, I don't know where that idea came from. There isn't really any thing here that supports it. Can anyone elaborate?
I use a macro that combines an assert with a throw in my code to enforce pre-conditions. (my environment doesn't terminate the application on an assert). I don't mess around with post-conditions (well, okay I do UnitTest those) and I do very little with class invariants, but when I do I use the same macro. This has the effect of enforcing the contract even in production. -- PhilGoodwin
By the way, I saw somewhere some test cases used in UnitTests in the C3 project. At least some of these were simply checking contracts: if I put this in, that must come out. [Can somebody put in a reference? I cannot find the test cases anymore.] So using contracts may decrease the number of test cases that have to be written.
UnitTests are testing to see whether the class works. I suppose that is the same as checking whether contracts are upheld. Semantic difference only at that level? UnitTests are separate classes from the subject class, and generally actually exercise the class in a way that embedded contract checking cannot. In order to get comprehensive testing, even if you do have contracts, you need to have an external exerciser of some kind. We have that in our UnitTests and AcceptanceTests, and the tests do the checking as well as the exercising. -- RonJeffries
Assertions and UnitTests have a lot in common. Let's focus on the differences:
Contributors: DaveHarris RonJeffries BillTrost StuHerbert, NickLeaton?
I'd say that 1-3 are advantages of assertions, and 4,5,6,8 are reasons to use UnitTests as well. -- DaveHarris RonJeffries
I'd say that 7 and 9 relate to (minor) drawbacks of assertions, which may or may not be reason to avoid them depending on the implementation. Some of the samples above seemed quite unreadable to me, for example. -- RonJeffries
14 is the really interesting one. Given Assertions, you don't need to write as much code in your UnitTests You need your UnitTests to exercise the code, and have the Assertions doing the testing part for you. If you then run the code for real, the testing is also performed by the Assertion. This is not the case with UnitTests
JML has a unit testing tool that can use specifications such as pre and postconditions to help decide test success or failure. Parasoft's JTest is somewhat similar. Both of these tools allow you to get the best of points 1-5 and 11. --GaryLeavens
Some quotes from above:
Every method has a pre-condition and a post-condition, whether you specify it or not. Why would you not specify it?
Because every line of code we write requires reading and maintenance, and is subject to error. The benefit of conditions may outweigh these costs, but the costs are significant. A better question might be "when would you and when would you not specify it". -- RonJeffries
That applies to UnitTests as well, doesn't it? When would you not bother to write a UnitTest? -- DaveHarris
At a minimum their specification even as comments improves code because it tells you what the client should make true before using it, and exactly what it can expect to be true afterwards.
In procedural languages this might be more true than in object languages, IMO. Since comments and reality can and do go out of sync, I would particularly deprecate use of assertions as comments. If a method deserves an assertion, it deserves a real one. -- RonJeffries
Agreed. AssertionsAsComments is for when you are cannot express the condition within the assertion language. -- DaveHarris
Why would maintaining the definition of a method increase maintenance costs over and above not maintaining the definition of a method? Is guessing cheaper than knowing?
Straw man. The assumption of the above is that only by specifying the definition can one know the definition: that guessing is the only alternative. This is a significant overstatement. -- RonJeffries
Example:
balance ^self inject: 0 asDollars into: [ :sum :each |sum + each]What are the pre- and postconditions for this very typical Smalltalk method? I haven't a clue.
Probably simple, e.g. the result is a non-negative amount of money. -- PatrickLogan
A precondition guarantees a correct result. In this case, the sum must not overflow the representation. When some one gives me more dollars I expect to have more dollars. This is not testable on entry. -- DickBotting
The question to ask is: "When is it legal to invoke the balance method?". If the answer to that question is: "You may ask for the balance of an account at any time", then there are no preconditions to that method. If the answer is "You should only ask for the balance of open accounts", then the precondition should be isOpen. The precondition is less about the method itself, than about the assumptions that go into using the method. -- JimWeirich
Written in C, it might look something like this:
USDollar balance()
{
USDollar result = 0;
for ( int i = 0; i < size; i++)
result += values[i];
return result;
}
Even here I would be reluctant to add assertions: what would you guys add?
I disagree. The example cited is perhaps not a good one for this purpose, as the only thing that should be asserted is the set of class invariants (here, values[size-1] is a valid array element). Other methods - even very small ones - may have preconditions beyond the class invariant. A commonly cited trivial example is the pop method for a stack - which is only valid if the stack is non-empty.
The key is that assertions are not only for documentation purposes, but also to catch programming errors at run-time, in order to ensure that we get obvious errors (system can't do that) rather than subtle ones (system gives an answer that seems reasonable but is incorrect). -- RussellGold
I understand that that's the point. Where I'm not on the train is in thinking it really makes any difference.
For example, in C3, when something goes wrong analogous to popping from an empty stack (which would basically never happen in Smalltalk, of course), the system throws an exception, which is caught and a Notification is filed that the Person didn't pay. For this to work, the exception logic has to not throw an exception. This is true in Eiffel as well.
If the system is to compute an incorrect answer, it will happen because someone programmed something incorrectly, not because a pre/postcondition wasn't met. For example, the programmer may have put a value in the wrong bin. This happens because the programmer has it wrong. Even if there were a postcondition saying there'd better be a part in the bin, it would also refer to the wrong bin. I suppose you could have something like this, but it seems very unlikely:
put part into Bin DEDedSavings. postCondition: part is in Bin DEDedEarnings.I think this is what you would want, i.e. to assert the part is in the correct bin. -- PatrickLogan
But no other kind of postCondition is going to catch the error.
A case could be made that if one programmer wrote the conditions and another implemented ... but no. -- RonJeffries
A followup thought: Smalltalk programs generally fail by throwing an exception. It's rare, though certainly not unheard of, for a (well-tested) Smalltalk program to fail with a wrong answer. In ExceptionalConditions, messages are sent to the wrong object, typically nil, or an object is removed from an empty collection, or the like. Eiffel programs typically fail for the same kind of reasons, because they use contracts to create exceptions that wouldn't occur in, say, a C program.
C programs are perfectly happy to read off the end of arrays or do arithmetic on four random bytes from a string or the like. Real object languages won't do that.
This is making me think that the language level has some impact on the need for pre- and postconditions.
It's also making me want to break out the different kinds of uses of assertions, leading to something like:
I just searched across a few projects for preconditions and I found that NULL pointer checks and index boundary testing are the most common. Afterwards, we have other kinds of domain errors... you are receiving an instance and only some of its states are ones that the receiver should have to deal with. It seems to me that these cases must aways be around, the alternative, that methods should always be able to accomplish their work dealing with the full domain of the passed object's state seems extreme to me.
Exceptions are not my favorite way of dealing with errors. YouDontWantAnExceptionYouWantaTimeMachine. -- MichaelFeathers
A couple of points. RonJeffries sometimes gives the impression the code is written first and the assertions added afterwards. It should normally be the other way about: assertions first (just as for UnitTests). Assertions are part of the design process, not implementation (TheSourceCodeIsTheDesign).
Again this is part of the whole static checking thing which Smalltalkers depreciate. In Eiffel one produces pure abstract base classes whose sole purpose is to describe an interface, and such a class would carry assertions. ("Pure" not withstanding - assertions are interface, not implementation.) Assertions get inherited, so this interface class states constraints that all derived classes, all implementations, must respect. They are part of the specification.
Secondly, I want to point out that Smalltalk throwing an exception because an array bounds is out of range, is an example of checking a precondition. If you believe there should be no assertions at all, you should be using C or assembler. :-)
This leads to the question, "Do I need to state a precondition which is just the sum of the preconditions of all the routines I call (including assertions in standard libraries)?" Certainly much of the value of a good Eiffel library is that it is chock-full of assertions, and they help detect errors in the user code that invokes them, even if the user doesn't have any assertions of her own. It's like the library somehow provides free UnitTests for my stuff.
Just as a good language allows assertions to be inherited, so an environment could attempt to propagate them automatically by performing the above sum for you. With such a tool, short routines wouldn't often need explicit preconditions.
Even so, it doesn't follow that the only assertions in a project should be low-level library ones. Method implementations translate between abstraction layers, so for example, "index out of bounds" becomes "empty stack". (A stack does not have an index.) Plus higher level code adds its own, higher level constraints, eg "this array should always be twice the size of that one.". --DaveHarris
When a Relational DB is used for persistence, the quickest and best supported method of adding condition checks to support DesignByContract is enabling RelationalIntegrity checks in the schema. Even if you can't afford the overhead in production (the usual argument against it), one can run with it turned on in development and early integration testing. All the arguments in favor of DesignByContract apply to RI as well and adding such checks is FAST. -- MarkSwanson
It is mentioned above that languages like C++ and java have no support for preconditions. I'd like to assert the contrary (pardon the pun) and further suggest that Java has better support for contracts than most languages, if you recognize that the type system is implementing a special case of contracts for you for free, and that when used thoughtfully, TypesAreContracts. -- RusHeywood
A couple of thoughts.
Assertions in Eiffel are a testing mechanism. The code must be written with the assumption they will be turned off when it is run in production. I think preconditions could complement UnitTesting well. UnitTests are most effective in checking that the class behaves itself. Pre-condition assertions test that it calls methods in other classes properly too. - Tom Ayerst
Some place in WhatAreAssertions I made the statement that assertions are largely worthless without some kind of testing. Does anybody disagree? -- CurtisBartley
I do. Unless you count normal use as "testing". Or unless you don't regard AssertionsThatThrow? to be real assertions. I worked on a project that used AssertionsThatThrow? to keep a ManufacturingExecutionSystem? program running constantly twenty-four by seven. The assertions were great because they would detect that something had gone wrong and cancel the current transaction without bringing the entire sever down. Another bonus was that the Debug and Release versions of the code always took the exact same code path. I would soften the statement to say that assertions are worthless unless the code is run with them turned on. -- PhilGoodwin
From WhatAreAssertions: An assertion that is never executed tells you nothing. An assertion is only useful if the code path containing it is executed. So I don't think we disagree at all. -- CB
What if you can't UnitTest? (Because your program isn't structured as units). Assertions made a major difference to the reliability of a large BallOfMud? program that I know of. UnitTests would have been technically difficult and politically impossible (the idea of building a testing framework would have been viewed as a waste of time). One good thing about assertions is they can be added very incrementally - and then have the side effect of promoting DesignByContract as a way of working.
Unrelated point: DesignByContract seems very like the Vienna Development Method to me (a "competitor" to Z in formal programming). SystematicSoftWareDevelopmentUsingVdm? by Cliff Jones was an influential book for me, way before Eiffel and Meyer's book even existed... (I and Cliff Jones subsequently worked in the same company, but I don't think that influenced me :-) -- PaulHudson
Yes, DBC is related to VDM in that both have pre- and post-conditions, which are mathematical statements that you intend to be true on entry to and exit from the method respectively. You can use them for different purposes: (a) as documentation only, (b) to generate corresponding run-time tests, using a language such as Eiffel or one of the DBC extensions to Java, (c) to try to find bugs, using an extended static analysis tool such as ESC/Java, or (d) to create a complete correctness proof for the program, using a tool such as Perfect Developer. BTW there is an OO version of VDM now called VDM++, but unfortuately most of the documentation is currently only available in Dutch. -- DavidCrocker
I have never seen Eiffel and am not familiar with DesignByContract. My methods in Java and C++ (and even functions in C) often start with a GuardClause or two ... or three ... perhaps more. This is a sore point for me because it clutters up my code. I may have a GuardClause of some kind before I exit. How does anybody read their code when it's chock full of conditions?
Now, If I start writing my tests first, I won't write clause before exit, because I'll have confidence that I've testing those conditions. (I'm starting to see why UnitTests speed up development.) But my test suite will continue to fail unless I have those darn ugly GuardClause`s on the front end of the method.
Does DesignByContract seem to make this situation better or worse? -EricHerman
See BouncerPattern (aka "GuardClause").
Here are two important problems in the application of design by contract:
Here are three more interrelated problems:
Everyone seems to be focusing on the coding and testing aspects of the assertions, but that's a sidelight of DbC. It's called Design by Contract because it's a design technique. Specifically, the contracts explicitly delimit what is closed against changes under the OpenClosedPrinciple (which, not surprisingly, also was invented by BertrandMeyer). By implication, anything not stated in a contract is open to change.
With DbC, the only way that modifications in one routine can break a different section of code is if someone:
Designing proper contracts is challenging (to put it mildly).
DamienConway? released an implementation of DesignByContract on August 6, 2000.
--JoshuaSchachter
One of our colleagues remembers a guy from Norway who implemented a DesignByContract framework for Smalltalk, a few years ago. Can anybody point us to references? It's supposed to be on the UIUC archive, but we didn't find it there. --HaskoHeinecke and ChristianNoack?
Every Smalltalk programmer knows that (a = b) implies (a hash = b hash). Usually you learn it the hard way because that's only documented in Object's "=" method comment. The information is not repeated in "=" re-implementations in Object's subclasses. What's more, there is really no reason inherent to class Object why this is so. It only becomes meaningful when hashing classes like Bag, Set, and Dictionary are introduced. I think, such non-obvious constraints might be good candidates for contracts. (Of course, the fact that hash values should remain the same over time is recorded nowhere, too.) --HaskoHeinecke
I've recently used both DesignByContract and UnitTests on a single production project. The project currently consists of about 7,500 lines of C code (including comments), and it has some fairly harsh reliability and security requirements (it builds hierarchical, pointer-based data structures from untrusted network data, a quintessentially evil problem domain for C).
Out of the 7,500 lines of C, approximately 1,200 are UnitTests. Another 228 are assertions of one sort or another, mostly preconditions but also a few "class" invariants.
Along the way, I've noted several things:
Further update: The internal checks in this library catch more and more programmer errors as time goes on. I get about one e-mail a week from somebody who's trying to do something massively unwise, and is being frustrated by the various "contracts" in the library. I explain the right way to accomplish their goals, and everything works out OK.
One might more accurately say that we think the code, properly crafted, is the best documentation.
When asked for a largish example to see if this can be true none has ever been produced, so it remains more myth than fact. Much experience shows large projects made by a diverse group of programmers will not produce this holy grail of code.
Relying on UnitTests puts too much faith in programmers to always do the right thing. We put locks on our doors because not everyone can be trusted to do the right thing. As there is no evidence programmers are any more immune to temptation than the public at large. DBC is a way for authors to put locks into their code to make sure other people behave. Sorry if this conflicts with the ideal scenario where everyone creates and maintains great UnitTests, but the ideal is ideal for a reason. It is rare out in the state of nature.
If we cannot rely on the programmers to do the right thing, who should we rely on to oversee them? Why are programmers so susceptible to temptation (to do what?), while the authors (of what?) are immune?
No one is immune. There's is no top level where everything just works so overseeing is not an issue. Every level is built on top of humans/tools/processes of varying quality and motivation. The temptation is not to write UnitTests, not to update UnitTests, and not to write good UnitTests. As scheduling pressures increase the temptation increases. In the GoldenAgeOfMan people would alway do the right thing, but this has not been the case in my observation of many projects over many years over hundreds of developers. When DBC is made part of the class definition we do not have to rely on flawless execution in the future. We can specify how something is expected to work explicitly. How this can be considered a bad thing is mystifying. Somehow authors get complete freedom to code every step of how somethings work but they should be restricted from explicitly specifying what it means to "work."
If programmers were so perfect we'd all code in binary. It's interesting that all these people seem to have no problem with the discipline of ObjectOrientation despite the fact that that system forces programmers into 'strait jackets' too.
It seems to me that the above discussion only focuses on DBC's role in a client-supplier relationship. Just as importantly and often overlooked is the fact that contracts are inherited by descendant classes and therefore regulates their behaviour (not easily implemented in languages lacking native support for DbC). The DbC inheritance rules state that a subclass can only weaken the pre-conditions and strengthen the post-conditions of its ancestor, i.e. it can accept more (relaxing the client part of the contract) and it can promise to deliver more than its parent (strengthen its own part of the contract). Secondly, inherited contracts are a great help for ensuring that the semantics implied by the ancestor is actually preserved in descendants. -- EirikMangseth
Admittedly, I don't fully understand DesignByContract, but I think Microsoft Labs' "Vault" project at http://research.microsoft.com/vault/ makes for interesting reading in this context. (My apologies if I'm totally off-base!) If I understand the Vault documentation correctly, I think it more properly qualifies as a hyped-up type safety environment, but I can't help noticing some similar features to various DesignByContract rules through its use of 'tracked' variables. It's kind of a cumbersome means of expressing a postcondition.
Then again, I think Vault grew out of a sense of NullConsideredHarmful (see http://research.microsoft.com/~leino/papers/krml109.pdf). Either way, its syntax is pretty awful compared with EiffelLanguage, but I guess it has a sort of quaint, ObfuscatedCee feel to it.
Here's what's interesting - all of the funky directives used in Vault are evaluated at compile-time, not runtime. I don't pretend to understand EiffelLanguage very well, but I'm guessing that all of its require/ensure/invariant directives are evaluated by the environment and/or compiled code at runtime. It kinda makes Vault look like a not-quite-DesignByContract language with several drawbacks but one nifty perk.
See also: FlatShortForm, DesignByContractVsProgrammerTests, VerifiedDesignByContract
I am interested in learning more about Design By Contract: among my readings, I found older references to iContract, an extension of Java to do DBC. As of now, 2004, the site recommended above http://www.reliable-systems.com does not exist anymore.
Does anyone know what happen to iContract, or used it? Do you know of other preprocessing attempts at managing tests on preconditions, postconditions, and invariants? I heard that Java 1.4 has incorporated an "assert" command, though not something specific to preconditions, postconditions, and invariants.
Thanks for shedding some light on this if you could. -- RegineHorteur?
No idea what happened to iContract but there still is jContract from parasoft
I wonder if some actual examples of pre- and post-conditions would help understanding? It would certainly help me, and I like to think it would help others too. I am trying (for the first time) to use DbC *and* unit tests in my design/coding. It is becoming clear to me that choosing the right pre/post-conditions is as important as choosing the right classes in an OO design environment. Would I be right in assuming the bad conditions will minimise the benefits of DbC, maybe even make things worse? -- SteveMerrick
The typical example is that of a stack.
is_empty: Boolean
-- True if the stack is emptytop: Item
-- Returns the top element of the stack require: not is_empty -- We can only return the top element of the stack if the stack isn't emtpy ensure: result /= Void -- We have to return something.push (i: Item)
-- Pushes i on the stack ensure: not is_empty -- Pretty obvious, we have put something on the stack, so it can be empty top = i -- Not obvious, but also true. The top of the stack must now be ipop: Item
require: not is_empty -- Pretty obvious again, we can't get an item off the top of the stack unless it isn't empty-- NickLeaton?
One thing I see completely missing form the discussion so far is the combination of DbC with StaticAnalysis?, but in my other readings on the subject of DesignByContract, that was one of the major cases for using it. Static analysis can, in many cases, mathematically prove (or disprove) that a particular procedure will always meet its postconditions, and that it will never pass anything to another procedure that violates its preconditions. This is stronger than UnitTesting because the condition is mathematically guaranteed for all cases, not just demonstrated to be true for some boundary and representative cases.
Of course, it still might make sense to write UnitTests to ensure that the contracts mean what we think they mean, and of course, having never used DbC, I could be totally off base.
For DBC with static analysis, see VerifiedDesignByContract -- DavidCrocker
Just wondering if anyone has used Jass and DBCProxy framework. Which one is better?
--Bala Paranj
Just wondering what you think about this article http://www.codeproject.com/macro/DbC_and_Doxygen.asp, it play with DesignByContract and documentation.
Just wanted to point out how DesignByContract interacts with CommandQuerySeparation. In Eiffel, it is possible to write contracts that invoke methods that change the object being verified. This is obviously bad, but there is (sadly) no way for the compiler to prevent this.
See "A Practical Type System and Language for Reference Immutability", <http://www.pag.csail.mit.edu/~mernst/pubs/ref-immutability-oopsla2004-abstract.html>. Currently implemented for Java, but there's no reason why it couldn't be applied to any similar StaticallyTyped language.
I proposed on usenet the idea of integrating CommandQuerySeparation into DesignByContract by having a declarative syntax for commmands and queries. This way, the compiler could enforce that contract specifications only invoke queries.
Seems like any pure function could safely be used in a contract. If the language has a way to detect or denote pure functions, win.
I think the problem of specifying correct contracts is still far from being cracked: there's really very little support in today's computer languages for writing correct code. This is what I find interesting about Eiffel: it makes an attempt to help out here, but unfortunately it still doesn't prevent you from writing invalid contracts.
EditText of this page
(last edited October 23, 2013)
or FindPage with title or text search