Kuro5hin.org: technology and culture, from the trenches
create account | help/FAQ | contact | links | search | IRC | site news
[ Everything | Diaries | Technology | Science | Culture | Politics | Media | News | Internet | Op-Ed | Fiction | Meta | MLP ]
We need your support: buy an ad | premium membership

[P]
The Agility of Lightweight Formal Methods

By Coryoth in Technology
Wed Oct 11, 2006 at 12:00:00 PM EST
Tags: software, agile methods, formal methods, JML, Spec#, eiffel, design by contract (all tags)
Software

When most developers and programmers think of Formal Methods they tend to think of the sort of Big Design Up Front or Waterfall mentalities that these days are viewed as responsible for the failure of a lot of software projects. The modern trend is toward more flexible, so called Agile, approaches to software development. Getting early and regular feedback as development progresses can save a lot of headaches when the time comes for delivery of the final product. Contrary to common perceptions, however, this process is complementary to formal methods, and in fact lightweight formal methods can actually strengthen traditional Agile methods such as Test Driven Development.


Validation and Verification

The first step to seeing how formal methods for software verification and agile methods of software development can be complementary is to come to terms with the difference between Validation and Verification. Software validation is about asking the question "Are we building the right product?" while software verification is a matter of asking "Are we building the product right?". In general Agile methodology focuses mostly on software validation - getting working prototypes in front of the customer as soon and as often as possible to get as much regular feedback about exactly what is wanted as early in the development process as possible. From the Agile point of view there is no sense designing and building something the customer doesn't want, so early and regular feedback is key; moreover there is no point writing anything more than the minimum required to meet the clients needs at any given stage. In short, you want to be sure you're building the right product - that it has what the client wants, and that you're not wasting time on things the client doesn't care about.

In contrast formal methods focus on software verification - formalising requirements into a specification, and using those specifications to get early and regular feedback as to whether the implementation actually meets the requirements. Formal methods tend to have little or no interest in the validation side of the equation - determining whether the specifications will build the right product is considered a separate concern. Instead the focus is squarely placed on making sure the code you do right does exactly what you claim it does. From the formal methods point of view there is no sense relying on programmers to eventually spot that their code doesn't actually do what the informally written requirements actually demand; document requirements precisely and early and then let the computer do the work in an automated fashion - bugs caught early are much cheaper to fix than bugs eventually spotted down the road.

There is, of course, a certain amount of overlap. Formal methods tend to do a certain amount of software validation by working with the customer to refine a detailed formal specification. Agile methods attempt to handle software verification by means of unit tests. In practice, except for particular projects well suited to each approach, this overlap portion represents the weakest aspects of both methodologies: hypothetical models based on formal specification are a lot harder for clients to deal with than working prototypes and mock-ups; Unit tests offer, at best, rough case-wise specifications and leave plenty of scope for unforseen corner cases, and unexpected behaviour.

Agile Formal Methods

The obvious approach, then, is to try and take the best aspects of each approach and use them to bolster the weak points. This is actually surprisingly easy. Simply take an Agile approach, such as Test Driven Development, and augment the weaker Agile "verification via unit testing" with lightweight formal specification and the far more powerful verification that then becomes possible. You retain the Agile approach with rapid and regular customer feedback, including such things as Fit acceptance testing, while getting the strength of formal methods for verification: instead of just adding new unit tests, you add or refine the specification.

Isn't writing formal specifications all the time too hard, and formal verification just too much hard work? Perhaps, but there's a reason I said lightweight formal specification - a great deal of formal specification can be achieved easily using contracts which, when using JML for Java, Spec# with C#, or Eiffel, are no harder to write than the equivalent unit test. In practice writing a contract is actually simpler, and requires less framework and template code, than writing the equivalent unit test. As for how hard the resulting verification process is - it turns out to be very efficient: JML for Java supports ESC/Java2 for very practical yet powerful verification, while Spec# includes its own similar verifier, and there are many other tools available which will be discussed later. Modern verifiers such as ESC/Java2 and the Spec# verifier take a pragmatic approach, making use of the specification to do a raft of static checks, proving what they can, and simply warning about what they cannot - they integrate easily into modern IDEs like Eclipse and VisualStudio, and generally take around the same length of time to run as a compiler or unit test suite.

Is this approach really practical? Yes, it is - there is already a system for Eiffel called ESpec that provides an integrated workbench for exactly this design approach, seamlessly integrating Fit testing and Agile software validation techniques with formal specification, and code verifiers. Even if Eiffel isn't your language of choice it may still be worth a glance since similar systems will more than likely soon start appearing for Java and C#.

What Does it Do for Me?

Given the ingrained resistance to formal methods in the Agile community due to historical arguments and a lot of mistaken assumptions from both sides, it is worth outlining what adding lightweight formal methods to the traditional Agile process can actually do for you. The first win, and this may sound odd, is that it is actually less work! Given a good contract system such as that of Eiffel, JML, or Spec#, writing formal specifications is often easier and involves less redundant template code than writing the equivalent unit test. Of course not everything can be efficiently expressed as a contract - but no one is asking you to do away with unit testing, ESpec, for instance, specifically integrates unit testing into the workbench to cover cases that are more easily specified as tests rather than contracts. What a little specification really buys you, however, is far more powerful verification and testing - so lets talk about some of the sorts of tools that are available.

