Slashdot Mirror
Google Brings Design-By-Contract To Java
angry tapir writes "Google is developing a set of extensions for Java that should aid in better securing Java programs against buffer overflow attacks. Google has announced that it open sourced a project that its engineers were working on to add a new functionality into Java called Contracts, or Design-By-Contract. 'Contracts exist to check for programmer error, not for user error or environment failures. Any difference between execution with and without runtime contract checking (apart from performance) is by definition a bug. Contracts must never have side effects.'"
There have been several projects that have tried to do this before but the developers never saw it through. When annotations were added in JDK5 this was one of the features I've been looking for. Being able to define invariants on the interface will make implementations much more safe and consistent!
I did not realize buffer overflows were a problem for apps written in Java. Java has built-in "generic" dynamic data structures which should be suitable for 99% of the software any of us write. Why would we ever be manually managing memory in Java? Doing so should be "considered harmful" to a far greater degree than goto statements.
A slashdotter who didn't build his own computer is like a Jedi who didn't build his own lightsaber.
Actually, Google is bringing Programming by Contract to Java. Design by Contract is trademarked by Eiffel Software (and Bertrand Meyer).
It is a String-based implementation, which is awful in terms of consistency, type-checking, etc. and vulnerable in code refactoring. I would stay away or use something more type-safe and IDE-safe.
Using strings instead of compiled code is too fragile. org.apache.commons.lang.Validate or com.google.common.base.Preconditions are much better for this kind of validation.
According to Wikipedia there are already quite a few projects doing DbC:
Java, via iContract2, Contract4J, jContractor, Jcontract, C4J, CodePro Analytix, STclass, Jass preprocessor, OVal with AspectJ, Java Modeling Language (JML), SpringContracts for the Spring framework, or Modern Jass, Custos using AspectJ,JavaDbC using AspectJ, JavaTESK using extension of Java.
Do we really need an entirely new one? If none of those are sufficient, why not build on top of and improve an existing project? Starting over is not always a good thing...
D has had contracts since the get-go. Sometimes I wonder if it would be a better world if all the C and C++ out there was *magically* reimplemented into a better language.
Like all pain, suffering is a signal that something isn't right
There's a subset of Ada called SPARK that has these concepts.
SPARK (Programming Language)
I'm still waiting for a decent compile time DbC. Runtime checks won't catch an untested control flow, and when the fault does happen you better hope it happens in your lab and not on a client's computer. You can read my analysis of this in my Master's thesis (which focused on unique references that were ensured to be unique at compile time):
http://www.worldcat.org/title/applying-uniqueness-to-the-java-language/oclc/701244184&referer=brief_results
Isn't throwing an error a side-effect?
No, because it does not mutate a value, but only changes the control flow.
I wish I had more time to explain in detail, but that isn't going to happen today, unfortunately. Side-effect in this context is a highly specific term that means, essentially, to change the value of a variable through assignment.
Put my fist through my alarm clock with its ding-dong death inside my ear. - The Blackjacks.
The idea of contracts is that clients write their code to work with anything which fulfills the contract. So let's say you have some client code written, but then determine that there's a bug in the contract. What does this mean? The client code is either written for the "buggy" contract, or the client code was ALSO buggy and written for the intended contract. At that point, it seems that the client has failed to grasp what the contract is in the first place. The idea is that the contract cannot be buggy, since it is the definition of correct. If your clients code to the contract, you can't go changing it without breaking clients. The contract may be badly-designed, and it's good to avoid bad designs, but once you have clients, to go in and try to fix a "buggy" contract is to water down what contracts mean in the first place. It encourages clients to ignore contracts and code to what they imagine the routine should do. At that point, you might as well abandon contracts because they aren't being used as the definition of what is correct anymore, just a vague guide as to what the routine might do.
One of the best ones was the DEC Extended Static Checker for Java in the late 1990s. That project died after Compaq acquired DEC and shut down research. But it formed part of Microsoft's efforts for Spec#, which has a formal verification system.
Microsoft has had a huge success with formal proof of correctness - the Static Driver Verifier. This is a system which tries to formally prove that a Windows driver can't crash the operating system. All drivers for Windows 7 have to pass this verifier to be signed, It's an impressive system which works by symbolic case analysis. It yields a proof, a counterexample, or times out analyzing too many cases. About 3% of programs time out. (If your kernel driver has undecidable behavior, it needs work.)
I headed a team that did a proof of correctness system for Pascal back in the early 1980s. That was pushing the limits of what you could do back then; verifying a small program took 45 minutes on a 1 MIPS VAX. Today, with about four orders of magnitude more CPU power, it's a practical technology.
There have been many attempts to bolt some "design by contract" features onto various languages, but they're usually not very good. The problem is saying things about collections. The hacks that try to do design by contract at run time tend to avoid expressions which examine big data structures, since they have to run them over the whole data structure every time. Real verifiers prove or disprove such things at compile time. It turns out, though, that a few standard cases for collections cover many of the usual things you want to say.
Another big issue, which Spec# handles and this Google hack apparently doesn't, is the "insideness" issue for object invariants. Object invariants are supposed to be true whenever control enters and exits an object. But what if an object calls one of its own public methods, perhaps through a long chain of calls? Now, control is inside the same object twice. That violates the invariant rule.
This class of bugs is common in window systems, where all the widget, pane, window, and event objects are frantically calling each other. It also comes up in concurrency, which I don't see Google's hack addressing either.
Actually Design by Contract is a design discipline, not a bunch of error checks. It's a bit like programming without gotos: the benefit comes not from avoiding typing "goto" into your source code, but rather from the style of reasoning you use when you learn the proper alternatives.
Patrick Doyle
I mod down every jackass who puts his moderation policy in his sig. Oh, wait a sec....
Or you could use the .Net Code Contracts which do all this with static analysis. Therefore you get proof up front that your contracts will never be violated by non exposed code, and without a performance penalty at run time. If a contract cannot be verified, warnings are given. You can then introduce appropriate branching to provide guarantees as necessary. http://research.microsoft.com/en-us/projects/contracts/