* Open specifications * validation and verification of all equipment and procedures concerning the vote
In practice, this means the voting hardware and software must be open to public inspection. The same goes for the procedures used by voting officials. I would go even further and demand that both an English language and a formal specification that are open. That way you can validate the formal speciifcation against the English language version, and you can formally verify software code against the formal specification. There are plenty of independent systems that would allow such formal verification of code to be done, and machine checked. Sure, this requires more work to write a formal specification and to write code that can be verified against it... but if there was any case where you would want to be able to do full machine assisted verification of code against a specification rather than just eyeballing it and hoping you catch the errors, electronic voting would be it!
Slowly, but surely, security of software is becoming more if an issue. That doesn't mean writing perfectly secure software -- but it does mean closing up some of the glaring holes. As this article points out, a ridiculously large amount of security flaws in web applications come down to failing to do very basic things like failing to do adequate input validation/filtering, which leaves you open to SQL injection, XSS attacks and all manner of other nastiness. Expecting perfect code for simple things like web apps is unreasonable. On the other hand, if we can educate more programmers on basic techniques for handling these very common sorts of errors then things will undoubtedly improve significantly on the security front. Ultimately we are moving toward software assurance, where developers provide certain assurances about their software to let clients know what they can expect. It's not a matter of assuring perfection, it's being able to state clearly what aspects you can be confident of. Being able to say that all user input gets filtered through specific validation and filtering function, for instance, is an example of assurance. That doesn't mean the filtering function is perfect, but guaranteeing that all input goes through it is a start - if you want to provide assurance of stronger security then you might provide assurances as to what types of attacks the filtering function will prevent, and so on. As security becomes more important, providing such assurance offers in contracts will be increasiongly valuable.
I should add that these fossil discoveries lead to various people taking a more serious look at the presumed facts of mammal evolution and were the catalyst for a "rethink", however there is even more "hard evidence" in the paper cited by the NYT article which was a far more detailed study looking at far more fossil (and apparently molecular) evidence.
Does it raise questions in no one else's mind when it is quite consistently being "rethought?" It seems it should not be dogmatically asserted as it is now, nor should a "rethinking" be taken in stride as if it's entirely normal behavior for science. And yes, I know it's not a scientific fact, it is a scientific theory, as most scientific thoughts are - but most school kids don't know much of the difference between "fact" and "scientific theory." It's simply taught...Maybe informative materials should be re-evaluated when the theory itself is re-evaluated. I think we should be clear on what is being re-thought here. The theory of evolution itself, that variation and descent, combined with selective pressure, will lead to complex organisms with the appearance of design, is not being rethought. The theory that evolution via natural selection is responsible for the diversity of species of life on earth is not being rethought. All that is being rethought is the particular history regarding the evolution of mammals. That the theory of evolution can be used to explain this particular history, but there are unknown factors in the specifics of the history, so the particular explanation provided as the most likely by evolutionary theory may change as particular facts regarding the particular history of a particular line of organisms changes. Let's consider an analogy: the theory of gravity is a relatively well accepted theory. It can be used to provide an explanation for the history of the development of solar systems, and has been used as a basis for developing a theory as to how our particular solar system developed. As it happens, that particular history is being rethought, as we don't know all the facts about the particular history of our particular solar system. As the available facts regarding the particular history of a particular solar system (ours) have changed, the explanation of that particular theory furnished by the theory of gravity has changed. You have no more reason to think that "informative materials regarding the theory" of gravity should be re-evaluated than you do with regard to "informative materials regarding the theory" of evolution.
Until the next "re-thinking." Will we ever have hard evidence, or just thought experiments? But we do have hard evidence - indeed it was hard evidence that helped lead to this rethinking. Recently there have been a number of finds of surprisingly large mammals that are much older than had previously been expected. They include a beaver like (pre)-mammal from the Jurassic that was almost half a metre long, discovered in 2004, and two species large carnivorous mammal from the cretaceous (dated to about 130 million years ago - or 65 million years prior to the dinosaur extenction) which were discovered in 2000 and 2005. Such large mammals (relatively speaking) during the time of the dinosaurs draws into question the previous belief that mammals were restricted to small rat/mouse like scavengers at that time. Instead we see evidence of large, active, meat eating mammals. This implies that mammals were rather less marginalised during the dinosaurs "reign" than previously thought, and imples that mammal evolutionary history needs to be rethought accordingly.
Also, what about a professor with a PhD in one field posting inaccurate information in another, closely related, field. The professor may honestly believe his information is correct, but that doesn't make it so. In this case, the incorrect information will stay on the Wiki until someone with more relevant credentials can successfully argue against it. This can and does happen. A good example of this is the case of Carl Hewitt, a Computer Science professor at MIT and (co-)creator of the Actor Model as a formalism for concurrency. The problem was that Hewitt was very fond of his own and his students ideas, and this spilled over into his editing, with extreme boosterism for the Actor model approach spilling over into pages about other formalisms (such as CSP, CCS, and others) with (dubious) criticisms of the other formalisms added to those pages. Worse, there was a huge proliferation of new pages created by Hewitt, again ostensibly as boosterism for his and his students work, that spilled well outside the area in which Hewitt was well acquainted, including speculations on applying the Actor model to develop new/different/better theories of Quantum physics and General Relativity. In the end the case went to the Arbitation Comittee (case archived here, the evidence section is worth reading too). The user CarlHewitt (who was identified as being the same MIT professor) was banned from any autobiographical editing and put on probation regarding any editing related to his own work.
Had a system been in place where highly credentialed people who had been verified had the final say then Hewitt's edits would have gone unchecked - Professor Hewitt is extremely well credentialed, and very notable within the CS field; no-one complaining was anywhere near Hewitt's standing. Before you side with Hewitt on the presumption that, since he is better credentialed than those who opposed his edits, take some time to read the evidence from the ArbCom hearing. It doesn't take much to see that Hewitt was clearly overstepping the bounds.
Most of those species simply weren't important to us and we found alternatives for those that were. We'll do the same thing in the future. Life on earth is about change and adaptation. That is what drives evolution and life itself. The earth is a big place and has been around a long time. It will be here long after you and I are dead. Indeed, replacements will be found, or new ways of life will be adapted to. We, and life, will change to suit the conditions. That doesn't mean change will be easy. The people of Easter Island survived by adapting their way of life after they ran out of trees. Of course that involved a period of significant turmoil and civil war due to overpopulation before new ways to live and suitable new population levels were found. The fact that we can adapt and change to new situations doesn't mean that the period of adaptation will be pleasant, or indeed, something we wouldn't wish to avoid if we could. Aiming to have amore sustainable approach is not about avoiding a life destroying catastrophe (though that is a very remote possibility) so much as trying to smooth over the unpleasant and painful periods of adjustment that can occur when we are forced to rapidly adapt to new situation. You may not care about the lack of cod stocks, but I assure you that anyone living in New Foundland does - their lifestyle took a very significant hit, and the province is still trying to adapt and find ways to generate income other than fishing. If we can look ahead and see such potential problems on the horizon then doesn't it make sense to do what we can to minimize the impact by using the resources more sustainably? It doesn't have to be an epic disaster looming to make such an approach sensible - the impact may be small on the grand scale, but present significant economic hardship on the scale of individual human lives, and it would still be worth avoiding if we can.
I said we have never run out of anything important and I stand by that statement. When one resource dries up we move to the next. I think the OP was merely trying to point out that, while we might get away with that approach, it doesn't mean it is a good one. There is often (though not always) a certain amount of discontinuity between one resource being effectively depleted and something else becoming sufficiently prevalent to fully replace what we depleted. In the grand scheme such discontinuities are just blips - but on the scale on individual human lives those periods can involve considerable hardship. If we can avoid that sort of thing by using a little foresight and trying to make use of our existing resources in a more sustainable manner then we can smooth over the doscontinuities and save ourselves potential hardship - are you suggesting that doing so is necessarily a bad idea?
And they said I was stupid to invest in all this uranium when it was cheap! Now, if I could just stop coughing up blood long enough to take some photos for eBay, I'll be set for life... Look on the upside, even if you don't manage to take any photos for eBay it will be because you're already set for (the brief) rest of your life! As the saying goes, light a man a fire and you warm him for a night, but light a man on fire and you warm him for the rest of his life.
From the perspective of a FOSS desktop, if vendors (say Red Hat) can't distribute a derivative of Qt, then that qualifies as "proprietary hold." The ability to distribute derivatives is hardly useful only a "small handful of zealots." The QPL was just not viable for a free desktop, and, from a licensing perspective, there was still a place for GNOME even in 1998. Indeed, from a licensing perspective, there is a place for GNOME right now, since GTK+ is LGPL: there is a reason that things like Mozilla, OpenOffice, SWT, etc. use GTK+ rather than QT. Yes, the whole GPL v LGPL issue for the GUI toolkit is, for many many people, a minor point that makes no difference. There are people for whom the difference matters, however, and as long as the difference in licensing exists there will continue to be a licensing niche that GNOME successgully occupies.
The only real 'stigma' against SciFi/Fantasy is that it's expensive. That doesn't have to be the case at all - there are some great SF films that have been done on remarkably small budgets. Try Pi or The Sticky Fingers of Time, both intelligent interesting science fiction done very cheaply. SF is only as expensive as you choose to make it. The real difference between the films you mention, Dark City and Memento, was the visual style - and it was the particular rich visual style of Dark City that made it expensive.
The other issue is comparability of the systems. There's quite a difference between RHEL and Windows in terms of what gets patches released for it: RHEL includes everything from OpenOffice.org, to databases, scripting languages, a whole suite of development tools and IDEs (including a host of libraries), raster and vector paint programs, and lord knows what else. A problem with any of those packages will get a patch, and if it is an unimportant or rarely used package it may take a while. Windows, on the other hand, was presumably only having patches directly against the standard install counted against it, while problems with MS Office, SQLServer, VisualStudio, etc. were not. Indeed, many packages in RHEL are available for, and widely used on, Windows. If Firefox or Thunderbird or Perl or Python have a vulnerability then it is as much a problem for Windows as for RHEL. I doubt it gets counted that way however.
SCOOP, like all concurrent programming models, has all kinds of unexpected non-intuitive quirks. It's not easier than single-threaded programming. Who said anything about easier? I was commenting with regard to not significantly harder. Sure there are quirks, just like there are quirks to using garbage collection, or OO design. It isn't that much to learn, however, and it is a damn sight easier than trying to do threading with hand coded mutex locks.
Unfortunately I think many programmers that read Slashdot are scared off by the clear, readable, maintainable syntax. Typing end is clearly too much work, or something, and as we all know IDEs can't possibly help with that... I would like to see Ada get more use, but unfortunately I doubt it is going to happen.
Well, if you're going to remove 99+% of the common trouble spots of multi-threaded coding by moving to a messaging paradigm, then yes, it probably is conceptually easier than OO. It can also be significantly slower depending upon the application's design and function and greatly increase its memory footprint. e.g., I don't think a game like Quake would work all that well under this paradigm. I think it is nowhere near as bad as you seem to think - it all depends on how message passing is handled. If you're doing via some slow complex scheme then, sure, it will be slow. But the trick is to think conceptually in terms of message passing - that doesn't mean it actually has to be handled with a big clunky message passing interface internally; just in terms of how you think about it. Take SCOOP for instance. The "message passing" mechanism there is feature calls, the message being parameters passed to the feature/method. The preprocessor and compiler handles all the messy details of locking etc. and in practice it runs about as fast as hand written threading. The difference is that you think in the simpler terms of actors and messages, while the computer (in this case the compiler) handles the grunt work of converting that into efficient code. This is no different than OO, or garbage collection, of course: you simplify what you need to write by writing in a higher level paradigm and leave the hard work of turning that into efficient machine code to the compiler.
You'll also still have the potential of concurrent modifications in this scenario, but at least you won't be working on the same memory storage locations, potentially reading indeterminate/incoherent values. Instead you'll have inconsistent values displayed, depending upon which thread's data you're displaying. Read the page on SCOOP, or this draft paper, to see what it actually does - it is well worth it: it's the best mix of OO and concurrent programming I've ever seen. You won't end up with inconsistent values because everything will block accordingly with the compiler handling all the necessary locking/blocking/waiting and letting you get on with just writing code.
Writing good code is harder, designing good OO code is even harder, and designing and writing good multi-threaded code is yet a step beyond that. In theory writing good multi-threaded code shouldn't be much harder than designing good OO code - it's a matter of actually learning the right paradigm to think about things, and then it all flows easily (presuming you've got a language that supports your paradaigm well - otherwise it is doable, but a little clunky, much like OO). If you're willing to let go of shared state concurrency and think in terms of message passing then things get much easier. Think of actors passing messages and try writing multi-threaded code in Erlang. You'll find it is surprisingly easy to do well. If tht's too much trouble then try SCOOP for Eiffel which attempts to convert the OO model into a message passing model (which in some sense it was originally intended to be). In that case designing to multi-threaded code is hardly different than designing good OO code - just decalre which objects are allowed to be handled by in parallel and let the compiler do all the work of sorting everything out.
usually meticulously position windows every login (because windows never remember regardless of the settings you choose) to have these all set up at the proper viewing, but having to fiddle with a 2-line deep taskbar to bring up the right ones for the task I want to do at the moment can be frustrating. Obviously you haven't played with virtual desktops and such, so I'll give you an idea of the sort of thing that many people do. You can divide up your windows over several different desktops, usually according to task or some such. That means to switch tasks you just switch desktops. This has the added bonus that if you have a bunch of windows all carefully positioned for a given task then, by switching to that desktop, you go from dealing with none of them to having just those windows visible, and all positioned appropriately - a lot better than picking through a taskbar and raising the 3 or 4 windows you need each in turn. Virtual desktops also help clean up your taskbar since you can set the taskbar to only show windows on the current desktop, thus you don't get buried with a 2-line deep taskbar. Throw in a window selector applet (a single button on the taskbar that pulls up a menu of all windows, grouped by which desktop their on) so you can go straight to any window from any desktop and things start to look much more manageable.
What other Sun tech are they licensing? I don't know about licensing, so much as just using since it is open source now, but Leopard apparently has DTrace and Apple is providing a GUI tool to visualise data from DTrace instrmented code called Xray (scroll down to find info on XRay).
Don't want null to be passed into a function? Make a unit test to make sure it doesn't happen. Heh. I'd be interested to see that "unit" test, since you'll essentially need to be checking that all code that calls that function can't result in the parameter passed being null - you'll be testing every unit that calls that code, and you won't cover all possible code paths, just the few you happen to test. But worse is that you're exporting the problems with one unit (that you want to have a non-null parameter) to everything else. What happens if you write another unit that also happens to call that code? You'll have to remember to write an extra unit test for the new unit to ensure if won't pass in a null value. It makes much more sense to localise the checking with a single contract on the function that will flag an error if a null ever gets passed - you're writing the "test" once, and it is directly associated with the point where the problem will occur.
I think your example mostly shows how little you know about DbC systems. For example, code those contracts in Eiffel and run ES-Verify over it and it will happily inform you that the contracts on g and h cannot be guaranteed. Likewise code it in Java with JML and run ESC/Java2 over it and it will tell you the contracts on g and h cannot be satisfied, and it will even be kind enough to explain why. Fix the precondition on f to specify that that you also require a > 0 and b > 5 and all of a sudden it will verify in both systems. Which is to say that, in fact, DbC systems will let you catch precisely the sort of error you give as an example.
Even if you don't use verifiers then the problem will likely be found in testing (rather than production), and given the contract violation and the call stack you can quickly see that f will require further constraints for the pre-conditon. Running again the problem will naturally bubble up through anymore call layers if you have something calling f unsafely.
Contrary to your claims DbC is far better at catching errors such as you suggest, and is clearly going to be a vast improvement over no contracts at all.
At least this should up the effect of sunspot activity (if there are any satellites that are in service for over 20 years). Indeed, sunspot activity is well tracked since the 1800s so we have a pretty good record. You can plot the teperature record, CO2 data, and sunspot activity together. It seems clear enough that sunspot activity has some effect of temperature, so the OP is right in the sense that global warming is not "entirely out fault", but the upswing in temperature, particularly over the last 50 years or so, is far more reasonably attributed to CO2 increases. We may not be "entirely" responsible, but it seems we should accept a big chunk of the blame.
I think you're missing the point of contracts. It isn't to tell you what the function does when you write it (though stating your intentions doesn't hurt to clarify your thoughts), it is to tell other people what the function does, and to tell yourself in a years time. Contracts go in the documentation so you can read them instead of having to fish through code. More importantly, for functions less trivial than the one you happened to specify, contracts can and do describe functionality and requirements far more succinctly than implementation code does. I can tell you what contracts a sort function must meet much more easily than I can explain the details of a particular sorting implementation. All you're doing is saying "here is a really simple example for which the implementation is as short as the contract, therefore contracts are always useless" which is nonsense. I can write a function for which the type signature is essentially the same as the implementation, that doesn't mean static typing is of no value. Degenerate cases don't prove ineffectiveness in general.
Secondly, in real systems that much of the code just doesn't lend it self to being described by pre/post conditions.... Subscriptions.get_expired()... Seems pretty straightforward, get me a collection of expired Subscriptions...What kind of Contract would I use....
pre-conditions: Are there none? post-conditions: All returned subscriptions are expired.....hmmm seems to be stating the obvious.... It seems simple enough to me. Presuming you don't already have an invariant to cover it you might end up with
require
has_subscriptions: Current/= Void and subscription_array.size > 0 do
deferred ensure
results_are_expired: Result.for_all(agent(subscr : SUBSCRIPTION) do Result:= subscr.expired end)
all_expired_in_results: not subscription_array.exists(agent(subscr : SUBSCRIPTION) do Result:= subscr.expired and not Result.has(subscr) end) end
But perhaps some of the Eiffel idioms are not helping there, so how about in JML for Java
Or something similar (it depends on the implementation as to the exact details of course). This isn't redundant information from a maintenance, refactoring, or API documentation standpoint. Perhaps because the example is simple it doesn't appear that useful, but as soon as you get much more complicated...
Just because you're interested I'll do a little boosterism for the Java DbC system because it is actually pretty cool. First I'll admit the downside: it works by embedding annotations for contracts in comments (like JavaDoc comments basically) which makes it a little bit hacked on, but you take what you can get. The upsides include: good tool support, so not only do you get a compiler that converts annotations into runtime checks, but a version of JavaDoc that incorporates annotations into the auto-generated API documentation, and a tool that can read the contract annotations and generate a corresponding JUnit class, along with automated data generation schemes (to which you can add if you wish). If you throw in ESC/Java2 which does static checking of the contracts and can catch a lot of subtle errors statically, and Daikon which exercises your code and tries to statistically infer likely invariant properties (spitting out results in form that can be added directly as annotations), and Eclipse plugins and the whole thing starts to look quite nice. Here's a journal entry I made on the subject.
I love Quicksilver on the Mac and would love Linux even more if I had QS there as well. It sounds like Deskbar is not a bad alternative to Quicksilver - it seems to offer the same sort of functionality. Having never used QS I can't comment on how they compare, but I can say that Deskbar is very powerful and well worth having, and would certainly make things nicer on Linux if you're a QS addict.
Slashdot Mirror
* validation and verification of all equipment and procedures concerning the vote
In practice, this means the voting hardware and software must be open to public inspection. The same goes for the procedures used by voting officials. I would go even further and demand that both an English language and a formal specification that are open. That way you can validate the formal speciifcation against the English language version, and you can formally verify software code against the formal specification. There are plenty of independent systems that would allow such formal verification of code to be done, and machine checked. Sure, this requires more work to write a formal specification and to write code that can be verified against it... but if there was any case where you would want to be able to do full machine assisted verification of code against a specification rather than just eyeballing it and hoping you catch the errors, electronic voting would be it!
Slowly, but surely, security of software is becoming more if an issue. That doesn't mean writing perfectly secure software -- but it does mean closing up some of the glaring holes. As this article points out, a ridiculously large amount of security flaws in web applications come down to failing to do very basic things like failing to do adequate input validation/filtering, which leaves you open to SQL injection, XSS attacks and all manner of other nastiness. Expecting perfect code for simple things like web apps is unreasonable. On the other hand, if we can educate more programmers on basic techniques for handling these very common sorts of errors then things will undoubtedly improve significantly on the security front. Ultimately we are moving toward software assurance, where developers provide certain assurances about their software to let clients know what they can expect. It's not a matter of assuring perfection, it's being able to state clearly what aspects you can be confident of. Being able to say that all user input gets filtered through specific validation and filtering function, for instance, is an example of assurance. That doesn't mean the filtering function is perfect, but guaranteeing that all input goes through it is a start - if you want to provide assurance of stronger security then you might provide assurances as to what types of attacks the filtering function will prevent, and so on. As security becomes more important, providing such assurance offers in contracts will be increasiongly valuable.
I should add that these fossil discoveries lead to various people taking a more serious look at the presumed facts of mammal evolution and were the catalyst for a "rethink", however there is even more "hard evidence" in the paper cited by the NYT article which was a far more detailed study looking at far more fossil (and apparently molecular) evidence.
Had a system been in place where highly credentialed people who had been verified had the final say then Hewitt's edits would have gone unchecked - Professor Hewitt is extremely well credentialed, and very notable within the CS field; no-one complaining was anywhere near Hewitt's standing. Before you side with Hewitt on the presumption that, since he is better credentialed than those who opposed his edits, take some time to read the evidence from the ArbCom hearing. It doesn't take much to see that Hewitt was clearly overstepping the bounds.
The other issue is comparability of the systems. There's quite a difference between RHEL and Windows in terms of what gets patches released for it: RHEL includes everything from OpenOffice.org, to databases, scripting languages, a whole suite of development tools and IDEs (including a host of libraries), raster and vector paint programs, and lord knows what else. A problem with any of those packages will get a patch, and if it is an unimportant or rarely used package it may take a while. Windows, on the other hand, was presumably only having patches directly against the standard install counted against it, while problems with MS Office, SQLServer, VisualStudio, etc. were not. Indeed, many packages in RHEL are available for, and widely used on, Windows. If Firefox or Thunderbird or Perl or Python have a vulnerability then it is as much a problem for Windows as for RHEL. I doubt it gets counted that way however.
Unfortunately I think many programmers that read Slashdot are scared off by the clear, readable, maintainable syntax. Typing end is clearly too much work, or something, and as we all know IDEs can't possibly help with that... I would like to see Ada get more use, but unfortunately I doubt it is going to happen.
I think your example mostly shows how little you know about DbC systems. For example, code those contracts in Eiffel and run ES-Verify over it and it will happily inform you that the contracts on g and h cannot be guaranteed. Likewise code it in Java with JML and run ESC/Java2 over it and it will tell you the contracts on g and h cannot be satisfied, and it will even be kind enough to explain why. Fix the precondition on f to specify that that you also require a > 0 and b > 5 and all of a sudden it will verify in both systems. Which is to say that, in fact, DbC systems will let you catch precisely the sort of error you give as an example.
Even if you don't use verifiers then the problem will likely be found in testing (rather than production), and given the contract violation and the call stack you can quickly see that f will require further constraints for the pre-conditon. Running again the problem will naturally bubble up through anymore call layers if you have something calling f unsafely.
Contrary to your claims DbC is far better at catching errors such as you suggest, and is clearly going to be a vast improvement over no contracts at all.
I think you're missing the point of contracts. It isn't to tell you what the function does when you write it (though stating your intentions doesn't hurt to clarify your thoughts), it is to tell other people what the function does, and to tell yourself in a years time. Contracts go in the documentation so you can read them instead of having to fish through code. More importantly, for functions less trivial than the one you happened to specify, contracts can and do describe functionality and requirements far more succinctly than implementation code does. I can tell you what contracts a sort function must meet much more easily than I can explain the details of a particular sorting implementation. All you're doing is saying "here is a really simple example for which the implementation is as short as the contract, therefore contracts are always useless" which is nonsense. I can write a function for which the type signature is essentially the same as the implementation, that doesn't mean static typing is of no value. Degenerate cases don't prove ineffectiveness in general.
pre-conditions: Are there none?
post-conditions: All returned subscriptions are expired.....hmmm seems to be stating the obvious.... It seems simple enough to me. Presuming you don't already have an invariant to cover it you might end up with But perhaps some of the Eiffel idioms are not helping there, so how about in JML for Java Or something similar (it depends on the implementation as to the exact details of course). This isn't redundant information from a maintenance, refactoring, or API documentation standpoint. Perhaps because the example is simple it doesn't appear that useful, but as soon as you get much more complicated...
Just because you're interested I'll do a little boosterism for the Java DbC system because it is actually pretty cool. First I'll admit the downside: it works by embedding annotations for contracts in comments (like JavaDoc comments basically) which makes it a little bit hacked on, but you take what you can get. The upsides include: good tool support, so not only do you get a compiler that converts annotations into runtime checks, but a version of JavaDoc that incorporates annotations into the auto-generated API documentation, and a tool that can read the contract annotations and generate a corresponding JUnit class, along with automated data generation schemes (to which you can add if you wish). If you throw in ESC/Java2 which does static checking of the contracts and can catch a lot of subtle errors statically, and Daikon which exercises your code and tries to statistically infer likely invariant properties (spitting out results in form that can be added directly as annotations), and Eclipse plugins and the whole thing starts to look quite nice. Here's a journal entry I made on the subject.