The power of extended static checking should not be overlooked. You can think of it as lint on steroids if you like - but it is definitely worth taking a look at what modern extended static checking using contracts can do. Essentially the static checkers analyse the code and contracts checking both for common errors (much as lint does) as well as attempting to verify that the code meets the contracts using theorem provers. Counterexamples will even be generated in cases where contracts will not necessarily be met. ESC/Java2 can catch everything from potential null pointer exceptions to possible race conditions. And all of this can be seamlessly integrated into your existing IDE. Extended static checking catches potential bugs early, and catches bugs that will be missed by all but the most exhaustive of testing.

The other push button power tool is automated testing. Again it is Eiffel that offers the most robust solution here with AutoTest, but similar tools are in development for Java, and for Spec#. The idea is simple enough - use contracts as a test oracle and generate random test data. In the case of AutoTest this has produced a tool in which the developer simply presses a button and walks away and the code is exercised automatically, over a vast array of possible test cases, and a simple final report with simplified failure cases is presented at the end. Test data can be generated by many different schemes, from purely random, to genetic algorithms, to schemes designed to provide maximal search space coverage. Failing test cases are even automatically added to unit tests for regression testing. This sort of thrash testing really is effective: AutoTest successfully uncovered bugs in the Eiffel base libraries that had gone unnoticed for over a decade.

By combining these approaches we arrive at a level of robustness checking and software verification that basic unit testing simply cannot match - and all at no significant extra cost. By writing contracts instead of unit tests wherever it makes sense we enable far more powerful static checking and provide the necessary extra information for completely automated thrash testing.

Conclusions

As much as it may surprise those who are used to the ideological divide, Agile Formal Methods really can work - complementing each other very naturally to provide a far better system than either methodology can offer alone. Moreover this sort of pragmatic lightweight formal method approach is beginning to seriously gain traction with JML and Spec# becoming increasingly popular. Already Agile Formal Methods suites are available for Eiffel, and we can expect that it is only a matter of time before similar systems become popular for Java and C#.

Sponsors

Voxel dot net
o Managed Hosting
o VoxCAST Content Delivery
o Raw Infrastructure

Login

Poll
Can Formal Methods be Agile?
o Yes 25%
o No 0%
o Yes, but it will never catch on 33%
o No, but it will be a popular buzzword 66%

Votes: 12
Results | Other Polls

Related Links
o Big Design Up Front
o Waterfall
o Agile
o Test Driven Development
o Fit acceptance testing
o contracts
o JML for Java
o Spec# with C#
o Eiffel
o ESC/Java2
o ESpec
o AutoTest
o for Java
o simple final report
o Also by Coryoth


