OnLAMP features a new article on how to use a simple implementation of DBC with C code. If you ever wanted to know what designing by contract is, and why C’s assert is not enough read this.
Design By Contract for C
About The Author
Eugenia Loli
Ex-programmer, ex-editor in chief at OSNews.com, now a visual artist/filmmaker.
Follow me on Twitter @EugeniaLoli
I would love to see more articles on forms of code proving — both informal (like DBC), and formal proof systems.
This was well-written, excellent article. I ‘knew’ design by contract was a Good Thing, but hadn’t really seen it in action before. Now I know it’s a Good Thing as well as non-invasive. Of course, I’m always happy to see someone using my current favorite language, Ruby, for real work.
Should give Eiffel or D a try. This is a really nice hack, but it remais that. DbC remains more powerful in languages that embrace it, especially when those languages make object-oriented programming possible and have contracts which get inherited.
Some time ago I played a bit with some macros to allow design by contract in Objective-C … here is the page : http://www.roard.com/contracts/ if somebody is interested.
1) ‘sparse’ is a tool aimed at checking linux kernel source code:
http://www.linuxjournal.com/article.php?sid=7272
2) SPIN is an open source model checker (protocol verification, etc.). The tool was awarded the prestigious System Software Award by the ACM. There is lots of documatation on the internet. Newer versions also feature model extraction from C code (modex).
http://spinroot.com/spin/whatispin.html
this is indeed very funky. I have downloaded it and will peruse it on the morrow.
Design by Contract, checking the robustness of your code and pre and post-conditions is obviously nothing new but it was interesting to see it applied to C.
But, to really make this work you need object-oriented features and ideally a tool to completely automate all this for you and integrate it with your design specs. Doing this manually, even with a simple tool, is something you don’t really want to get into for a sizeable system, especially with changing requirements.
Doing this manually, even with a simple tool, is something you don’t really want to get into for a sizeable system, especially with changing requirements.
No doubt there are those who would say that this is precisely the kind of system this mechanism should be used for.
***
Nice article. I’m not sure I like all these safety nets though. It’ll be a dull world if programmers can’t royally screw up a system through bad programming (Or am I the only one who enjoys debugging?).
indeed. very interesting.
That’s something I really could use in my projects.
Thank you very much Eugenia 🙂 ;-*
No doubt there are those who would say that this is precisely the kind of system this mechanism should be used for.
Errr…..
The Design by Contract system is as old as the hills. Worryingly, you would have thought it was common sense by now, but I never cease to be surprised. In a large system however, you need good, higher level tools to be able to manage it effectively. The system itself isn’t good enough.
Nice article.
Eiffel compiles to intermediate C code, and cooperates very well with C code, so it would be worth the effort simply to convert to coding with Eiffel, writing bindings (? right word?) to cooperate with your C code, than to try to implement DbC in C.
Eiffel’s a beautiful language. Try taking a look at it, either ISE Eiffel (Meyer’s version) or SmartEiffel (a really nice free version).
http://www.eiffel.com/
http://smarteiffel.loria.fr/
A nice hack for DBC in C, but now I am more intrigued than ever to look into Eiffel!
Ya know, every year since I learnt Eiffel I’ve gone looking for some nice big apps written in Eiffel to demonstrate why Eiffel is good and should be used to production systems. Unfortunately the only “large” apps I have ever found written in Eiffel are either tools for developing Eiffel or libraries that have had Eiffel bindings written for them. Where are all the good Eiffel apps? There must be some out there. It’s easier to believe the language isn’t being used at all than it is to believe the language is only being used in proprietary code. Where are the open source Eiffel apps?
It’s not that hard to believe Eiffel is being mainly used in proprietary code. Outside of the academic environments that spawned SmallEiffel (which became SmartEiffel), and which usually pushed another language later in their CS courses, Eiffel’s largely been the domain of those with a lot of money to invest.
Eiffel lends itself to large projects, and the commercial compiler packages can be very expensive to license. Until recently, SmartEiffel has not been of sufficient quality to get many people to look into it. It may not yet have completely reached that stage, especially as the language is approaching a standard and the standard may include many features SmartEiffel does not.
Open-source projects tend to be smaller, and generally there isn’t the funding to spend thousands of dollars on a compiler license. SmartEiffel is an option, but even if it’s technically suitable, the lack of a standard to code to currently, the lack of marketing, and the cultural inertia saying Eiffel isn’t easy or useful is fighting against it.
well, I can think of the Arachno-* family of IDEs (ATM the only thing available is the free beta of the ruby IDE, but they plan to support perl, python and php).
The system is written in (Small/Smart)Eiffel, and indeed seems quite cool (even if the fox toolkit is not one of my favourite).
It’s easier to believe the language isn’t being used at all than it is to believe the language is only being used in proprietary code. Where are the open source Eiffel apps?
My project isn’t what most people would call “big”, but I wrote system to test a conjecture of mine. Without it, I wouldn’t be graduating.
One of the nice things about Eiffel’s implementation of DbC is that the code documents itself. As I recall, in Java you have to add special documentation for javadoc & similarly for others, but with Eiffel the requirements come straight out from the listed preconditions and postconditions.
See for example
http://smarteiffel.loria.fr/libraries/array.html
http://www4.ncsu.edu/~jeperry/eiffeldocs/monomial.html
Oops. Part of the point of that was: One of Meyer’s goals with Eiffel was to design a language where the design, documentation, and programming were all done at once. You specify your preconditions & postconditions & so on (require & ensure clauses) and during development the usual compiled code will check itself. I’ve found this to be an immense aid to debugging.
When it’s time to finalize code, however, you compile with the -boost option and all those checks are taken out for performance reasons, much like removing stack checking from Pascal or Modula-2 code. But the documentation of contracts remains; it’s part of the source code, part of the documentation generated by Eiffel tools, part of what anyone looking at the code would naturally see. They don’t have to look lines of code for the comment. Just as Pascal (& Algol?) forces all variable declarations to occur at the beginning of the code so you didn’t have to hunt for them to modify it, Eiffel forces all requirements & guarantees to be listed in a specific place, so you don’t have to hunt for them to modify it.
The bonus is that with one simple switch in the standard language specification, you can turn checks on or off, keeping the documentation. If I remember this article precisely, that’s a pretty nice feature of his Ruby & perl scripts, too.
We will have the formal methods to verify the contracts at compile time instead of run-time. Unit testing is never exhaustive.
well, I guess you jst need to find a nice alghoritm for checking dependent types
Nice to hear the positive feed back.
DBC for C is being actively developed and I just set up a mailing list (got about 3 people on it at the moment).
Here is the wiki:
http://dbc.rubyforge.org/wiki/wiki.pl
and the project page is here (click on lists tab for mailing list info):
http://rubyforge.org/projects/dbc
-Charlie