Home » forums » LtU Forum

Design By Contract in C

I just returned from a nice relaxing weekend of no-computers and found, upon return, this nice article on dbc in c.

http://www.onlamp.com/pub/a/onlamp/2004/10/28/design_by_contract_in_c.html

It's not too long, and i found it a good read, so i decided to share it.

I guess the keywords are: Ruby, C, DSL, Design By Contract

By Jillis ter Hove at 2004-10-31 16:05 | LtU Forum | previous forum topic | next forum topic | other blogs | 8064 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Just playing devil's advocate here

In thinking through DbC, I have a couple of concerns that I'd like to clear up.

1). Static contract checking: As near as I can tell, DbC provides a formal (or informal) mechanism for checking Pre, Post and Invariant conditions. Yet, the checks are not intended for the consumption by the compiler. They are simply run-time checks that test the assumptions of the values and conditions which are verfied during the test phase of software development.

2). Test phase only: Most DbC schemes seem to believe that checks are something you will want to disable once the code is moved to production. They are not aimed at checking for post test phase enforcement of the contracts. For one thing, a production environment usually doesn't like to have the program halt just because a condition is not met. For another, no monitoring mechanism seems to be the default - that is, shouldn't someone receive a notification that a contract has failed, even if the program carries on during the production phase

3). Redundant with TDD: Unit tests seem to be the manner that most shops are moving in verifying code. DbC is usually more restrictive than TDD because it focuses on the specific method or object, rather than the interaction of the system as a whole. That is, DbC is much more narrowly focused in testing a range of possible values rather than whether a specific value yields the desired results when the system as a whole is factored in. The question is whether DbC adds value to TDD as whole, or is it just an overlapping of functionality. Perhaps it prevents you doing something stupid, but it no more acts as a guarantee of correct results than does TDD.

Anyhow, just a couple of thoughts. :-)

By Chris Rathman at Sun, 2004-10-31 21:00 | login or register to post comments

I don't know

Concerning point 2:
I could certainly envisage a dbc implementation that could be integrated with the run time system. What about a ContractFailedException. Unfortunatly c doesn't have all these nifty features..

Point 3:
Valid! Because of this i actually see dbc as a 'little language' for TDD, it automates a lot of the common tasks of tdd and the added clarity coming from the consistency of the notation is beneficial as well.

That you are able to leave them out of a compile is good imho because some people just want ( and need ) speed. This is something a compiler should facilitate in.

By Jillis ter Hove at Mon, 2004-11-01 14:13 | login or register to post comments

Design vs. Verification

A nitpick: It is called design by contract, not verification by contract. A large reason for using DbC lies in its applicability as a design mechanism: The clear assignments of rights and responsibilities to clients and suppliers and documenting them in the interface of a class. Note, for instance, that preconditions, postconditions, and invariants can and sometimes are provided as comments when they cannot be adequately expressed in code.

Regardless of this, verifying that a system satisfies the specified contracts is of course interesting and important for actual use; but how one attempts to verify adherence to contracts, whether by testing or theorem proving -- cf. the Larch system, for instance -- or something else, is largely orthogonal to the other benefits.

By Reimer Behrends at Mon, 2004-11-01 22:15 | login or register to post comments

Static DbC is typechecking, Unit tests are black-box

1) Isn't static DbC just type checking? A type system with dependent types might be able to provide the same level of functionality as DbC, but it's harder to program with (since you're essentially constructing a proof). DbC is easier because you use plain-old turing-complete code to verify a concrete piece of data.

3) It may be partially redundant, but DbC allows white-box testing. You can assert invariants on the internal data structures, which may make some things easier to test for. I don't know if you'll catch many more bugs, but errors will probably be easier to pinpoint. I suppose unit tests could be allowed to break encapsulation barriers, but I don't think this is common practice.

Another difference is that DbC seems to have a lower barrier to entry. It's easier to check a couple of field relationships in each method than write a unit test. And while DbC is not truely declarative (like static type checking is), it's sort of declarative in that tests are separated into preconditions, postconditions and invariants. This serves as a form of documentation and is easier to read and understand than a unit test is.

By Kannan Goundan at Tue, 2004-11-02 21:30 | login or register to post comments

Using contrived examples

Off-topic, but somewhat funny.

[...], and more coding introduces the possibility of more errors. A statement such as

assert(size >= 0 && size = MAX_BUFFER_SIZE);

is valid C code, but obviously it does not produce the desired effect.

No, but the "obvious" bugfix, size == MAX_BUFFER_SIZE, would?

By ahe at Fri, 2004-11-05 08:17 | login or register to post comments

Different obvious

No, but the "obvious" bugfix, size == MAX_BUFFER_SIZE, would?

Wouldn't the obvious fix be "size

By Marc Hamann at Fri, 2004-11-05 15:29 | login or register to post comments