Display: Sort:
The Agility of Lightweight Formal Methods | 26 comments (19 topical, 7 editorial, 0 hidden)
Abstained. (none / 1) (#2)
by creature on Wed Oct 11, 2006 at 06:02:35 PM EST

I normally have a hard-on for stuff like this, but man - you wrote one boring article. Maybe I'm in the wrong frame of mind but this made me drowsy.

Oh, one more thing: (none / 1) (#3)
by creature on Wed Oct 11, 2006 at 06:03:18 PM EST

So why didn't I -1? Because you were non-trolling and got your grammar straight.

[ Parent ]
-1, too much Wikipedia (2.33 / 3) (#5)
by alby on Wed Oct 11, 2006 at 06:11:32 PM EST

I like Wikipedia as much as the next man, but the first four links all go to crap Wikipedia pages. I suspect the rest do too, but TLDR.

--
Alby

ZZZZZZZZZzzzzzzzzz... (1.50 / 8) (#6)
by the spins on Wed Oct 11, 2006 at 06:39:44 PM EST

y'all should wait around until i submit my grand article on classical airfoil theory. oh wait, i won't, because that would be boring as shit, just like this article.

 _
( )
 X
/ \ SUPPORT THE DEL GRIFFITH MODBOMBING CAMPAIGN

Wake me when there's tits [nt] (1.00 / 8) (#8)
by debacle on Wed Oct 11, 2006 at 07:31:06 PM EST



It tastes sweet.
agreed (3.00 / 3) (#12)
by dongs on Thu Oct 12, 2006 at 02:22:29 AM EST

agile formal methods complement each other very naturally to provide a far better system than either methodology can offer alone.

AKA How managers justify their existence part III (2.60 / 5) (#13)
by toulouse on Thu Oct 12, 2006 at 04:49:28 AM EST


--
'My god...it's full of blogs.' - ktakki
--


Management optional (none / 1) (#19)
by Coryoth on Fri Oct 13, 2006 at 09:11:31 AM EST

Pretty much all of this is management optional - it is not about new rules and procedures for management to impose, its about new tools and techniques for developers to use. Rapid feedback and acceptance testing via Fit tables is simply something developers can do to get a better idea of requirements than relying on whatever vague and poorly communicated spec their manager gives them. Adding contracts to code is just that: coding - it is developers only. Once you've got the contracts written in the code it is all abot the new tools that are available to get a ot of the hard work of weeding out bugs done for you, automatically, at the push of  button. Have a look at ESpec.

[ Parent ]
I find that. . . (2.33 / 3) (#14)
by IHCOYC on Thu Oct 12, 2006 at 07:40:48 AM EST

Problems in a development process may arise in three places:
  • at its proposal and inception, which in A. E. Neuman's terminology is labelled the alpha phase;
  • during the period of its operational implementation, the theta phase; and
  • during its finalization, or the closing stages of the process: the omega phase.
Problems in a development process may moreover be classified into two separate categories:
  • the monogenetic problem, in which a single cause intervenes in the process, and
  • the polygenetic problem, in which several different causes intervene, either simultaneously, concurrently, or serially.

--
"Complecti antecessores tuos in spelæis stygiis Tartari appara," eructavit miles primus.
"Vix dum basiavisti vicarium velocem Mortis," rediit G
bleh (1.00 / 2) (#15)
by buford on Thu Oct 12, 2006 at 08:00:14 AM EST

Being made to take a subject on this crap in my CS course, utterly boring shite... UML diagrams! Barf!

0 because I'm probably biased about this and it actually looks like a well written article :)

zHHD's first law of grandiosity:
if a man zeros you, he is a spastic with the scro

UML is not Formal Methods (3.00 / 4) (#17)
by Coryoth on Fri Oct 13, 2006 at 12:54:52 AM EST

If you think UML has anything to do with formal methods then I am very sorry for you.

[ Parent ]
if you give a shit about computer science trivia (1.50 / 6) (#21)
by adventure games import export on Fri Oct 13, 2006 at 03:26:57 PM EST

then i am very sorry for you.

[ Parent ]
babble (1.57 / 7) (#18)
by Eivind on Fri Oct 13, 2006 at 07:50:10 AM EST

you babble a lot. But you don't actually say much of anything.

agreed (none / 0) (#24)
by randy007 on Tue Oct 31, 2006 at 06:05:09 PM EST

100% with you on that

[ Parent ]
Sounds lie ADA to me... (none / 0) (#20)
by claes on Fri Oct 13, 2006 at 02:37:59 PM EST

which wasn't all that bad except for when the idjuts decided I had to write device drivers in it. uuuugly it was.

-- claes

I just caught up with this (none / 1) (#22)
by Scrymarch on Sat Oct 21, 2006 at 05:15:07 PM EST

I found it quite fascinating. I was a formal methods maven at uni but never really saw an opportunity to apply it once I started work. Similarly I find the Agile principle of sufficiency absolutely invaluable, but often find rigourous unit tests hard to retrofit onto existing code, or code dependant on fixtures like databases. Mock objects, they say, but it's never given me much joy.

If you're using automatically generated unit tests, do they run into the same problems as manual unit tests re mock objects?

Damn shame about the k5 reception on this very lucid article. Are you planning on writing followups? Where are you thinking of posting them?

Thanks (none / 1) (#23)
by Coryoth on Mon Oct 23, 2006 at 09:07:41 PM EST

Thanks for the positive feedback. I was thinking, in fact, about a follow up posted here, though it houdl work as a stand alone article and, given a slightly more direct approach, will hopefully be a little better receieved.

As to the issue of mock objects - specification doesn't completely eliminate the need for them for testing purposes, but provides a far more detailed interface specification which makes writing mock objects a lot easier when they are required - the absolute minimum to provide results meeting the postconditions and invariants is sufficient to support testing, and those conditions are explicitly spelled out. It's still not ideal, but then few things are. It does provide some improvements.

[ Parent ]

Zzzzz (none / 1) (#25)
by randy007 on Tue Oct 31, 2006 at 06:05:40 PM EST

boring

lack of evidence (none / 0) (#26)
by jcarnelian on Wed Nov 01, 2006 at 05:39:40 PM EST

<i>Given the ingrained resistance to formal methods in the Agile community due to historical arguments and a lot of mistaken assumptions from both sides,</i>

No, the resistance to so-called "formal methods" is that there is no evidence whatsoever that, given any particular budget, they improve software quality any more than other methods one could use.

The Agility of Lightweight Formal Methods | 26 comments (19 topical, 7 editorial, 0 hidden)
Display: Sort:

kuro5hin.org

[XML]
All trademarks and copyrights on this page are owned by their respective companies. The Rest © 2000 - Present Kuro5hin.org Inc.
See our legalese page for copyright policies. Please also read our Privacy Policy.
Kuro5hin.org is powered by Free Software, including Apache, Perl, and Linux, The Scoop Engine that runs this site is freely available, under the terms of the GPL.
Need some help? Email help@kuro5hin.org.
My heart's the long stairs.

Powered by Scoop create account | help/FAQ | mission | links | search | IRC | YOU choose the stories!