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]
A Case for Formal Specification

By Coryoth in Technology
Sat Jul 30, 2005 at 11:51:28 AM EST
Tags: Software (all tags)
Software

Formal Specification helps build more robust, more maintainable software with fewer bugs and defects. It has a long history, but it is still a developing field. While it may not be suitable for all software projects, a case can be made that there are many projects not currently using formal specification that stand to benefit from it. As the methods and tools for formal specification develop it is increasingly becoming something that developers and software engineers should learn to use to their advantage.


What is Formal Specification

Formal specification is simply a matter of being more explicit and specific in defining the requirements of software. At the simplest level this can take the form of Design by Contract, where functions and procedures specify pre- and post-conditions and loops and objects include a set of invariant properties. In the more rigorous case formal specification involves building an explicit mathematical definition of the requirements of the software. Using such a definition one can prove the correctness of the system, or simply prove theorems about properties of the system. An implementation can also be checked against such a formalised specification, verifying that the implemented code does indeed do precisely what the requirements claim. At the most rigorous level the initial formal requirement specification can be expanded, through (mathematically rigorous) refinement, to ever more specific and detailed specifications resulting eventually in executable code.

All of these different levels allow a significantly greater degree of analysis of the software, be it improved static and runtime checking with contracts, to more complex data flow analysis and proof with more complete specifications. In the same way that static types allow more rigorous checking at compile time, catching a lot of simple errors, contracts and specifications allow even more analysis and checking, catching even more errors at the early stages of development when they are most easily and efficiently fixed.

A Simple Example

In order to be both short and easily comprehensible, examples of formal specification are necessarily simplistic. This example should at least provide an idea of what a formal specification might look like however.

The specification for a simple stack, in SPARK, a version of Ada that adds formal specification semantics, would look something like the following:


package Stack
--# own State: Stack_Type;
--# initializes State;
is
    --# type Stack_Type is abstract

    --# function Not_Full(S: Stack_Type) return Boolean;
    --# function Not_Empty(S: Stack_Type) return Boolean;
    --# function Append(S: Stack_Type; X: Integer) return Stack_Type;

    procedure Push(X: in Integer);
    --# global in out State;
    --# derives State from State, X;
    --# pre Not_Full(State);
    --# post State = Append(State~, X);

    procedure Pop(X: out Integer);
    --# global in out State;
    --# derives State, X from State;
    --# pre Not_Empty(State)
    --# post State~ = Append(State, X);

end Stack;

The package body, containing the implementation, can then follow.

The own simply declares the variable State to be a package global variable, and initializes means that the variable State must be initialized internally in this package. We then declare an abstract type (to be defined in implementation) and some simple functions. The in and out keywords in the procedure declarations tag the parameters: in means that the parameters current value will be read in the procedure, and out means the parameter will be written to in the procedure. The global keyword declares the the package global variable State will be used in the procedure (and both read from and written to). The derives keyword provides explicit declarations of which input will be used in determining variables that will be output or written to. The pre- and post-conditions should be largely self explanatory.

As you can see, mostly all we are doing is making explicit exactly how we intend the procedures to operate. This specificity provides automated verification tools the information necessary to properly analyse and validate implemented code: Prior to a compile step you can run a verification and flow analysis tool that catches many subtle errors.

A similar object, specified in an algebraic specification language like CASL might look something like this:


spec
    Stack[sort Elem] =
    sort
        stack
    ops
        empty: stack
        push: stack * Elem -> stack
        pop: stack ->? stack
        top: stack ->? Elem
    axioms

        not def pop(empty)
        not def top(empty)
        forall s : stack; e : Elem
             · pop(push(s,e)) = s
             · top(push(s,e)) = e
end

CASL offers syntax that can compact this considerably, but this longer version is probably more clear.

We declare a specification for a stack of generic elements, of sort stack; and with operations empty (which is in a sense the constructor creating and empty stack); push which maps a stack and an element to a "new" stack; pop a partial function (denoted by the question mark) which maps a stack to "new" stack; and top another partial function which maps a stack to an element. We then define axioms: first, as pop and top are partial functions, we say they are not defined on empty stacks; secondly we declare that pop and top should behave as (partial) inverses for push for all stacks and elements.

This is sufficient information to completely specify stacks as a universal algebra and brings a great deal of powerful mathematical machinery to bear on the problem, much of which has been coded into a set of analysis tools for CASL.

While these examples are very simple, they should give you the flavour of how formal specification can work. Both SPARK and CASL support structured specifications, allowing you to build up libraries of specification, making them scalable to very large problems.

Why Use Formal Specification?

Why use static types? Why do any compile time checking? Why produce design documents for your software? Not every project is worth writing design documents for, and some projects are better off being developed quickly using a dynamically typed language and runtime checking. Not every project really needs formal specification, but there are a great many software projects that could benefit greatly from some level of formal specification - a great many more than make use of it at present.

I would suggest that it is probably unimportant whether your paint program, music player, word processor or desktop weather applet uses formal specification. What about your spreadsheet application? Bothering with formal specification for the GUI might be a waste of time. Bothering to do some specification for the various mathematical routines, ensuring their correctness, would potentially be worth the extra trouble. Formal specification doesn't need to be used for a whole project, only those parts of it that are sensitive to error. Likewise any network services could easily benefit from formal specification on the network facing portions of the code to significantly reduce the possibility of exploits: it is far easier to audit and verify code that has been properly specified. Security software, and implementations of cryptographic protocols, are far safer if formally specified: with cryptography the protocols are often rigorously checked, and many exploits relate to errors where the implementation fails to correctly follow the protocol. Finally mission critical business software, where downtime can costs millions of dollars, could most assuredly benefit form the extra assurances that formal specification and verification can provide.

None the less, barring a few industries, formal specification has seen little use in the past 25 years. Developers and software engineers offer many excuses and complaints as to why formal specification isn't suitable, isn't required, or is too hard. Many of these complaints are founded in a poor understanding of how formal specification works and how it can be used. Let's consider some of the common complaints:

But Formal Specification is too much Work...

Formal specification can be as much work as you choose to make it. You can do as little as adding contracts to critical functions or classes, or you can write the entire project from the top down by progressive refinement of (and verification against) a specification for which you have created formal proofs of all important properties. There is a sliding scale from a dynamically typed script with no documentation or comments, all the way up to a completely explicitly specified and proven system. You can choose the level of specificity and verification that the given component requires.

Writing contracts is only a little more work than static typing: you are simply declaring formally what you intend the function to do, something you ought to have a clear idea of before you write the function anyway. Writing a basic specification is only a little more work that writing a design document: you are simply formalising the diagrams and comments into explicit statements. For a little extra work in the initial stages you gain considerably in debugging and testing. Extended static checking based on contracts can catch many simple errors that would otherwise go unnoticed, and debugging is significantly accelerated by the added information contracts supply about runtime errors. If you've gone to the trouble of writing a formal specification you can statically verify various behaviours and properties of the system before it is even implemented. Once implemented you can validate the implementation against the specification. When performing testing you can use the specification to help determine the best coverage with the least testing.

Formal specification does work in practice, and the gains in efficiency in testing and debugging can often outweigh the potential extra overhead during design. Design by Contract, for instance, is often cited as saving time in the development process, and there are many real world success stories where systems were developed faster by using contracts. A 20 person team completed in 5 months what took a team of 100 people using standard C++ almost a year. For projects where robustness is critical, full formal specification has been used successfully. Companies like Praxis High Integrity Systems use formal methods successfully in the rail, aerospace, nuclear, finance and telecommunications industries (among others), and have sold their formal method tool-set to a variety of large companies. Reading through some of their recent work and case studies makes it clear that formal specification and verification can prove to be more efficient and faster to use.

But Formal Specification is Not Practical...

On the contrary, formal specification is used all the time in many industries, and there are various companies like Praxis High Integrity Systems, B-Core, Eiffel Software, Kind Software, and Escher Technologies who provide formal specification tools as a major part of their business.

Formal specification has proved to be practical in the real world. What it has lacked is mature tools to make development using formal specification faster and easier (try writing code without a good compiler, try doing formal specification without good static checking tools), developer awareness, and developers skilled in the languages and techniques of formal specification. It doesn't take much to learn - learning a specification language is not much harder than learning a programming language.  Just as programming appears to be a difficult and daunting task to a person who doesn't know any programming languages, specification looks difficult to people who don't know specification languages.

But Formal Specification Still Can't Guarantee Perfect Software...

Correct, there are no guarantees. Complete proofs are often too complicated to perform, so theorem proving for specific properties is usually undertaken instead. Static checking can be enhanced significantly with suitable specifications, but not all errors can be caught. Your software is only going to be as stable and secure as the system it is running on. If you can't be perfect why try at all? Because significant gains can be made and the costs may be smaller than you think. Even if the whole system can't be proved, managing to prove key properties may well be all the assurance of correctness that is required for the application at hand. Even if you can't catch all the errors statically, reducing the number and severity of runtime errors can bring significant efficiency gains in the testing phase. Furthermore the cost of errors in software found after release can be sufficiently high that any reduction is worthwhile. Finally if you can't trust your compiler and operating system, then everything is compromised. At some level you have to trust something - we all trust a great deal of software right now that we expect to have flaws - reducing the source of errors to trusted components is still a significant gain.

But Formal Specification Is Only Viable for Trivial Examples...

Not even close to the truth. Formal specification and formal methods have been used for large projects involving hundreds of thousands of lines of code. Just look at many of the examples provided above: these were not small projects, and they were not toy trivial examples; these were large scale real world software systems. Examples of formal specification tend to be small simplistic cases because they are meant to be just that: easily comprehensible examples. In the same way that programming languages often use "Hello World" and quicksort as examples, formal specification languages use equally simple but demonstrative examples. Don't take this to mean that the language and method doesn't scale.

Conclusions

Formal specification isn't a silver bullet, and it isn't the right choice for every project. On the other hand you can use as much specification and verification as is suitable for your project. You can apply formal specification only to the portions that are critical, and develop the rest normally. More importantly, the techniques, languages and tools for formal specification continue to improve. The more powerful the methods and the tools, the more projects for which formal specification becomes a viable option. In an increasingly network oriented computing world where security and software assurance is becoming increasingly important, the place for formal specification is growing. If you are a software engineer it makes sense to be aware of options available to you.

Sponsors

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

Login

Related Links
o Design by Contract
o SPARK
o Ada
o CASL
o many
o real world
o success stories
o 20 person team completed in 5 months
o Praxis High Integrity Systems
o a variety of large companies
o recent work
o case studies
o B-Core
o Eiffel Software
o Kind Software
o Escher Technologies
o Also by Coryoth


Display: Sort:
A Case for Formal Specification | 151 comments (142 topical, 9 editorial, 0 hidden)
On the subject of verification (3.00 / 3) (#4)
by dimaq on Fri Jul 29, 2005 at 02:06:02 AM EST

You are touching an interesting subject here. software verification et.al. will be seen more and more.

And yet most of the code that I end up writing falls into 2 categories neither of which gives to the formal specification easily -

1. Business logic. specifying it in words is already hard, coding alread complex, formal specification would be 3 to 10 times more complex than the code.

Twice more complex might still be acceptable becuase code needs more debugging than the spec.

Business logic tends to evolve over the course of project too, maintaining 3 copies of it (human language doc, formal spec and programming language code) would be a significant hindrance.

2. Libraries. once written and debugged they don't require formal specifictaion anymore. it could still be useful to verify libraries in simpler cases, like a malloc implementation, but becomes more and more difficult when higher level objects are concerned, such as an xml stream. provided that library functionality is frozen, I don't see much use in formaliszing it beyond the interface and some documentation. although I admit it would be cool!

What I would like to see on the automatic verification front is a tool that is able to deduce the intention of the programmer from the source code (with minimal annotation for the tool). so if you wrote memcmp(), it would detect a bound read-only memory access and be able to use this information later when the function is invoced from some other bit of source code. obviousely such a tool would have to come with a library of concepts it understands (such as free memory or objects or linked lists), though considering how often we reinvent the wheel in programming, I guess the variety of programming concepts is still orders of magnitude smaller than the number of implementations or pieces of code written.

Someone once wrote a demo compiler that outputs binary (for a library or function) together with a proof that the code won't do anything illegal (like reading random memory address). I suppose it cannot handle complex functions/libraries, but it's a start. And it's only a security thing, it doesn't prove the correctness of the results.

An alternative is to write in ever higher level programming languages which (through some inefficiency) guarantie safety from ever wider range of mistakes.

I think this depends (2.50 / 4) (#7)
by Coryoth on Fri Jul 29, 2005 at 02:46:13 AM EST

Business logic. specifying it in words is already hard, coding alread complex, formal specification would be 3 to 10 times more complex than the code.

In some cases it could well be an issue, particularly for very poorly defined business logic (which is to say, a lot of cases).  There are cases though where the extra work of formalising the logic (or at least getting the client to be specific enough that it can be formalised) saves you a lot of work down the line...

Business logic tends to evolve over the course of project too, maintaining 3 copies of it (human language doc, formal spec and programming language code) would be a significant hindrance.

You see if you hammer things out to the point of formality at the beginning, that can eliminate some of the changes down the line by getting a much more exacting set of requirements at the outset.

The other thing you can look at is something like SPARK or JML where code and specification are maintained together in the same files.  With JML (which is essentially Java with annotations for specification and associated tools to process the annotations) you can use javadoc to have documentation, specification and implementation all in the same place, with the specification handling a lot of the documentation for you.  Simply update the specification, and then fix the code till it validates against the new specification.

The other bonus is that if you wrote a solid specification at the beginning it can be a lot easier to determine the impacts that a change in requirements will have, and to ensure that that any such change is fully implemented and you don't have legacy code hanging around causing errors or security holes.

What I would like to see on the automatic verification front is a tool that is able to deduce the intention of the programmer from the source code (with minimal annotation for the tool)

It's a lovely idea, but I just don't think it is viable.  Managing to deduce the intention of the programmer with the current level of formal specification is hard enough for the automated tools we have.

Think of specification this way: take a moment to first write some quick (specification) code saying what you mean, then sit and write the code for how you think that should be done.  It's hardly that much extra work if you have bothered to learn a spec language (or a programming language that has support for specification such as contracts).

Jedidiah.

[ Parent ]

business logic is not very poorly defined... (none / 1) (#59)
by dimaq on Sat Jul 30, 2005 at 05:40:59 AM EST

...or perhaps is inherently poorly defined.

Either way the point being that business logic is inherently complex and computer science is poorly suited for it.

I thounk I should refer you to the mythical man-month for details.

[ Parent ]

But that's where you want precise specs (none / 0) (#70)
by GileadGreene on Sat Jul 30, 2005 at 11:10:58 AM EST

"Inherently complex" systems are exactly where you would want precise, formally analyzable specifications: the formal nature of the specification allows you to manage the complexity of the logic. It's the simple or trivial systems where using a formal approach is less well-suited - like swatting a fly with an elephant gun.

BTW, Brookes' point in the Mythical Man Month was that there is no one technique that will solve all of your problems - not that there aren't techniques that could help make your job easier.

[ Parent ]

Brook's point that I was referring to (none / 0) (#86)
by dimaq on Sun Jul 31, 2005 at 07:13:10 AM EST

is that programming is inherently complex because program are meant to solve inherently complex problems.

Applied to the verification thing, what I was trying to convey was that fully formalizing a problem or an algorithm would necessarily require more work than hacking some implementation that happens to work for now.

My view is that formal specification is 3x to 10x longer than code. Also formal spec is something that needs to be understood (by programmers, etc), while code demonstrated to work doesn't need to be understood. (alright, are changes or bugs, partial understand is required).

[ Parent ]

Why fully? (none / 1) (#89)
by GileadGreene on Mon Aug 01, 2005 at 11:33:40 AM EST

...what I was trying to convey was that fully formalizing a problem or an algorithm would necessarily require more work than hacking some implementation that happens to work for now...

Who said anything about fully formally specifying something? You're right, that would be a lot of effort, and probably not worth it in most cases. The idea is to formally (i.e. precisely) express those elements of the design that are most critical and/or most complex. Because those critical or complex parts are expressed formally they are then amenable to analysis that allows you to ensure that (a) the critical properties you wnat to be preserved actually are, and (b) the complex interactions actually produce a result that you want.

My view is that formal specification is 3x to 10x longer than code.

Have you ever actually done any formal specification work? I have, although I'll admit that my experience is limited. But none of the projects I've worked on involving formal specification have produced a spec even 1x the size of the code, let alone 3-10x. Mostly because we only formally spec'ed the critical elements of the design (as I mentioned above). But also because a real formal spec is written at a level of abstraction above the final code, so it can express more in less space. Most of my experience has been with CSP, and there we typically see code that is around 8x larger than the original spec (varies slightly with target language).

Also formal spec is something that needs to be understood (by programmers, etc), while code demonstrated to work doesn't need to be understood.

I hope this is a joke. Of course code should be understandable, for maintenance reasons if nothing else. To say nothing of the fact that if the task you are supposed to be doing isn't defined (by some kind of spec) then how do you know when it actually meets the criteria that allow it to be "demonstrated to work"? If you just run the code until the output "looks right", how do you know that it'll still look right when you run with some other input that you have tested? Honestly, this sounds like code development by the "monkeys producing Shakespeare" method.

[ Parent ]

if you wrote a solid specification at the beginnin (none / 1) (#60)
by dimaq on Sat Jul 30, 2005 at 05:56:05 AM EST

then you already eneded up with "clean-room software development model" and that is not something you want! not in real life cases anyway.

[ Parent ]
Oh, and libraries... (2.00 / 4) (#9)
by Coryoth on Fri Jul 29, 2005 at 03:17:43 AM EST

Libraries. once written and debugged they don't require formal specifictaion anymore. it could still be useful to verify libraries in simpler cases, like a malloc implementation, but becomes more and more difficult when higher level objects are concerned, such as an xml stream. provided that library functionality is frozen, I don't see much use in formaliszing it beyond the interface and some documentation.

It's worth having a formal specification for libraries - in fact you can have libaries of specifications.  The point is this: Say I want to link to a given library and use a given function in my application.  When I go to do analysis on my application the tools will have no idea what to make of the external call to the library... unless  I have a spec for the library - in which case I only need to make sure that data I pass to the call always meets the preconditions, and my application never assumes the data that comes out violates the post conditions (and possibly that the class I've called from the library only assumes its invariant properties as necessary for operation).  I don't need to run the analysis over the library itself - hopefully it has already been verified, but I do need to know the explicit specifications of the library so the analysis can be sure that I am using the library correctly.

Jedidiah.

[ Parent ]

this is like saying that (none / 1) (#58)
by dimaq on Sat Jul 30, 2005 at 05:37:14 AM EST

that one could very well use a formal specification for a computer (hardware) when testing some new peice of software - surely it would be neat and might catch a few bugs, but hardly worth it!

[ Parent ]
C libraries have formal specification (2.00 / 2) (#79)
by Coryoth on Sat Jul 30, 2005 at 04:44:06 PM EST

No, really, they do.  It's just a very limited kind.  If you want to call a function from a C library, you need to pass it parameters of specified types.  That is, the function specifies the types of parameters that it takes (as well as the type of value it will return).  You can take that further and rather than just saying "the first parameter must be an int" you can say "the first paramter must be an even integer value between 0 and 312", or whatever is required for that particular function.  Right now we do that with a loose definition in the documentation.  Formal specification would simply be a matter of truning that english language description into a specific computer parseable description so that you can do checks beyond "am I passing this function the right type?" and make sure you are always passing valid values.  Moreover, you have more specfic specification of the return values, allowing you to reason more carefully about how you use them, and construct proper proofs of your code.

Jedidiah.  

[ Parent ]

Libraries (2.00 / 4) (#12)
by Vs on Fri Jul 29, 2005 at 06:11:50 AM EST

Even debugged libraries have specifications, albeit only in the documentation: "Don't pass a NULL-ptr" here, "Only pass values >0" there.
--
Where are the immoderate submissions?
[ Parent ]
I disagree... (2.50 / 2) (#65)
by skyknight on Sat Jul 30, 2005 at 09:07:50 AM EST

Having some kind of formal specification for a library is highly useful. First of all, it's hardly ever the case that something is fully debugged or feature-frozen. Even assuming for a moment, though, that it is behaviorally correct, you may one day wish to rewrite the internals to gain improved performance or allow it to function on a new architecture. Having the spec formalized in some way allows you to work on the guts of the implementation while being assured that you're not breaking any of the interfaces.



It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
[ Parent ]
I would agree... (none / 1) (#85)
by dimaq on Sun Jul 31, 2005 at 07:07:44 AM EST

I agree with your view except for one thing - formal specification, being a by-product of the library should be simpler than the library itself. current formal specification languages don't seem to fulfill this criterion.

in short, for a regular library, having formal spec in Z is like writing a library in python and then re-writing it (or part of it that you propose to formalize) in assembly for the purposes of documentaion!

I admit that in some cases a heavier formalization is still suitable (think space flights where delivery vehicle is thousands times heavier than the satellite).

[ Parent ]

Perfect Developer (2.00 / 5) (#8)
by QuantumG on Fri Jul 29, 2005 at 03:01:30 AM EST

I have an evaluation copy of Perfect Developer. It is a very good product, however I am not sufficiently trained to wield its awesome power. The problem is that you are required to program in a language which makes it difficult to do so. The language is too strict and dissimilar to existing programming languages. This isn't surprising, as it's ment to be a specification language, not a programming language, but unfortunately the specifications have to be so detailed that what you're really doing is programming.

More importantly, Perfect Developer is an environment for writing new software. It in no way helps you write specifications and verify them on already existing code. This is a major downfall in my opinion as it is simply not feasible to throw away all the code in existance and start again with formal methods.

So what do we need? We need tools that can extract specifications from software written in existing programming languages. I'm talking C/C++, Java and to a lesser extent, Ada. A programmer can review these mechanistic specifications and refine them such that the desired behaviour of the program (not necessarily the actual behaviour) is expressed in a clear form.

Then we need automated verification tools to prove that existing software, written in the realworld programming languages I've stated above are actual refinements of the specification.

When we have these tools we will see formal methods break into the mainstream of programming, but not before.

Ok, so when's that gunna happen? 4th of Never, right? Reasoning about software is just too damn hard for a computer to do. But what about humans? Grab yourself a professor of formal methods from your local univerisity. Give him enough students and enough money and chances are he can formally prove your implementation meets your specification in a few months. How is this possible? Well duh, humans are better at symbol manipulation than computers. It's this thing we call intelligence.

How scalable is this? Assuming we had twice as many people doing formal methods could we prove a single implementation meets a single specification in a faster time? I believe we could. I believe that specifications are in fact divisible down to the statement level.. so there's no reason why throwing more adequately trained people at the problem won't result in faster formal proofs.

But that costs lots and lots of money. Where you gunna find all these people? How you gunna train them all? Professors have it easy, they have an infinite supply of first year students who have to complete their assignments to get a grade. Unfortunately he has to mark all those assignments (although automatic proof checking is a heck of a lot better than automatic proof generation) so he tends to give them all the same problem.

What if we were to start a project where people interested in formal methods could learn how to prove some open source project's source code meets its specification? We have an automated proof checker online and people submit their proof for all the different parts of the specification. We'd still have to write the specification up front, but the most time consuming part, proving the software meets the specification would be done by thousands of distributed volunteers.

Writing specifications could be a distributed activity too, but you'd have to have volunteers review the specifications written by other volunteers.

So concludes my rant.

Gun fire is the sound of freedom.

Replacing existing code (1.00 / 2) (#10)
by Coryoth on Fri Jul 29, 2005 at 03:26:20 AM EST

As you say, you just can't throw out the wealth of already existing code that lacks sufficient annotation to make it amenable to analysis.  We do have a couple of things going for us though:

(1) We don't need to replace everything, just those portions of code that are deemed critical, be it for security or other reasons.  There is a lot of code for which it just won't matter.

(2) A project akin to this has already been undertaken: The Gnu project managed to replace the entirety of UNIX with their own "written from scratch" libraries and applications.  It can be done.

There's no need to replace everything, and there's no need for things to be switched over at once - libraries can be swapped out as needed, and you can simply link to or use informally specified code in the meantime.

If formal methods become more publicised and more popular and more software starts to get developed that way then a transition to using it wherever it is appropriate will happen quite naturally.  I'm not sure I see the need for a vast "changeover".

Jedidiah.

[ Parent ]

Side note (1.50 / 2) (#11)
by Coryoth on Fri Jul 29, 2005 at 03:30:37 AM EST

I do like your idea for creating a distributed system to write and verify specifications to help buld up a good set of base libraries of specifications.  I mean, that's how Gnu managed to pull off their minor miracle right?

It is something I will keep in mind for when I get a little more spare time.

Thanks for your comments.

Jedidiah.

[ Parent ]

Automation (none / 1) (#48)
by GileadGreene on Fri Jul 29, 2005 at 11:44:18 PM EST

We need tools that can extract specifications from software written in existing programming languages. I'm talking C/C++, Java and to a lesser extent, Ada.

There has been at least some work on this already - see for example Martin Ward's work on abstracting specs from source code - but I'm not sure it's hit mainstream tools yet. More recently, Gerard Holzmann and NASA-JPL have done some work on abstracting concurrent C programs into the Promela modeling language.

There have also been plenty of projects that have simply performed a manual abstraction from code to spec, so it's not really the case that tools are 100% necessary. The reality is that in many cases, only some small, but critical, portions of the code need to be verified, so that's all you need to reverse-engineer.

Well duh, humans are better at symbol manipulation than computers.

Not really true. In fact, most applications of formal specification techniques to industrial-scale problems make use of either fully automated model-checking, or use proof-assistants to help humans deal with the complexities of the correctness proof.

What if we were to start a project where people interested in formal methods could learn how to prove some open source project's source code meets its specification? We have an automated proof checker online and people submit their proof for all the different parts of the specification. We'd still have to write the specification up front, but the most time consuming part, proving the software meets the specification would be done by thousands of distributed volunteers.

This is a nice idea, but a little misguided. The reality is that it's often the writing of the spec that's the time consuming part, not performing the verification. But it's also spec writing that's the most valuable part, since it forces you to clarify your ideas about what the system is and is not supposed to do. Often that can be very hard for people to articulate precisely.

Richard Guindon once wrote that "writing is nature's way of telling you how sloppy your thinking is." Leslie Lamport went a step further, and said: "mathematics is nature's way of telling you how sloppy your writing is."

[ Parent ]

Marketing Formal Specs and Program Correctness (1.75 / 4) (#13)
by OldCoder on Fri Jul 29, 2005 at 09:10:06 AM EST

Some business IT shops have a cadre of professionals called 'Systems Analysts' who are a ripe target to convert to formal specification. But lots of business environments don't have a place for a design phase. The PHB is going to ask "How long will it take?" and "Why do you have to do it?".

It's all about tools. Formal specifications and proving program correctness have a great potential for improving software quality and productivity, but the tools and even the underlying theoretical analysis just isn't in place.

It is notable that Microsoft tools provide zero support and their publications about "Best Practices" don't even mention the topic. I've looked through Microsoft Research pubic websites and see precious little. Although there is a related internal MS product called 'Prefix' that is worth investigating.

One of the practical problems with software analysis tools is that you have to analyze the environment, the libraries and the operating systems as well. When the code makes a call "Outside" the analyzer gets lost. This is similar to the problem of providing symbol tables and precompiled headers for kernels and libraries -- that is, it's a solvable problem. But the whole thing requires system level support. And neither Linux nor Windows provides it.

Fortunately, there are many competing groups fighting out "Language Wars"; Python vs Ruby, C# vs Java, Lisp vs Fortran... If one of the groups could offer useful tools to provide provable practical program correctness they could pull ahead. So the question is, why aren't they doing this? Microsoft has the resources to do this and is offering nothing. The Universities and Labs have good connections with the Linux community but appear to be doing nothing. Eiffel was founded on the idea and is not exactly taking the world by storm.

The embedded systems market should be a good target for a software correctness toolset because debugging and developing can be so much more expensive in that environment. If Cisco or a telecom company is going to put a million lines of software into ROM and deploy that box to a hundred thousand remote locations you'd better believe they would be willing to spend to get it right. Likewise with avionics and some medical systems.

The market evidence is that there is something wrong with Design By Contract and proving software correct. And you can no longer claim that it's just unfamiliarity. It's been over 16 years since Gries published The Science of Programming, and 30 years since Dijkstra published A Discipline of Programming.

Currently, India is competing with the US and Europe by body-shopping their citizens, apparently having no confidence in their investment or managerial skills (compare to Japan and China which compete by offering products). If India could pull ahead by offering better (proved?) software, they'd love to do it. But they aren't. Neither is (hardly) anybody else.

--
By reading this signature, you have agreed.
Copyright © 2004 OldCoder

Programmers can't estimate the test cycle (none / 0) (#18)
by Coryoth on Fri Jul 29, 2005 at 12:58:50 PM EST

I think one of the main reasons that formal specification has had so little uptake is that programmers aren't very good at all at estimating how long the test phase is going to take.  Let's be honest, programmers are notorious for underestimating how much time and effort testing will take.  Whenever a project ends up horribly behind schedule it is often because testing time blew out from what was predicted.  Whenever a project has some phase truncated to meet a deadline it is almost always the testing phase because it is taking far longer than expected.

Why does that matter?  Because formal specification offers a trade off: a little more work at the outset in the design and implementation phase, but a significant reduction in the amount of work in testing and debugging phase.  Because programmers chronically underestimate the amount of work involved in testing and debugging, they chronically underestimate the benefits of formal specification.  Almost always (and you'll see people repeat it here despite the fact that I covered this in the article) people will complain that formal specification is far too much work, and would take too long.  The practical cases where formal specification was actually used simply don't bear this out - projects that used some level of formal spec have been delivered faster and with less errors than the projects that didn't.  for all the claims that formal specification will take too long, the empirical evidence is that formal specificiation will actually save you time.  This gets ignored because programmers have a tendency to think that their project will work fine, have few bugs, and pass testing quickly and easily.  It doesn't of course, but they're optimistic that next time it will all be fine...

I do agree that the tools aren't exactly there, though Eiffel and EiffelStudio are actually great products.  While I haven't used it Perfectdeveloper from Escher Technologies looks excellent, and at least one poster here who has used it raved about it.  SPARK and the associated tools are also excellent, but the developers need to know Ada.  There has been an effort to bring similar annotations and analysis tools to Java called JML, but that is still young and the tools aren't mature yet.  So while the tools aren't quite all there yet, they are beginning to arrive and the next 5 years could see the rise of formal specification, at least on some level.

The other issue is that programmers are the most stubborn people on earth, and many are more than happy to continue polishing the turd they have.  Tell a devout C programmer that actually Java might be a better option for some projects and he'll give you a host of reasons why Java sucks and why it should never be used.  Tell a devout Java programmer that C might actually provide some benefits for some projects and he'll explain carefully why C is old, outdated and sucks, and why C should never be used for anything.

The fact is that most developers are, for all intents and purposes, devout informal specification users, so when you tell that some projects might actually benefit from using formal specification they'll just manufacture a whole bunch of (potentially unfounded) reasons why they were right all along and should keep doing exactly what they were doing.

Jedidiah.

[ Parent ]

Programmers Don't Decide (none / 1) (#117)
by OldCoder on Wed Aug 03, 2005 at 12:19:52 PM EST

Managers decide whether to use advanced tools. At least, in the larger shops they do. And there are lots of managers in IBM, CSC, Microsoft and Oracle etc. who have timed and measured and costed all their projects. Over and over. We need to find their blogs and discussion groups and see what they have to say.

--
By reading this signature, you have agreed.
Copyright © 2004 OldCoder
[ Parent ]
What's the Difference? (none / 1) (#14)
by mberteig on Fri Jul 29, 2005 at 10:38:55 AM EST

Between formal specification and test-driven development?


Agile Advice - How and Why to Work Agile
Proof by random example (none / 1) (#15)
by Coryoth on Fri Jul 29, 2005 at 11:36:07 AM EST

At it's heart the difference comes down to the difference between "Proof by construction" and "Proof by random example".  Test driven development is only as good as the tests you can dream up to use, and fails to cover cases that you fail to forsee as possible problems.  Formal specification seeks to formalise the requirements and discover all the inherent assumptions.  If you create a formal specification it becomes easy to determine what the entire test space is, and how to get best coverage.  In test driven development your coverage is only as good as what you forsee and write as test cases during development.  There's some threads about this on various comp. newsgroups, for example here, at the bottom.

Which is not to say test driven development is bad, merely that its not as complete (and certainly lacks the theoretical underpinnings that give formal specification it's strength).  There isn't really much practical difference between test driven development and just writing quick contracts into your code as you go and doing your checking at runtime (which is about the lowest amount of formal specification you can do).  Or, to put it another way, test driven development is further up the assurance heirarchy than standard coding, but formal specfication offers many layers of assurance above and beyond what test driven development can offer.

Jedidiah.

[ Parent ]

Can't you (none / 1) (#33)
by trane on Fri Jul 29, 2005 at 04:38:12 PM EST

implement your formal spec as tests?

[ Parent ]
Um... (none / 1) (#38)
by Coryoth on Fri Jul 29, 2005 at 05:51:27 PM EST

I guess you could, but that would be an extremely long compliated test to run.  If you're not testing every possible caseand system state, then you're not managing to cover as much as the spec can.  If you are testing every possible case and system state...  WOW! that's a lot of testing!

Jedidiah.

[ Parent ]

So (none / 0) (#41)
by trane on Fri Jul 29, 2005 at 07:14:26 PM EST

I don't get it. How do you know your formal spec is valid unless you define tests for the contracts? To me it seems that the testing has to be done somewhere...

[ Parent ]
Mathematical proofs (none / 1) (#42)
by Coryoth on Fri Jul 29, 2005 at 08:08:07 PM EST

How do we know that the side lengths of a right angled triangle obey the a^2 + b^2 = c^2 law without trying it for every triangle?  How do we know that there is no set of 3 postive integers x,y,z such that x^3 + y^3 = z^3 without trying every possile set of positive integers?  How do we knows that the fundamental theorem of calculus holds without trying it for every possible integral?

Some of those proofs are very hard, others are relatively easy.  Many of the proofs for well specified code are quite straightforward, and due to the nature of formal specification are amenable to automated proof tools.  At the very least you can do a certain amount of flow analysis with contracts.

Think of it as test driven design with added power for static checking that can catch a lot of bugs before you even compile, and the latent possibility of proving properties of the code if you so desire.

Jedidiah.

[ Parent ]

Never Their Absence (none / 0) (#145)
by gidds on Sat Aug 13, 2005 at 04:55:38 AM EST

I think the point is that, assomeone once said, "Program testing can best show the presence of errors but never their absence".

Testing can show that your formal spec might be valid, but it can't prove that it definitely is. There might always be a test case you haven't tried.


Andy/
[ Parent ]

Deduction versus Induction (none / 1) (#84)
by Scrymarch on Sun Jul 31, 2005 at 06:33:48 AM EST

Formal specification and particularly refinement is a deductive process.  You define the spec, then deduce the code in a number of mathematically rigourous steps.  Test driven development is a scientifically inductive process.  You predefine hypotheses you want your code to prove true.  Then you write the code and tune it until it fulfills the hypotheses.

Mathematical induction (ie formal development) can prove things in the strongest, mathematical, sense.  Test driven development can prove things in the weaker, scientific, sense of accumulating evidence until the theory breaks.  On the other hand, test driven development can more easily test empirical requirements that require a lot of financially marginal work to capture in the general case.  Eg will the boss's favourite report run in under five minutes.

They do share a philosophy of setting the exam before sitting it.  It seems to me that TDD is a kind of refinement vernacular.  I wrote a diary on it once.

I've wished in the past that the two approaches could be more formally/mechanicallly linked, say by a tool that generates specs from unit tests, but it looks like a nasty problem, provably impossible in the general case.

To Coryoth, if he's reading: cool article.  I was a formal spec maven at uni, but have never had much of a chance to use it in the wider world, beyond very occassionally and casually sketching out (Object-)Z specs to understand a problem.

[ Parent ]

That's the beauty of having formality available (2.00 / 2) (#90)
by GileadGreene on Mon Aug 01, 2005 at 11:43:21 AM EST

I was a formal spec maven at uni, but have never had much of a chance to use it in the wider world, beyond very occassionally and casually sketching out (Object-)Z specs to understand a problem.

That's the great thing about having at least some exposure to formal specification: you can "sketch out" some ideas mathematically to better understand the implications of your decisions. Nothing says that you have to do a full, refinement-driven formal development to make use of formal specification (although it's worth doing if the project warrants it). You can also do quick "back-of-the-envelope" stuff just to understand what's going on and what the implications are. And sometimes the back-of-the-envelope leads you to realize that things are more complex than you thought...

I think that's where Coryoth was trying to go with this article: to at least make people who haven't seen them before aware that these tools exist.

[ Parent ]

my eyes! they burn! (2.75 / 4) (#17)
by RelliK on Fri Jul 29, 2005 at 12:40:02 PM EST

Oh man! I hadn't seen formal specifications since soft eng courses in university, and I was hoping to never see them again. No one uses them in the real world for one simple reason: <b>they are not human-readable</b>. Consider this snippet of code (frou your example):

        not def pop(empty)
        not def top(empty)
        forall s : stack; e : Elem
             · pop(push(s,e)) = s
             · top(push(s,e)) = e

While it is very precise, it is also very useless, simply because it is written in a language that 99.9% of developers do not understand. That language is also very impractical: while it is (relatively) easy to specify basic data structures and algorithms, try using it for specifying business logic. I dare you. If you even manage to do it, your specification will be:

1. Longer than the actual code
2. Completely unreadable
3. Take you forever to complete

The purpose of specs is to give you a brief overview of the system. Both developers and managers are supposed to be able to glance at the specs and have a reasonable idea of what the system does. That is *not* the case with formal specs. You have to strain to figure out wtf they mean. That's no better than just reading code (in fact, formal specifications are a form of code!). And that is why this crack-pot idea never quite made it out of academia, and never will.
---
Under capitalism man exploits man, under communism it's just the opposite.

What? (3.00 / 2) (#25)
by Coryoth on Fri Jul 29, 2005 at 03:01:35 PM EST

No one uses them in the real world for one simple reason: they are not human-readable.

It's no harder to read than a programming language - much easier really.  I'm sure it's hard to read if you don't know the language, but C (and even Python!) looks awfully indecipherable if you don't know the language.  It is very much human readable, presuming you've learned to read.

While it is very precise, it is also very useless, simply because it is written in a language that 99.9% of developers do not understand.

That's simply because 99.9% of developers haven't learned to read it - it really really isn't that hard to learn.  If you can learn to program you can learn a specification language.  If you've learned any mathematics algebraic specification reads incredibly naturally (I was reading CASL specs successfully before I had learned any of the language at all!)  This argument is like saying no one should program Java or C# or Perl or Python or  ML or... because they would have to learn the language.  If you spend a little time learning (and believe me, it doesn't take that long) then reading specs becomes easy and natural.

That language is also very impractical: while it is (relatively) easy to specify basic data structures and algorithms, try using it for specifying business logic. I dare you.

A great many large projects involving business logic have been successfully specified and coded in SPARK, specified in B, Z, or VDM, and others.  CASL is a newer language, but other algebraic languages like Clear and OBJ3 have been used quite successfully for projects.  Just because you lack the ability to see how more complicated things could be specified doesn't mean it can't be done, and can't be done easily.  As I said, the examples were necessarily simplistic, but that doesn't mean much more complicated things can't be easily expressed.

CASL in particular has a powerful system for structuring and inheriting specifications.  This means you cna build up a library of basic specifications (which is already being done) which you can easily use as building blocks for progressively more complicated specifications.  Trying to code complex software in C without using any libraries is, unsurprisingly, very hard.  C comes with some standard libraries, and people have written many more.  Using those libraries the program becomes a lot simpler.  In the same way specifications can be hard if you want to write the entire thing completely from scratch.  Thankfully there are some standard libraries for specifications, and people are writing more.  Complex specifications are a lot easier to write than you seem to think.

Jedidiah.

[ Parent ]

ok, do this as an exercise (none / 1) (#35)
by RelliK on Fri Jul 29, 2005 at 04:52:18 PM EST

Please specify the behaviour of a (relatively simple) GUI, like kuro5hin. In fact, let's simplify it even further: specify only viewing, posting, and moderating comments. This can be described in great detail in less than a page of a really awesome specification language called English. Do that with your favourite formal specification language.

but C (and even Python!) looks awfully indecipherable if you don't know the language.

My point is, you are specifying code with.... more code! Wow, that's useful!
---
Under capitalism man exploits man, under communism it's just the opposite.
[ Parent ]

Sure, what are the requirements? (none / 1) (#37)
by Coryoth on Fri Jul 29, 2005 at 05:47:20 PM EST

Please specify the behaviour of a (relatively simple) GUI, like kuro5hin. In fact, let's simplify it even further: specify only viewing, posting, and moderating comments. This can be described in great detail in less than a page of a really awesome specification language called English.

Tell me what the requirements you're looking for are, and I'll try and write a spec for them.  If you can describe it precisely in english, then you can describe it at least and efficiently in a spec language... unless of course your englash language version of the requirements is extremely vague and ambiguous and open to considerable interpretation.

My point is, you are specifying code with.... more code! Wow, that's useful!

Yes, it is, because, you see, computers can't parse and analyse vague specifications written in english, but they can parse and analyse specification written in a formal language.  The benefits you get in writing good working code first time around via a spec, static analysis, and verification saves you vast amounts of time and effort in the testing and debug cycle, as well as providing explicit documentation of the code for when it comes time to alter or extend it.

You already specify code if you write in C, or C++, or Java, or any statically typed language - you are specifying types for variables and type signatures for funtions and methods.  That's useful from a correctness and maintenance perspective.  All I'm really saying is that there are several more layers of such specification at your disposal, and you can use as much or as little as is required - but certainly more specification is moe helpful for correctness and maintenance.

Jedidiah.

[ Parent ]

Neither will the human brain (none / 0) (#40)
by nkyad on Fri Jul 29, 2005 at 06:49:55 PM EST

computers can't parse and analyse vague specifications written in english

And the human brain can't do that either, at least not at the level required to write the desired software. Any given human brain will "interpret" the specification to fit its own expectations and prejudices - so, we're always hitting the same communication barrier, users and developers interpreting the same set of words in completely diffrent ways. That's reason to re-examine the formal specification process but I fear most users will find it absolutely unbearable - most users can't stand Math any more than they can stand C++.

Don't believe in anything you can't see, smell, touch or at the very least infer from a good particle accelerator run


[ Parent ]
So turn your computer off if it's not useful (none / 1) (#81)
by Thought Assassin on Sat Jul 30, 2005 at 10:13:51 PM EST

My point is, you are specifying code with.... more code! Wow, that's useful!

If you've never written a type declaration, or understand why they are useful*, you should probably leave this discussion to those who have.

The idea is that the user of the code only needs to understand the top level specification of the entire chunk of code they are using, and because it is machine-readable their tools can verify that the code actually meets the spec. Asking why the spec isn't in English is almost akin asking why you're not writing the whole program in English.

*Actually most of the type declarations you write are unnecessary, because a smarter compiler/language could infer them for you, but if you know that then this whole post is old news to you.

[ Parent ]

formal spec languages are harder to read (none / 1) (#149)
by jasonlttl on Tue Sep 06, 2005 at 10:14:38 PM EST

not def pop(empty)
not def top(empty)
forall s : stack; e : Elem
pop(push(s,e)) = s
top(push(s,e)) = e

That's simply because 99.9% of developers haven't learned to read it - it really really isn't that hard to learn.

There are several problems with specification languages.

First, like the unix command prompt, abstract mathematical languages have always valued concise expressions. Often this is achieved by creating a very large number of symbols and functions in a global namespace. not, def, pop, top, push, s, e. It is software development 101 to create clear function names and never use variables like s and e yet you see this all the time in formal specifications. The next great syntactical revolution will come from the field of mathematics adopting the notation and methods of software development, which has piled more resources into the problem of readability in the past 50 years than has the field of mathematics since the conception of humanity.

Second, a program reads like directions while a specification reads like a logic problem. Since a program is more or less directions, and a specification is a collection of true/false logical statements, this is more or less true. What's also true is that directions are much easier to follow than logic problems. Directions require you to follow one path of execution while a logic problem requires you to imagine all possible consequences of a set of statements. Given the abilities of humans to generalize based on examples, an example and an english description will almost always be a more efficient communications mechanism than a formal specification.

What is the error rate of a human interpretting a formal specification versus an english description? How does this change since more eyes can see an english specification? What if the english description is accompanied by annotated code as in maintenance situations (90%+ of development). If the formal spec is in addition to the english spec and the code, what is the value proposition behind formal specifications? Where is the cost to benefit analysis? If it reduces software bugs, what is the cost?

[ Parent ]
I believe you are wrong (2.50 / 2) (#39)
by nkyad on Fri Jul 29, 2005 at 06:37:47 PM EST

First, the term "business logic" is slightly wrong - "domain logic" or "application logic" describes the concept better (if for nothing else, at least because it is quite wierd to think about Mario's jump behaviour or the turning of a space shuttle antenna in order to keep it aligned to a certain satelite as "business logic").

But I believe it is fair straighforward to specify the domain logic the same way you specify data structures and algorithms. Actually, there is exactly no fundamental mathematical difference between a QuickSort and the validation of a form's data.

And I really don't know where you got the idea that the specification should be shorter than the actual code.

First, it does not make any sense to compare a written description of a system with its programmatic form (in which language, by the way? Cobol, raw Assembler and C++ are quite different beasts, lenghtwise no less).

Second, and by far the most surprising thing you said, the specification should not be "a brief overview of the system" to give developers "a reasonable idea of what the system does". The specification of a system are supposed to be a complete description of the system, in user understandable terms, stating exactly what the system is supposed to do. Anything else and you invite disaster, usually in the form of the user interpreting the loosely written specs in ways you never expected (and it will happen more or less a day before the final imovable deadline).

And by the way, how many languages is a developer expected to learn and use during his career these days? Why would learning an specification language be more difficult than learning Java or Python or Ruby?

Don't believe in anything you can't see, smell, touch or at the very least infer from a good particle accelerator run


[ Parent ]
It's Even Worse Than You Think ! (none / 1) (#116)
by OldCoder on Wed Aug 03, 2005 at 12:08:54 PM EST

The job of a business manager is to make decisions that change the way the company does things. When more and more of the operations of the company is done by software, this means that every day the boss comes to work and changes the specification!

The whole gamut of business logic should be done in the highest level of software that can be run, and kept there. It's always a prototype! The businesses of the twenty-first century will succeed by being agile. Agile means the business is always changing the way it does things -- always changing the software.

Challenge: develop the specification/proof system that can accept changes while maintaining system integrity. Hint: the definition of system integrity keeps on changing as the system changes.

--
By reading this signature, you have agreed.
Copyright © 2004 OldCoder
[ Parent ]

Agile ==> not Precise? (none / 1) (#118)
by GileadGreene on Wed Aug 03, 2005 at 12:43:24 PM EST

I fail to see how the need for agility negates the need for precision. I would think it'd be better to be capable of precisely expressing your goals at any given instant (i.e. have a formal spec) - you would then be in a better position to (a) understand exactly what change is being made (if any) and (b) understand what the implications of that change are. That's certainly been my (albeit limited so far) experience with formal specification.

If you don't really know what your supposed to be doing now, how can you possibly know that a change is needed, or where to make the change?

[ Parent ]

People are too lazy, what you are asking for (none / 1) (#19)
by tweetsybefore on Fri Jul 29, 2005 at 02:00:53 PM EST

is for people to write more code. That won't work. People cannot write more code and still stay productive at the current levels. Managers do not want you to be less productive.

A solution that would work is software that writes proofs for your code describing what it does. Design by contract is nice and I've used it in testing and verifying security constraints at run time, but to use it everwhere would slow down development. Also another thing working against it is that it isn't supported in any widely used language by default, so you have to code your own support for it. Eifel doesn't count.

I'm racist and I hate niggers.

Not exactly (none / 0) (#22)
by Coryoth on Fri Jul 29, 2005 at 02:32:35 PM EST

I'm asking for people to write more code so they have to spend less time debugging and testing.  Naturally programmers are painfully optimistic about how little debugging and testing they'll be doing, so it looks like more work.  For a great many projects it is in fact less work in all to do some specification at the beginning and save yourself large amounts of debugging.

When you say "Managers do not want you to be less productive." what you mean is "Managers are dumb, and are even worse at estimating how long software takes to test and debug."

If you want design by contract then it is available for Ada (via SPARK), Java (via JML), D (built in), Python (A PEP is pending, but the implementation is available), Eiffel (built in), and C (via a preprocessor written in Ruby).  That's a fair number of languages, and several are fairly mainstream - sure some require add ons, but JML, extra preprocessors for C, or a Python library are not exactly hard to obtain or use.

[ Parent ]

people want it built in and to work automagically (none / 0) (#27)
by tweetsybefore on Fri Jul 29, 2005 at 03:34:31 PM EST

they don't want to create alot of dependencies on software. they want to use Visual Studio and just go with it. no need to install extra stuff. People are too lazy to do the design up front.

I'm racist and I hate niggers.
[ Parent ]
Sure (none / 1) (#31)
by Coryoth on Fri Jul 29, 2005 at 04:10:40 PM EST

People are incredibly lazy - but the tools are coming.  I expect once JML is na little more mature it will get an Eclipse plug in and you'll have formal specification with Java and an IDE that fully supports it (and can probably do analysis for you).

The other point is that a bit of design up front is not such a stupid idea.  People use UML, and people write requirements and design documents.  It only takes a small shift from there to writing formalised requirements, and fully dpecifying your design.

Will people bother for that neat new mp3 tagger they're writing? No, and I wouldn't expect them to.  Will people bother for that complex three tier enterprise application?  Well you're going to have to spend a fair amount of design anyway - it can't hurt to formalise it and save yourself a lot of time in testing and debugging.

Jedidiah.

[ Parent ]

design-by-contract is a catchy phrase (2.50 / 2) (#45)
by blue tiger on Fri Jul 29, 2005 at 11:05:33 PM EST

which usually hides crackpottery. the glaring example is eiffel, which 'verifies' contracts by checking them at run-time. and disables them altogether in production code, because of performance reasons. thus it behaves like a testing framework (1), instead of a formal verification one.

(1) it is a damn good testing frameowrk, but that's outside the scope of this discussion.

[ Parent ]

That is true (none / 0) (#46)
by Coryoth on Fri Jul 29, 2005 at 11:31:10 PM EST

But if you want specification built into the language you do have limited options.  SPARK Ada or JML Java or EML (which is an ML) are your best bets.  If you want more options or more mainstream then you have to settle for just contratcs.

Of course the serious option is to learn a specification language and write your specification against that then either validate the code against it, or generate the code by refinement of the specifications.

Jedidiah.

[ Parent ]

the implementation language is immaterial (none / 1) (#50)
by blue tiger on Sat Jul 30, 2005 at 12:42:30 AM EST

heck, making formal proofs about assembly language is old news by now. see proof-carrying-code and typed assm languages. what is hard is prooving interesting properties, in your language of choice.


[ Parent ]
Indeed (none / 1) (#78)
by Coryoth on Sat Jul 30, 2005 at 04:35:11 PM EST

Proving interesting properties can be hard, and that's why there are languages, like Z, VDM, B, CASL, OBJ3, and so on that are specfically designed for specification (they are not executable) so that it is as easy as possible to prove interesting properties about them.  It is then a matter of validating any executable code you write against that spec, something for which some have tools available for, and others have tools being worked on.  The whole point of the developments in formal specification, and where the improvements are occuring now, is in the provision of tools and languages that make it easy to prove interesting properties about the code at hand.  Take a look at CSP or CCS where you can prove interesting properties about multithreaded code like "A deadlock cannot occur".  Using such methods multithreaded code goes from a horrible and complicated mess to something easy to evaluate and use.

Jedidiah.

[ Parent ]

Problem with your example (3.00 / 2) (#20)
by dhall on Fri Jul 29, 2005 at 02:15:10 PM EST

A formal spec needs to address all possible outcomes. You need to include the exceptions, since you could run out of memory or something.

Memory bounds (none / 1) (#23)
by Coryoth on Fri Jul 29, 2005 at 02:36:43 PM EST

Algebraic specifications in CASL don't worry about memory bounds because they are intended to be language and platform independent.  Given the axioms, however, it should be possible to analyse the memory bounds of the implementation using available tools.

For SPARK memory constraints are something it does worry about, and the tools specifically check such things.  In the case of my example - yes that's the high level specification, and the implementation in the package body will need to contain some further annotations.  Those annotations (which aren't hard to add) provide the SPARK analysis tools all they require to do complete analysis of memory bounds and other such issues.

In short: yes, you are right, but I was trying to keep the examples simple and clear.

Jedidiah.

[ Parent ]

That you are intending... (none / 1) (#63)
by skyknight on Sat Jul 30, 2005 at 08:36:50 AM EST

something to be platform independent is no reason not to test the behavior of code under scenarios that will arise in concrete instantiations. You could still simulate such an error as the memory allocator choking, using some kind of mock object, and then see what happens.

It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
[ Parent ]
Formal specs are not code (none / 1) (#71)
by GileadGreene on Sat Jul 30, 2005 at 11:30:57 AM EST

The formal spec is not code. It is a precise description of what the code should do when it is operating correctly. If the underlying infrastructure is not working, then the spec is meaningless anyway - correct behavior simply may not be possible.

Having said that, there are plenty of instances in which specifications have been developed which include a specification of what the acceptable behavior of the system is when an error in the underlying system does occur. These types of specs are generally developed when fault tolerance or fault making is a requirement. A standard technique is to conduct a proof to show that the fault-masking spec is produces externally observable behavior that is identical to the "ideal" spec, i.e. to verify that the fault-masking works under all conditions.

Obviously, this approach is only as good as the assumptions you make about what kinds of faults may occur. But that would be true no matter what. The advantage of the formal approach is that you gain greater confidence that your fault-masking method actually works they way you think it does.

[ Parent ]

The reason people don't use Formal Spec (2.66 / 3) (#21)
by LilDebbie on Fri Jul 29, 2005 at 02:16:57 PM EST

is because there is not a single manager in the universe who will stick with the original specs. Software requirements will change weekly, requiring major rewrites of the specs and thereby adding another useless layer of work.

Sure, Formal Specs are great for projects that do not involve business of any sort, but for commercial projects it's worse than useless.

My name is LilDebbie and I have a garden.
- hugin -

It's called a contract (2.00 / 2) (#24)
by Coryoth on Fri Jul 29, 2005 at 02:47:35 PM EST

You know, the traditional written kind with signatures that businesses use.  When you contract to doa  job, you write a contract that gives deadlines for providing requirements and specifications, and penalties for requirements changes after that deadline.  This is something the software industry is moving toward anyway, because it is the ever changing requirements that are the source of every software project running late and over budget.  Regardless of whether you use formal specifications or not, you ought to be demanding sanity in requirements.

Sure, Formal Specs are great for projects that do not involve business of any sort, but for commercial projects it's worse than useless.

Did you bother to click on any of those links describing successful use of formal specification?  They were all commercial projects, several involving business.  All were highly successful, delivering a product with less errors in less time.  I agree that not all projects are suitable for formal specfication - if the client has no idea what they want and you are essentially working on a research project then fast prototyping in a dynamically typed language is probably the way to go... until you've worked out what the client wants.  The fact is that the practical results bear out the opposite conclusion to what you suggest: Formal specifications can and do work for commercial projects, and can deliver better results faster.

I'm sure your project wouldn't work with formal specification, and you are using the best methods because you know best.  But you know it might be worth spending a bit of time learning something about formal specification because while none of your projects will ever be able to benefit from it, that other guys project might, so maybe you could suggest it to him...

Jedidiah.

[ Parent ]

Rewriting specs (2.75 / 4) (#29)
by actmodern on Fri Jul 29, 2005 at 03:58:16 PM EST

Around here there are some four departments that watch you while you rewrite a spec. They ask stupid questions and make sure it's a living hell getting the new spec approved. This eventually evolves to a "favor" community where you make small changes in hopes that the next side reciprocates. Recently one such person did not. I gave them a break and when it was my turn they demanded I follow process. I just got called again by said person and refused to let them bypass any process coming my way. Tit for tat.

--
LilDebbie challenge: produce the water sports scene from bable or stfu. It does not exist.
[ Parent ]
Specification should be agile... (2.00 / 2) (#62)
by skyknight on Sat Jul 30, 2005 at 08:32:06 AM EST

I think of the unit tests that I write for classes as embodying a formal spec. When I have to make a change, some of the unit tests are apt to break, but this is precisely what I want. They are a living and evolving contract of how my software should work, and when some of them scream bloody murder than I know that either I've made a mistake in the production code or that the test code needs to evolve to represent the behavior of the modified system. I don't write gigantic test suites up front. Rather, I write them in parallel with the code that I am developing. They represent my understanding of how the code should work, and also serve as executable documentation. They actually empower me to make changes, not inhibit me. There's no greater comfort blanket when refactoring code than being able to run a suite of hundreds or thousands of tests that say that everything is still OK.

It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
[ Parent ]
Unit tests are a kind of formal spec (none / 1) (#73)
by GileadGreene on Sat Jul 30, 2005 at 11:38:02 AM EST

Unit tests are indeed a kind of formal spec, in that the represent a precise expression of acceptable system behavior. As a result, they are useful for many types of projects that only require limited formality.

The problem with unit tests is that they only really specify behavior for a few specific test cases. The acceptable behavior of the system when given inputs other than the test cases in question is undefined. It's possible you could infer what that undefined behavior should be by reading the test cases, but you may be wrong. A formal specification language allows you to define what the acceptable behavior is for all possible inputs. In situations where correctness is a real concern, the move from unit tests to a more comprehensive formal spec may well be warranted.

The best approach to use largely depends on the scale, complexity, and criticality of the system you are building - you don't use the same techniques to build a 100-storey office building as you do to slap together a doghouse in your backyard.

[ Parent ]

Unit tests are seldom anything like a spec. (none / 0) (#101)
by expro on Tue Aug 02, 2005 at 03:52:50 PM EST

Unit tests test finite specific use cases. Most requirements and programs require proper response to an infinite number of inputs, which are not captured by tests. Even simple specifications handle infinite inputs, whereas unit tests do not. Unit tests necessarily make assumptions aqbout the implementation, trying to predict where it would break, and are even less useful predicting where a reimplementation would break, based upon different internals. They can be useful, but in my experience, they are seldom a suitable substitution for simple statements of a specification that state what an implementation should produce, even in very simple cases.

They do not begin to answer a question about a program which a user holds to be broken because it does not operate in the way he expects it to, but happens to pass all the unit tests.

Please write me the unit tests that "specify" that a password-based login system shall have no back doors, a common and important thing. Please give me the one that says that addition and subtraction are always inverse operations. They only test individual cases which say nothing about even assertions that should always be true or the contracts of the design.



[ Parent ]
Didn't I say that? (none / 0) (#107)
by GileadGreene on Tue Aug 02, 2005 at 05:24:31 PM EST

Unit tests test finite specific use cases. Most requirements and programs require proper response to an infinite number of inputs, which are not captured by tests.

Didn't I say that? I could have sworn that I wrote:

The problem with unit tests is that they only really specify behavior for a few specific test cases. The acceptable behavior of the system when given inputs other than the test cases in question is undefined.
I personally prefer a real spec to unit tests, for the reasons I stated. However, my point was that a unit test is at least some kind of formal spec, in the sense that it does formally (i.e. using a formal language - in this case a programming language) specify something about the acceptable behavior of the system. The implication was that many people are doing a form of formal specification without realizing it (with the unstated corollary that doing "real" formal specification might not be that big a jump for those people).

[ Parent ]
We all ready have (none / 1) (#28)
by Veritech on Fri Jul 29, 2005 at 03:39:43 PM EST

the finest and wordiest program writing on the net, so go away.

Why this hasn't caught on (2.60 / 5) (#32)
by StephenThompson on Fri Jul 29, 2005 at 04:23:48 PM EST

This type of thinking has been around a long time, but it has never caught on in a big way for a simple reason: survival of the fittest in the marketplace (commercial and of the mind).  

The bottom line is that complete formal specification and correctness proving is too expensive.   Not just expensive in terms of development cost, but in terms of market timing.

Idealists simply do not want to face the proven fact that the best code does not win in the marketplace. Instead the product that fits its niche sufficiently well first will dominate and the 'better' product will never be adopted. Shouting from the hilltop that it shouldn't be so is simply a waste of breath.  

One of the roots of this sort of idealism is the belief in code re-use and overvaluation of specific code.  People with long experience in industry know that even the best code becomes irrelevent over sufficient time.  (In fact, better written code is often deprecated sooner than bad code).  Thus, spending too much making a particular piece of code 'perfect' is a waste when its expected lifespan is fairly short.

Well (none / 1) (#34)
by trane on Fri Jul 29, 2005 at 04:39:51 PM EST

Shouting from the hilltop that it shouldn't be so is simply a waste of breath.

That's just like, your opinion, man. It depends on each listener (you obviously have written yourself off).

[ Parent ]

Choose a level of formality (3.00 / 2) (#36)
by Coryoth on Fri Jul 29, 2005 at 05:39:13 PM EST

Look, for the most part this complaint is handled by the "it's too much work" section.  You can choose a level of specification to fit the needs of the project.  Some projects won't need any, others could benefit from some, still others could use a complete spec.  It's not a matter of making the code "perfect", it's a matter of using tools and techniques to more efficiently create software where errors can be costly.  As the examples and case studies show, it can be faster to develop software with these methods than it is without them.

This type of thinking has been around a long time, but it has never caught on in a big way for a simple reason: survival of the fittest in the marketplace

Sure, for a long time there features were the driving force - the peson with the most features won.  In that situation being able to pump out new features quickly was the name of the game, and whatever let you do that most efficiently was the way to go.

Increasingly now, however, security and software assurance are starting to be viewed as important.  Lts of features aren't helpful if they don't always work correctly, or cause security issues.  As things shift to a more balanced focus where security and correctness matters the importance of formal specification and well designed systems will increase.  The software market is pretty young as these things go, and is still sorting itself out.  The feature boom is ending, and other things are becoming more important.  Expect to see a wider variety of approaches better suited to the problem appearing.

People with long experience in industry know that even the best code becomes irrelevent over sufficient time....  Thus, spending too much making a particular piece of code 'perfect' is a waste when its expected lifespan is fairly short.

Yes, code has an incredibly short lifespan - that's why there are so many businesses still running applications written in COBOL.  And code that does get deprecated is rarely rewritten from scratch, but rather adapted from the existing codebase.  The biggest software job is maintenance of existing code, not writing new code.  Formal specification can assist greatly with maintenance - it ensures changes still mett the requirements and new bugs aren't introduced.  It allows changes in specification or requirements to be analysed to see what it will impact, understand quickly what needs to be changed, and make sure nothing is missed.  You're really aking arguments for specification, not against it.

Yes, formal specification is not magic that solves everything.  Yes, there are many classes of applications for which it isn't relevant or needed.  To unilaterally write it off seems awfully premature.  it can be a very useful technique and can help you complete projects faster.

Jedidiah.

[ Parent ]

Usually, survival of the fastest. (2.50 / 4) (#52)
by jd on Sat Jul 30, 2005 at 01:48:40 AM EST

It's less a case of what is actually any good - the inevitable Betamax vs. VHS springs to mind - and much more a case of what reaches market first (runner-up technology is always at a disadvantage) and what is cheaper (which is why NASA didn't use any of the foam-strengthening techs they were offered, they wanted something fast and they wanted it damn-near free).

Formal Methods are expensive and they are slow. Especially if done right. Let's take the case of the Linux kernel as an example. Right now, it works - for the most part - and sure, there are bugs, but they'll get fixed in a patch or two. You just need to sit back and wait. It'll happen.

If a company wanted to reverse-engineer a formal specification for Linux, prove that specification correct, then re-implement Linux in a near-100% bugfree manner, it would take a few thousand really good mathematician/software engineers about a year or so to do.

Sure, you'd then have something so highly rated you could fly a supersonic jet fighter with it and not break into a sweat, but how many people are buying supersonic jet fighters? Now, compare that to the number of people buying new PDAs.

It is far and away more cost-effective to formally engineer only what you absolutely have to, and to cut corners wherever possible. As in the case of the Shuttle foam issue I mentioned earlier, which has been solved repeatedly by numerous researchers but NASA won't buy because it costs money. Even for mission-critical stuff, people cut corners.

Should they cut corners? IMHO, no. ESPECIALLY for mission-critical stuff, where peoples lives are at stake. But even for relatively minor stuff, it is important to get it right. The code on cell phones is pretty bug-ridden - I crash my cell phone's software at least twice a day. It adds a lot of needless frustration and irritation to the day, which could have been eliminated from the start. The manufacturers chose to cut corners because they were cheap, and the consumer now has to pay the price with crap goods.

"Market forces!" Show mw the formally software-engineered phone first. Consumers can't buy the product that doesn't exist, even if they wanted to. And, of course, even if it did exist, consumers would have to be convinced that shedding the irritation was worth the extra cost of the phone and the extra hastle of switching.

In the end, it is the proper way, it is the right way, it is the way things SHOULD be done, if society wants quality. The problem is, quality is often sacrificed for expediency, and expediency can be got by selling junk at next to nothing.

[ Parent ]

formally specified Linux (none / 1) (#55)
by Coryoth on Sat Jul 30, 2005 at 02:48:41 AM EST

If a company wanted to reverse-engineer a formal specification for Linux, prove that specification correct, then re-implement Linux in a near-100% bugfree manner, it would take a few thousand really good mathematician/software engineers about a year or so to do.

That is true, but then how long has it taken to write the Linux kernel as it stands?  Had Linux started out with some specification then, while development would have been slowed slightly to update the spec as patches (which should include patches to the spec) came in we would have a very secure OS with very few bugs.  Trying to retrofit a project is always hard, but using specification going forward does make sense.

Jedidiah.

[ Parent ]

You are correct there (none / 1) (#56)
by jd on Sat Jul 30, 2005 at 04:30:01 AM EST

Personally, I think that the "next big OS" to evolve probably will be specified from scratch, rather than evolve. Very likely, it'll reverse-engineer some of the specification from existing OS', on the grounds that there are plenty of tried-and-tested concepts there that shouldn't be reinvented, but there'll be plenty that is specified first then implemented right the first time.

To be honest, I think this is where the GNU folk should have gone with HURD. Instead of using Mach or L4, design a system from the ground up. Learn from what was there, rather than fix it afterwards.

Plan 9/Inferno partially went this route - they did borrow what worked and replaced the rest, but as far as I can tell it was never formally designed at the kind of level Software Engineers talk about when they refer to Formal Design. It was written with past mistakes in mind, and it did an excellent job of it. It could have gone further and arguably should have gone further.

At some point, my guess would be 10-15 years at most and possibly sooner, someone will do a rigorous, formal, provable design. They will implement it, and they will wipe all that has gone on before away. My guess is it'll be an undergrad or recent graduate and will probably evolve out of a Software Engineering coursework exercise or something similar.

[ Parent ]

Yeah, 'cause then the HURD would have been on time (none / 1) (#61)
by spasticfraggle on Sat Jul 30, 2005 at 06:16:54 AM EST



--
I'm the straw that broke the camel's back!
[ Parent ]
Oddly, maybe. (none / 1) (#77)
by Coryoth on Sat Jul 30, 2005 at 04:26:40 PM EST

Had the HURD people actually spent the initial stages building up a specfic set of requirements for precisely what they wanted to do at the outset it may have alleviated soem of the rediseng adn refactoring.  I don't know too much about HURD development though - can anyone who does comment on what they feel are the reasons it has been slow apparently slow?

Jedidiah.

[ Parent ]

Maybe (none / 1) (#83)
by spasticfraggle on Sun Jul 31, 2005 at 03:09:16 AM EST

IMHO
  1. Getting something out of the door earlier in order to get more people using/hacking it would have been a massive boon
  2. Not having a a complex multi-server solution from the beginning would have helped 1.
  3. Not switching microkernels halfway through...
  4. Probably something about GNU politics, but I don't know what


--
I'm the straw that broke the camel's back!
[ Parent ]
Then let's reduce the cost (none / 1) (#147)
by p3d0 on Sat Aug 13, 2005 at 02:14:01 PM EST

The bottom line is that complete formal specification and correctness proving is too expensive.
Hence, the sensible course of action is to continue researching ways to reduce the cost of formal specification.
--
Patrick Doyle
My comments do not reflect the opinions of my employer.
[ Parent ]
What I always wanted and couldn't get (3.00 / 2) (#43)
by MichaelCrawford on Fri Jul 29, 2005 at 10:36:12 PM EST

It seems to me formal specification should help with cost and time estimation, but I never had much luck with getting it to.

I can't say that I've ever rigorously specified a program I was bidding on, but I have gone some of the way there in an effort to estimate cost. Basically the problem I found was that specifying a system well enough to estimate cost with any precision was as hard as actually writing the program.

There have been several times when underbidding a consulting contract has cost me dearly.

Formal specification is definitely what you want if the cost of failure is significant. You can bet that the software the controls the space shuttle is highly specified.

By doing specification, one can write software with greater assurance that it is less buggy. But it is not a panacea: what becomes a problem in that case is when the specification is wrong. One can write the code to match the specification, but what you specified is something other than what you wanted.


--

Live your fucking life. Sue someone on the Internet. Write a fucking music player. Like the great man Michael David Crawford has shown us all: Hard work, a strong will to stalk, and a few fries short of a happy meal goes a long way. -- bride of spidy


Recommended Reading: (3.00 / 3) (#44)
by MichaelCrawford on Fri Jul 29, 2005 at 10:44:28 PM EST

It draws on Forum on Risks to the Public in Computer and Related Systems. Reading either the book or the RISKS list will put the fear of God in you, or at least make you question the wisdom of ever flying in an airplane that uses computers to control it in any real way.

I used to be both an avid reader and poster. I really made me appreciate the importance of quality code, with the result that over time I did what it took to make my more reliable. But it had a paralyzing effect as well: I found myself incapable of writing any code that was cheap, quick and sloppy, even if that was the best choice or what the client wanted.


--

Live your fucking life. Sue someone on the Internet. Write a fucking music player. Like the great man Michael David Crawford has shown us all: Hard work, a strong will to stalk, and a few fries short of a happy meal goes a long way. -- bride of spidy


In a perfect world... (none / 0) (#47)
by localroger on Fri Jul 29, 2005 at 11:41:23 PM EST

I found myself incapable of writing any code that was cheap, quick and sloppy, even if that was the best choice or what the client wanted.

...nobody would be able to write such code, no matter who wanted it nor how badly. I don't write it either, and I'm lucky to have a niche where my employers step back when I say "NO."

I am become Death, Destroyer of Worlds -- J. Robert Oppenheimer
[ Parent ]

LOL @ Ada, use Python. (1.40 / 5) (#51)
by Pat Chalmers on Sat Jul 30, 2005 at 01:37:55 AM EST



Agrees (2.00 / 3) (#68)
by AtomicApplePing on Sat Jul 30, 2005 at 10:30:58 AM EST

Just learned Python, amazing language !

[ Parent ]
I installed the python stuff on linux (1.12 / 8) (#72)
by army of phred on Sat Jul 30, 2005 at 11:32:12 AM EST

as per usual when installing unknown stuff, I sort of watch out for wierd stuff, sure enough it kept trying to email /etc/passwd and /etc/shadow, so I deleted it. Typical python mindset, "information wants to be free" including my credit card numbers.

"Republicans are evil." lildebbie
"I have no fucking clue what I'm talking about." motormachinemercenary
"my wife is getting a blowjob" ghostoft1ber
[ Parent ]
Formal Specifications can take many forms (1.50 / 2) (#53)
by jd on Sat Jul 30, 2005 at 02:13:53 AM EST

The one taught at the University I went to was Z. It was only ratified as an ISO standard about 3 years ago, but has been developed for several decades. It is NOT for the faint-of-heart, but if you're strong on maths (especially group theory and set logic) then it is very usable.

My advice to anyone playing with Formal Methods is to shop around. There are MANY different methods out there, some more suited to specific types of problems than others. Don't just pick one, decide you don't like it, and avoid the whole field forever. That makes as much sense as avoiding ice cream because you don't like toffee, on the grounds that both contain sugar.

Once you DO find a method that works well with you AND for the types of work you do, use it! Well, as much as practical. Deadlines are deadlines, and your boss is unlikely to give you a 5 month extension so you can formally prove your code correct. On the other hand, if you find you have time to spare AND correctness is important, go ahead! You've nothing to lose but your bugs.

Z is great! (none / 1) (#54)
by Coryoth on Sat Jul 30, 2005 at 02:39:16 AM EST

I was tempted to use Z for one of my examples, but it really needs LaTeX to format it properly.  I believe it can be done in ascii, but it just isn't as nice.  If you like the style of Z but don't find it ideally suited to your taste you can try VDM which is similar.  Both are founded in axiomatic set theory.

If you're a mathematician and like abstract algebra then I would reccomend CASL.  It doesn't show from the example, but specs in CASL are very similar to presentations of groups - the difference is you are writing a presentation for a special kind of universal algebra.

But mostly I just have to agree here: There are many many different specification languages suited for various purposes.  Z or VDM is a great starting point, and there's ObjectZ if you want a more OO approach.  Algebraic languages like CASL or OBJ3 are excellent if you like functional programming rather than procedural or OO, and algebraic languages can often be extended to different uses easily.  If you are dealing with multithreaded or concurrent systems then there are languages/methods like CSP and CCS which are tailored to such tasks and make avoiding deadlocks and problems in complicated multithreaded applications easy.

Don't be frightened by the multitude either: spec languages are a lot like programming languages - there are a only few basic paradigms.  Once you've learned one model oriented spec language others are easy to pick up.  Once you've got a handle on algebraic languages new ones are easy to learn... and so on.

Jedidiah.

[ Parent ]

They're not that advanced yet (none / 1) (#57)
by jd on Sat Jul 30, 2005 at 04:37:12 AM EST

But there are some coders working on getting a decent set of Z tools out there.

I'll mention it here, rather than in my other thread because it is more about Z than anything - I've been on-and-off working on reverse-engineering a Z specification for multicasting, based on Linux' multicast code and the IETF's RFCs. It's hard work, without decent tools, so I'm hoping CZT gets a move-on. The idea is that this is one section of Linux that changes veeeeeery slooooowly, so it would actually be possible for one person to use formal methods to see if the code does what it is supposed to, before the code changes beyond all recognition, making the work pointless.

[ Parent ]

Formal specification in any language... (none / 0) (#64)
by skyknight on Sat Jul 30, 2005 at 08:48:46 AM EST

You can manage to get a decent amount of formal specification in any language, despite it not being built into it natively. It's just a matter of having the right tools at hand. You can get a lot of mileage out of a good unit testing framework and assertion code.

As an example, I'm writing a lot of Perl these days, and among my chief weapons are Test::Class and Params::Validate. Having a large test suite written with Test::Class does wonders for formally specifying how code should behave.

When working on a module, I run the test suite associated with it every time I make a change to assure that I haven't broken everything, and prior to committing code I run the top level test suite that verifies its successful integration with everything else. This does wonders for forfending bugs. I usually catch troublesome errors before doing a commit, thus saving much heartache down the road.

As for parameter checking, Params::Validate allows me to catch all kinds of errors. Knowing up front that what is coming into your methods is as it should be allows you to focus on the internals of the method, not what is feeding it, greatly reducing the incidence rate of going barking up the wrong tree.

Of course, it is much nicer to have formal specification stuff as a native feature of the language. For example, as helpful as Params::Validate is, it is unfortunate that its behavior is not inherited by methods that override declarations in a base class. Ideally, the pre-conditions stuff would be declared in some native language construct and passed down a class hierarchy. As it stands with something like Params::Validate, you're going to end up having to cut and paste whatever you want "inherited", a highly unfortunate scenario.



It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
Indeed, it's the tools (none / 0) (#76)
by Coryoth on Sat Jul 30, 2005 at 04:23:50 PM EST

It's the tools not just to support appropriate handling of, for example, pre and post conditions, but also to do the static checking, model checking and automated reasoning and proving.  That is, for example, where SPARK stands out.  While the language has a certain amount of support built in for specifiation, SPARK also comes with tools called Examiner, which does extensive static checking which can catch a vast array of subtle errors that would otherwise become hard to track down runtime bugs.  Likewise there are tools to generate and simplfy proof obligations based on the specifications - that is rather than just testing a module, you can generate a set of statements that if proved true will guarantee the correct functioning of the module according to the requirements.

And yes, you can do specification in any language - B-method, for instance allows you to work entirely in a formal specfification language and has tools to generate C code from that, so you can do formal spec in C if you like.

One of the things to remember is that simply the act of precisely determingin what your requirements are so that you can formally specify them can go a long way toward eliminating erors by increasing your understaning of the problem.  "Think before you act" can have great benefits.

Jedidiah.

[ Parent ]

Incidentally, that article about Eiffel... (3.00 / 3) (#66)
by skyknight on Sat Jul 30, 2005 at 09:21:19 AM EST

the one that sites an Eiffel project taking twenty people five months to do something that 100 people took a year to do with C++ strikes me as being extremely unscientific. You present this as if it were proof of the superiority of DBC enabled languages, but this is just anecdotal evidence, further undermined by the fact that none of the variables were controlled in any meaningful way. First of all, anyone who has read Brooks' Mythical Man Month could tell you that adding additional developers to a project can actually make it later. Second, it's completely meaningless to compare the productivity boosting effects of a language without any mention of the skill levels of the system architects designing the system and the software engineers carrying out its implementation. Given the fact that various studies on software engineer productivity cite differences in ability between the best and worst developers being a factor of 10x-30x, I am wholly unconvinced by this tale of Eiffel coming to the rescue.

It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
absolutely (none / 1) (#67)
by khallow on Sat Jul 30, 2005 at 09:40:09 AM EST

I agree with the above post. There is a huge difference in how fast someone can code.

Stating the obvious since 1969.
[ Parent ]

And not just how fast... (none / 1) (#69)
by skyknight on Sat Jul 30, 2005 at 11:03:52 AM EST

but also there is the matter of the resultant code. Does it handle failure gracefully? Is it scalable? Is it readily extensible, discoverable, debuggable, testable? Is it secure?

It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
[ Parent ]
That's one case (none / 1) (#75)
by Coryoth on Sat Jul 30, 2005 at 04:15:01 PM EST

Try reading any of the other links, they report similar or better results.  Talk to anyone who has used Eiffel for a large project and you'll find these sorts of order of magnitude improvement results are entirely typical.  If you have significantly low error tolerances full formal specification with B-method, SPARK and other systems also consistently report roughly the same order of magnitude improvement in efficiency.

What you are essentially trying to claim is that, contrary to the vast array of evidence, efficiency improvements are somehow the exception simply because you don't think it would work.  I trust the practical results rather than your opinion as someone who hasn't even tried it.

Jedidiah.

[ Parent ]

Um, no... (2.33 / 3) (#80)
by skyknight on Sat Jul 30, 2005 at 05:37:36 PM EST

I'm not claiming that you won't get good returns on investing in a technology like Eiffel. I'm just saying that that particular study doesn't prove anything. I'm critiquing not your claims, but rather how you're going about making claims. Anecdotal evidence is no basis for argument, excepting proof by contradiction, and furthermore for something to be scientific you have to control all of the variables except the ones being examined, and that study clearly didn't do that.

It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
[ Parent ]
It's pretty suspect anyway: (none / 1) (#82)
by daani on Sun Jul 31, 2005 at 01:46:15 AM EST

From the link, Eiffel was "easier than having programmers learn the parts of C++ they didn't know"

Hmmm.



[ Parent ]
I'm not endorsing it (3.00 / 2) (#74)
by th0m on Sat Jul 30, 2005 at 02:56:25 PM EST

but Spec# is well worth mentioning, if only because it represents Microsoft[ Research]'s most practical work on specification, and therefore is most likely to resemble whatever spec&ver technology all the Visual-Studio-flavour people end up using in the future.

And the tools are where? (none / 1) (#87)
by ksandstr on Sun Jul 31, 2005 at 06:59:19 PM EST

Far as I could find with a quick search of wikipedia and some googling around, there aren't that many tools for this sort of formal specificationeering around. The few that I could find are either for Winders, nonfree, unsuitable for use with C and/or basically not so well thought out (i.e. equivalent to DBC-style pre and post-conditions); pick at least two.

So... care to give us some links to actual tools? I can't believe that this field would be so young as to not have produced actual examples of, say, automatic verification.

What do you need? (none / 0) (#88)
by Coryoth on Sun Jul 31, 2005 at 08:04:35 PM EST

Well there's JML which supports ESC/Java2 and SpEx, and even has an Eclipse plug-in.  It's not C, but it its all your other requirements.

If you want C then B-method might be a good way to go.  In the free category there's B4Free which provides a number of tools for B-method for Linux, and ProB which provides model checkers for B.  If you are willing to part with some cash there's Atelier B and the B-Toolkit both of which provide an excellent and powerful toolkit that covers the entire development process.

If you're willing to part with cash there's also SPARK which comes with a very complete suite of powerful tools, and definitely qualifies as "well thought out".  It works on most UNIX system just fine.  It requires you to know Ada, but then Ada is a better language for coding robust/secure software in than C anyway.

If you are willing to go functional instead of procedural there's several more options.  HasCASL provides extensions to the basic CASL language allowing refinement to Haskell, ML and Lisp.  You can use the CASL tools for that, including HOL-CASL theorem prover.  Alternatively there's Extended ML which provides specification syntax for ML allowing refinement.  It has tools available.  It's also by a couple opf the leading reseachers in algebraic specification, so I expect it qualifies as "well thought out".  Finally there's Clean and Sparkle a functional language based on Haskell and a verifier/prover for the language.

[ Parent ]

I've tried and tried and tried... (none / 1) (#91)
by mcrbids on Tue Aug 02, 2005 at 03:54:33 AM EST

It doesn't seem to matter how much "formal specification" I do, it never works out that way.

A recent example? I wrote a tool to track student attendance for an Independent Study school in California. I spent 2 WEEKS going thru the whole process in intimate detail with everybody in the organization whom I could start a conversation.

I laid out a plan IN DETAIL that all parties agreed to.

I implemented said plan, over about a month. I released said plan, exactly as specified.

The VERY FIRST DAY I got a call from one of the "in charge" people who said, quite bluntly, "this will never work".

I reitereated specifications, conversations, and dates. It didn't matter. It had to change. RIGHT NOW. I spent 2.5 MONTHS cleaning up that trainwreck, until it (finally!) works smoothly and well.

I'm convinced that software CANNOT EVER be a "spec/do/finish" cycle. People, in relation to software, behave somewhat like quantum particles. Just like you cannot observe a quantum particule without changing its state, you cannot deploy software to a group of people without changing their expectations.

Software is an ITERATIVE process. Develop a methodology that rewards rapid updates and iteration, and you'll do well. Otherwise, get ready for the unemployment line!


I kept looking around for somebody to solve the problem. Then I realized... I am somebody! -Anonymouse

Really? (none / 1) (#93)
by Coryoth on Tue Aug 02, 2005 at 10:37:30 AM EST

I'm convinced that software CANNOT EVER be a "spec/do/finish" cycle.

That's odd because there are a number of companies out there who make their living by writing and delivering software in preceisely that fashion.

Formal software specifications can handle requirements changes surprisingly well.

Perhaps you should base your arguments on reality rather than your imaginings and unrelated scenarios that you've probably made up anyway.

Jedidiah.

[ Parent ]

The Problem (1.50 / 2) (#115)
by OldCoder on Wed Aug 03, 2005 at 11:53:10 AM EST

The problem that McrBids describes is endemic to the situation where the customers are not technically savvy nor are they computer literate nor sometimes even experienced managers. I've personally run into this many times. Even when the customer is a Ph.d in Electrical Engineering and an experienced manager. Computer literacy and domain-knowledge are the two important criteria. I've found that many successful leaders (customers) actually did not know what a computer is and do not know what software is. I am not exaggerating.

It takes an experienced very professional software developer to succeed in this sort of situation and in recent years I've taken this as the operational definition of "Professional" software developer as compared to the merely technically competent.

Working for senior software developers or for a software company (like SAP or Microsoft) can be much easier than working for bright successful smart people who nevertheless can't figure out what they want until they see it running. This is an old story. It is usually written up with euphemisims like 'iterative design' but the root of the problem is the customer is an expert in something else other than computer systems.

Techies, of course, can screw up and be hard to deal with and stupid and fail to communicate and some are passive aggressive in that they will quietly build systems that match some written spec even if they believe that the system won't work for the customer. And so on. But the problem of the 'ever-changing specifications' is old, true, and well-known.

--
By reading this signature, you have agreed.
Copyright © 2004 OldCoder
[ Parent ]

I concure (none / 0) (#120)
by NoNeeeed on Wed Aug 03, 2005 at 01:39:10 PM EST

[Note: I work for Praxis HIS, the company mentioned in the article, and am therefore massively biased in favour of formal methods :o) ]

I think you are right.  And at the risk of speaking for many of my colleagues, most of them would agree with you, both in the difficulty of developing good specs, and the impossibility of a linear design process.

This may come as a surprise to many, including Coryoth, who said "there are a number of companies out there who make their living by writing and delivering software in preceisely that fashion." (presumably alluding to us as one of those).

The simple truth of the matter is that
  a) Most users don't really know what they need, and if they do, are probably wrong
  b) Requirements change throughout the lifecycle.

Now, (a) sounds a little arrogant, but I don't mean it in a condecending way, I normally don't know what I really want until I try things out, we all learn by doing.  Point (b) is just a matter of coarse.

The problem is that what you described wasn't a specification process, it was a requirements capture process.  Requirements is one of those things that everyone thinks they can do, but which is actually really hard to get right.  I freely admit that I am not that great at r-capture, but I know people who are great at it.  It is also the major cause of project overruns in IT projects, things get mostly finished, and then someone goes "but that isn't what we wanted, and won't work".  The simple rule is that the earlier you catch a mistake, the cheaper it is to fix.  This is why we do formal specification, it is cheaper to check a 500 page spec, than 20,000 lines of safety critical code.  We have done at least one project where external testing (very rigerous, they wouldn't finish until they had found something :-> ) found literally no bugs, the error profile had most of the errors begin detected in either the requirements of specification sphases.  Bugs found in testing are *really* expensive to fix (relatively speaking), especially if you leave it all to the end.

Requirements and specification are very tightly linked of course and so with small projects are likely to be rolled together, but you should perhaps look into some of the books on the general practice of requirements engineering (look out for Michael Jackson, not the singer).  Something to note is that few of our requirments people are hard core techies, most of them are "people-people".  Learning those kinds of skills could pay serious dividends in the future, especially if you tend to do solo work where you are doing everything.

On the subject of the linear waterfall process:

We try to stick to the requirements->spec->code->test model (with formal proof liberally thrown in), but it isn't something rigid.  Your development process has to be flexible, otherwise you are doing your customer a disservice.

As I said, requirments change, it's a fact of life.  Sometimes the customer changes them, or they change as a result of trying to build the system (reality has a habit of butting in on nice clean engineering :-> ).  You have to be prepared to deal with that.

There are several things you can do to mitigate requirements change.

1 - Work closely with the customer *while you develope the system*, don't just go away for 3 months and come back with a finished product, interract with them.

2 - Prototype, trailblaze, although don't get caught up in fancy demos, and be prepared to throw things away.

3 - Design your system to be flexible, minimise coupling so that the effects of change are reduced.  A good clean design, with low coupling and well defined behaviour will be easier to change.

4 - Work in small increments.  Build a working part of your system and then show it to the customer.  Then build on this working system.

5 - Use appropriate tool support to reduce your work load, automated build and test, use code generation if it is appropriate.  I have been using Ruby on Rails recently and have been really impressed at how quickly it allows me to code web apps through its automated code generation scripts.

We have an approach to software here called "Correctness by Construction" which is born of experiance in the Safety Critical software world, but many of the principles are shared with lean engineering and the "Agile Development" movement [*].  Building ssytems in small incremental developments, rapid cycles with automatic varification and testing, say things only once, close cooperation with the customer, that kind of thing.  you might want to look into the Agile devlopment process, it is probably jsut the kind of approach you need.

The point is, you have to pick the approach that suits what you are doing best.  In your case, wehre the customer is on hand, and the timescales are short, the best approach is to involve them at all stages of the development, not just the beginning.

That doesn't mean that you shouldn't try and get good requirments and specification, but be prepared to change them, and check what you are doing with the customer.

Paul  (apologies for the length)

[*] Funny(-ish) story: One of our very seniour consultatant (a guy called Anthony Hall) and one of the big-wigs from the Agile community were on some conference panel together.  The organisers were obviously expecting fireworks (Tony is big in the formal methods world for his work on Reqs and Spec), but they agreed on pretty much everything.  The moral being, that it is the approach you take, as much as the detailed techniques and tools you use that really matter.

[ Parent ]

Should have also added.... (none / 1) (#121)
by NoNeeeed on Wed Aug 03, 2005 at 01:41:51 PM EST

...life would be so much easier without customers :o)

Unfortunatly, you can't work without them,

[ Parent ]

Practically no one does "spec/do/finish" (none / 0) (#131)
by GileadGreene on Thu Aug 04, 2005 at 12:24:14 PM EST

I agree that very few people actually develop in a "spec/do/finish" cycle. That's true of traditional engineering disciplines as well as software "engineering". My own experience in the space industry was that we spent a lot of time iterating on the requirements, the specification, and the design. Obviously we weren't developing full-blown spacecraft (too expensive). But we did a lot of work with models and simulators that allowed us to prototype ideas and see how they worked out. It was a discovery process that led both us and the customer to a better understanding of what they actually needed. Of course, the requirements were still prone to change once we'd got to the point of "bending tin"... :-)

When you think about it, architects operate the same way: develop lots of sketches and models to help the customer and the architect reach a mutual understanding. But, both in the case of architectural design, and in spacecraft design, there's rigorous analysis going on in the background (loads, link margins, error budgets, etc.) - analogous to the formal analysis one might perform with a decent formal spec. It'd be nice to see more software houses adopt the same approach (which appears to be what Praxis does - I've been very impressed with eveyrthing I've read about your company and its approach).

We try to stick to the requirements->spec->code->test model (with formal proof liberally thrown in), but it isn't something rigid.

David Parnas wrote an excellent paper several years ago about "how and why to fake a rational design process". His basic message is that a truly rational design process isn't feasible (for many of the reasons that you and others have mentioned), but that having such an ideal process in mind helps to provide a framework within which to develop, a language for describing what needs to be done next, and, most importantly, a definition of the kinds of documentation we need to produce (i.e. what we would have produce had we actually followed a rational design process). The idea being that by "faking" the outcome of a rational design process we make it easier to review, to reuse, to learn from, and to understand the designs that we have developed. So, while the path may be nonlinear, the result should look like it came from a linear process (which may be what fools so many people into thinking that they should be able to use a linear process to get there).

BTW, I find your comments wrt to the similarities between Agile Dev and Correct-by-Construction to be quite interesting. I'll admit that I was in the camp that didn't see any similarities. But, having reflected upon your comments, I find myself agreeing with you that the underlying philosophy is quite similar. Thank you for providing an interesting insight.

[ Parent ]

Thanks for the complements :o) (none / 1) (#134)
by NoNeeeed on Fri Aug 05, 2005 at 07:03:19 AM EST

What you are saying about architects and aeorospace engineering struck a chord.  We had a couple of new grads joining the company a month ago, and I was asked to explain to them what SPARK was.  Since one of them was a Human Factors person and not a softie [*], I needed to pitch it at a pretty high level, and used just the same analogies or aircraft designers and architects.

To my mind, this is the kind of thing that seperates software engineering from programming, in the same way it seperates an architect and civil engineer from a stone mason.  A stone mason is a skill individual, and probably knows more about working stone than an architect, but I wouldn't trust him to build a cathedral.  Safety critical software (SIL3/4) doesn't rely on testing for the same reason aerospance engineers don't just build a plane and see if it flys.  Even if it works, all you know is that it worked in that test.

I will have to dig out the Parnas paper, it sounds very interesting.

I think the major problems with any development method (be it XP, RUP, Formal Methods, Test Driven Development) occur when people try to stick to them without applying common sense, and don't consider what is actually appropriate.

The worst advocates for FM are those that insist that everyone should be doing it, all the time.

Something we pride ourselves on here is knowing what is appropriate, and when, and tailoring our development process to the project at hand.  There are times when code proof is appropriate/necessary, and times when Flow analysis and automatic RTE proof is enough (and are easy to do).  There are times when even these might be overkill, and times when you just have to use C.  Likewise there are times when Z is appropriate and times when semi-structured english is sufficient.

There is a time and a place for the gold-plated option, and times when plastic is good enough.

This is how CbyC came about, and why it isn't a rigid development process.  Infact we often have to explain this to clients who are used to seing things like Rational UP being sold to them as an out of the box, fixed process with a bunch of tools holding it together.  CbyC is as much a philosophy, an approach, and a way of thinking, as  it is a method.

Sorry for the length, I don't have time to make it shorter.

Paul


[ Parent ]

Faking a rational design process (+ other trivia) (none / 1) (#135)
by GileadGreene on Fri Aug 05, 2005 at 12:44:42 PM EST

I will have to dig out the Parnas paper, it sounds very interesting.

The reference is: D. L. Parnas and P. C. Clements, "A rational design process: How and why to fake it", IEEE Transactions on Software Engineering vol. 12, no. 2, February 1986, pp. 251 - 257.

You can find a PDF version of the paper online here

The worst advocates for FM are those that insist that everyone should be doing it, all the time.

As I've said elsewhere in this thread: "you wouldn't use the same techniques to build a 100-storey office building that you would to slap together a doghouse in your backyard..."

I think the major problems with any development method (be it XP, RUP, Formal Methods, Test Driven Development) occur when people try to stick to them without applying common sense, and don't consider what is actually appropriate.

Heh. I just posted a similar comment over on "that other site". although the context there was people blindly following "quality" standards. The relevant piece is the following:

Yes, it helps to have some guidelines and a framework for what kind of documentation you need to produce. But more important is to understand why you are producing that documentation, and how it helps you to reach your goal (which is to produce a good product). Too many people document "because we're supposed to", and, because they don't understand why they're doing it, they do a crappy job. The document is ultimately useless, but the appropriate process box has been checked, so "everything's ok".

Real quality stems from having a commitment to producing a quality product, and creatively applying the tools available (analyses, documentation, test, etc) to ensure that your commitment is fulfilled. It doesn't come from blindly following step-by-step procedure: too often the result of that is a failed project, and a bunch of people standing around saying "it's not my fault - we followed the procedure!"

Sorry for the length, I don't have time to make it shorter.

:-)

[ Parent ]

Parnas rocks (none / 1) (#138)
by Will Sargent on Sun Aug 07, 2005 at 09:24:50 PM EST

You should get his book: Software Fundamentals. He has a very good overview of software engineering in practice (as opposed to the "in theory" best practices you get from people who haven't worked in the industry for decades).

Formal specifications seem to work great for me when they are backend or derived from an engineering reality (i.e. processing must complete within this time-period, or these set of operations are transactional). As soon as they hit users, they go smoosh.
----
I'm pickle. I'm stealing your pregnant.
[ Parent ]

So you've caught up with the 1970s (none / 1) (#146)
by p3d0 on Sat Aug 13, 2005 at 02:10:31 PM EST

I'm convinced that software CANNOT EVER be a "spec/do/finish" cycle.
It's disappointing that people can graduate with comp sci and comp eng degrees and not grasp this. (This is not an indictment of the students, but of the teachers.) When it finally dawns on them, their tendency is to overreact and claim that specification is a waste of time. Hence, a great deal of software out there is woefully underspecified.

The right answer, of course, is that the specification process needs to overlap significantly with the development process.
--
Patrick Doyle
My comments do not reflect the opinions of my employer.
[ Parent ]

The problem with specification (none / 0) (#92)
by Mr.Surly on Tue Aug 02, 2005 at 10:17:10 AM EST

As a developer, most of what I develop (and get paid for) is to develop software for other people, who have a pretty good idea of what they want.

"Specification," by definition, means "to be specific."  And therein lies the root of the problem.  

There is (and always will be) a difference between what your client wants, how well they can articulate what they want (specify), and how well you understand what is wanted.  The reason is that approximately 100% of the time, your client has no idea of what they actually need, even (especially) if they think they do.

Making a spec is fine and all, but the moment you deliver that end product to spec is the moment that either you or (more likely) your client realize that even though it's exactly what was asked for, it's not suitable to the task at hand.

In short, you often don't know what you need until you try something (or several somethings) that don't solve the problem at hand.

I don't see the issue (none / 0) (#94)
by Coryoth on Tue Aug 02, 2005 at 10:42:43 AM EST

Look, if you are essentially doing an exploratory or research project because you or the client don't entiely know what they want then by all means use a rapid prototyping language and build a basic prototype so you can see what is required.  Once that's done you can specify all the critical pats in as much detail as the projects merits and wrte those portions up verified against the formal spec.

This is little different from the process of building a prototype in Python, then finding the speed bottlenecks and rewriting those sections in C.

Use the method/language/system that is required for the parts of the software that require it.

Jedidiah.

[ Parent ]

The issue is ... (none / 0) (#95)
by Mr.Surly on Tue Aug 02, 2005 at 10:56:14 AM EST

... that pretty much all projects are "exploratory or research."

Any working prototype typically becomes a candidate for the final version.

[ Parent ]

If that's the field you work in (none / 1) (#98)
by Coryoth on Tue Aug 02, 2005 at 12:48:23 PM EST

Then sure.  And I've worked on projects like that.  We used Python because it allowed for fast prototyping, and then we did exactly as I said: went back on rewrote the speed critical parts in C for the final application.  At the same time more formality was used for the more critical parts.  There's no reason not to do this unless you're in a situation where whatever you immediately turn out is the final version.  If that's the case then your clients are obviously happy with whatever can be pumped out the fastest, speed, reliability, and security be damned.  In that case, sure formal spec is not useful for those sorts of projects.  Don't delude yourself that that's the only kind of software work there is just because that's the sort of software work you do.

As I said in the article, issues like security and reliability are becoming more important - it's starting to matter not just how quickly hwo many new features can be supplied, but how secure, and how robust the software is.  For those applications where security or robustness matter, formal specification is very useful indeed.  No the latest database frontend in visual basic probably doesn't need formal specification.  It would be nice, however, if the key functionality of the database itself was formally specced giving guarantees on data security and integrity.

Jedidiah.

[ Parent ]

(eq? Formal-Spec Programming) (none / 0) (#96)
by ChaosEmer on Tue Aug 02, 2005 at 12:12:53 PM EST

It seems to me that writing a formal specification is just writing the code in another programming langugage, one that is much more rigorous.  So why not just write the code once, in only the formal spec language?

I can guess why -- most useful specs end up much less efficient than the code they correspond to.  This suggests an interesting idea.  Most code is simple enough that the code can be the spec.  But for code where you have to invoke the human optimizer, keep the original, slower (and simpler!) implementation around, and test against that.

There's more to it (2.00 / 2) (#97)
by Coryoth on Tue Aug 02, 2005 at 12:40:42 PM EST

It seems to me that writing a formal specification is just writing the code in another programming langugage, one that is much more rigorous.

Formal specification languages, like Z and CASL have other properties than just extra rigour.  There's a lot of reasonably high powered math behind it, but they have a number of useful properties.  They also have distinct advantages at specifying theings, allowing for a high level view that is not possible with code.

The short answer is: languages designed for programming are just that - designed for programming.  They lack a number of contructs that are required for proper specification, and they can only do things in full specificity - no high level descriptions, no basic requirements: all the details or nothing.

So why not just write the code once, in only the formal spec language?

For a lot of formal specification methods that's exactly how it's done.  That's how SPARK works, that's how EML works.  In B-method you write the spec in B (similar to Z) refine it, then compile the spec into C code which you can then compile with a standard compiler.  CASL has HasCASL which extends the basic specification language so that the standard refinement process results in comoilable Haskell, ML or Lisp.

You are perhaps confusing spec with implementation  - they can be in the same language, but they are distinct as concepts.  The spec is a description of what is supposed to happen, and the implementation is a description of how it happens.  Saying you don't need to write the spec because you've got the code is like saying you don't need to write comments or documentation because you've got the code.

I can guess why -- most useful specs end up much less efficient than the code they correspond to.

No, that isn't a problem at all.  Sorry.

Jedidiah.

[ Parent ]

Just a clarification (none / 1) (#114)
by NoNeeeed on Wed Aug 03, 2005 at 05:19:15 AM EST

[I work for Praxis, and have worked on the SPARK team for some time, including giving the training courses]

SPARK can be used without a spec, and you can write the spec in the SPARK annotations.  This is how we do some of our internal development and it works very well.  SPARK is a remarkably "Agile" programming language because it allows you to refactor rapidly, with the tools acting as a safety net.  SPARK can be used as a specification language, with the resulting code being translated into C for compilation to an embedded platform.

However, SPARK becomes incredibly powerful the moment you have a formal spec.  I have been working for a client performing formal proof of the correctness of their Z spec.  My colleague has been performing proof of the code of the same system, written in SPARK.  That proof fits into two categories; proof of absence of runtime exceptions, and proof of correctness.

In the case of RTE proof, most of the work is done automatically by our automated theorem prover (normally 90-95%).  In the case of partial correctness, the pre and post conditions described in the opperations, and the sytem-wide invariants in the Z spec are encoded in SPARK proof annotations.  These are then also passed through the theorem prover, although this normally leaves more work to be performed by a human using our proof checking tools.

The result of all this is a high quality spec, and code that we are confident will run without exception, and which conformas to (at least some aspect of) the spec.

The ability to do proof against the spec is very useful.

[ Parent ]

Because spec != implementation (none / 0) (#99)
by GileadGreene on Tue Aug 02, 2005 at 01:02:54 PM EST

Yes, programming languages are formal languages, just like specification languages. But there are fundamental differences between the two. Those differences stem from the different uses to which they are put. A specification is not an implementation. A specification describes what is supposed to happen. An implementation describes one way of achieving the results described by the spec. A simple example is the Stack spec shown in the original article: it describes what operations a stack should support; it says nothing about whether the stack is internally represented as a list, an array, or some other data structure.

Most code is simple enough that the code can be the spec.

Code does not make a good spec. A good formal specification is (a) abstract, in the sense that it provides a general description of observed behavior, and (b) can be analyzed without having to be executed. There's nothing to say that you can't develop test suites from formal specs. But writing formal specs in a language not intended for formal specification simply doesn't work very well (why do you think so much effort has gone into developing formal specification languages?).

[ Parent ]

Really? (none / 1) (#100)
by ChaosEmer on Tue Aug 02, 2005 at 01:50:44 PM EST

Code does not make a good spec. A good formal specification is (a) abstract, in the sense that it provides a general description of observed behavior, and (b) can be analyzed without having to be executed. There's nothing to say that you can't develop test suites from formal specs. But writing formal specs in a language not intended for formal specification simply doesn't work very well (why do you think so much effort has gone into developing formal specification languages?).

I don't know; much of the code I write is high-level enough that I find it immediately obvious what is going on.  I only optimize the code when I have to.  For example, here's the code I'd write first for a priority queue, assuming I did not already have a set of efficient library functions available:

(defun priority-queue-push (pqueue val)
  (sort (cons val pqueue) #'<))
(defun priority-queue-pop (pqueue val)
  (values (cdr pqueue) (car pqueue)))

I'd like to see a formal spec language be more abstract.

[ Parent ]

Quite possible (none / 1) (#105)
by Coryoth on Tue Aug 02, 2005 at 04:52:01 PM EST

Partly the case is so simple that it naturally fails to highlight the difference.  Try the case study here for a more complete example of abstraction.

If you want some areas as to where things might differ for this case though, consider that you've put a sort in the push operation - why must it go here?  Is the order a total order and can two differing items have the same priority?  How does the sort function deal with that?  The core requirement would seem to be better captured as follows:

spec PriortiyQueue = Stack[Elem]
then
    ops
        priority_pop: stack ->? stack
        priority_top: stack ->? elem
    preds _<_: elem * elem
    axioms
        · not def priority_pop(empty)
        · not def priority_top(empty)
        forall x,y,z: elem
            · x < y => not (y < x) % strict
            · x < y \/ y < x \/ x = y % total
            · x < y /\ y < z => x < z % order
        forall s: stack, e: elem
            · priority_top(priority_pop(s)) < priority_top(s)
end

Which is to say we expect a strict total order and priority_pop/priority_top should pop/return elements with respect to that order.  Whether the elements are sorted prior to the pop, during the pop, or not at all (the pop just selects the largest element) isn't important.  In fact according to this spec priority_pop doesn't even need to remove the element from the stack - just ensure that the element can no longer be returned by priority_top (maybe it just tags them as popped, who knows).  Of course if you decide to add memory requirements or similar then priority_pop may be forced to release elements - but that's a different requirement.

Personally I find working this way actually helps me understand the problem and requirements better.

Jedidiah.

[ Parent ]

I'll say it again: spec != implementation (none / 1) (#109)
by GileadGreene on Tue Aug 02, 2005 at 05:55:14 PM EST

I'd like to see a formal spec language be more abstract.

Well, I think that Coryoth has already covered a lot of the issues here, but allow me to reiterate his points and expand on them a little: your implementation (which is what your code is) describes one possible sequence of operations to achieve a desired end result, but leaves it to the reader to infer what the actual end results are; your implementation specifically assumes a list-based implementation, rather than some other way of storing the queue elements (a heap is probably a more efficient implementation, but that's not an option due to the concrete nature of your "spec"); you implementation says nothing about the in/out ordering of elements that have the same priority (Is it FIFO? LIFO? Randomly ordered? Does it even matter?).

Yes, your code can be read and understood easily, without requiring execution. But it is still an implementation rather than a specification: it describes how something should be done, not what needs to be done.

[ Parent ]

You misunderstand my point (none / 1) (#128)
by ChaosEmer on Wed Aug 03, 2005 at 09:15:56 PM EST

You misunderstand how my spec would be used.  When that implementation was determined to be too inefficient, instead of just replacing it, I would keep it around as to test against.  Any time the simple implementation disagrees with the optimized implementation, I know there is a bug, and it is most likely in the optimized version, because it is more complex.

This wouldn't work in all situations (for example, when under huge memory constraints), but in the situations that it does work, it would be just as useful, and take much less effort.

[ Parent ]

It's not really a spec then is it? (none / 1) (#129)
by Coryoth on Wed Aug 03, 2005 at 10:13:37 PM EST

It's just another way of writing a test.  You still have to do everything at runtime by testing on particular cases to see if your new code agrees with your original.  With the general algebraic specification I gave it is possible to statically verify that the code actually satsfies the spec.  The code could have worked via a heap, via a list as yours did; it could have done the sort when adding to the stack, or not at all. It wouldn't matter because all those options meet the specification. Code using a heap, or sorting during the pop would not meet your "spec" because it isn't doing what the spec requires.  The best you have is testing, which is nice, but it isn't equivalent to a properly written specification.

I'm not suggesting that you're doing anything wrong, or that your methods aren't entirely valid for the projects you're working on.  I'm simply trying to point out that there are other ways that are different and offer different benefits.  In fact formal specification is pretty much complementary to what your talking about doing.

Jedidiah.

[ Parent ]

Hmm... (none / 1) (#130)
by ChaosEmer on Thu Aug 04, 2005 at 12:20:30 PM EST

Interesting.  I'd just like a more clear demonstration, as a stack seems overly simplistic.  That's why I like the priority queue. :)

Let's say that we wanted items that were compared equal to come out in a FIFO order.  How would that complicate the spec?  Again, I can imagine a simple, inefficeint implementation as follows:

(defstruct pqueue
  queue
  (counter 0))

(defun pqueue-next-counter (pqueue)
  (incf (pqueue-counter pqueue)))

(defun pqueue-push (pqueue val)
  (let* ((pq (copy-pqueue pqueue))
         (elem (cons val (pqueue-next-counter pq))))
    (setf (pqueue-queue pq) (sort (cons elem (pqueue-queue pq))
                                  (lambda (e1 e2)
                                    (cond
                                      ((< (car e1) (car e2)) t)
                                      ((< (car e2) (car e1)) nil)
                                      (t (< (cdr e1) (cdr e2)))))))
    pq))

(defun pqueue-pop (pqueue)
  (values (make-pqueue :queue (rest (pqueue-queue pqueue))
                       :counter (pqueue-counter pqueue))
          (car (first (pqueue-queue pqueue)))))

How does the provable spec scale to this requirement?

[ Parent ]

Apples and Oranges (none / 0) (#132)
by GileadGreene on Thu Aug 04, 2005 at 01:04:20 PM EST

Why do you persist with this apples and oranges comaprison? A specification is not the same animal as an inefficient implementation. Your (informal) specification is something along the lines of "Items should leave the queue in priority order. If two items with the same priority are available to be dequeued, the item that entered the queue first should be dequeued first." Express that formally, and you have a formal spec (I'm not familiar with CASL, so I'm not going to try anything like that here). It says nothing about when or if items should sorted (perhaps you maintain separate FIFO queues for each priority level - doesn't matter, since that's an implementation detail). It simply states what the priority queue needs to do. It's the difference between an abstract data type, and a concrete implementation of an abstract type.

Your "inefficient implementation" says too much about the nature of a priority queue - it states how the results are achieved. Could you use it as a spec? I suppose you could in a loose sense. But in order to do so you need to mentally (or actually) execute the "spec" in order to infer the properties it claims to maintain. A real spec simply states what those properties are, without requiring any execution. And therein lies the fundamental, apples and oranges difference: specs declare properties, while implementations prescribe operations.

[ Parent ]

Ah well... (none / 1) (#133)
by Coryoth on Thu Aug 04, 2005 at 02:29:03 PM EST

Your missing the point completely, but GileadGreene seems to have covered that fairly well.  Here's how the spec changes to handle that.  Essentially the main change is that we no longer have a strict total order for priority.  We have two orders - a (non-strict) total order on priority, and a strict partial order determined by entry order into the stack. Gien that then the ore requirement require only a little tinkering: If the elements are equivalent by priority order, then they must adhere to internal stack order.  Note that FILO is just a matter of reversing the axiom on o<.

spec PriortiyQueue = Stack[Elem]
then
    ops
        priority_pop: stack ->? stack
        priority_top: stack ->? elem
    preds
        _p<_: elem * elem
        _p~_: elem * elem
        _o~_: elem * elem
    axioms
        · not def priority_pop(empty)
        · not def priority_top(empty)
        forall x,y,z: elem
            % push order (strict partial)
            · x o< y => not (y o< x)
            · x o< y /\ y o< z => x o< z
            % priority order (non-strict total)
            · x p< y \/ y p< x
            · x p< y /\ y p< z => x p< z
            % priority equivalence
            · x p< y /\ y p< x => x p~ y
        forall s: stack, e: elem
            · not (s = empty) => top(push(s, e)) o< top(s)
            · priority_top(priority_pop(s)) p< priority_top(s)
            · priority_top(priority_pop(s)) p~ priority_pop(s) => priority_top(priority_pop(s)) o< priority_pop(s)
end

It would seem to be scaling pretty well to me, and the requirements seem a lot more clearly expressed than in your implementation, as well as being more abstract.  Reference implementations and specifications are very different beasts that serve very different puproses.  If you want to formally record requirements a specification is the way to do it.

Jedidiah.

[ Parent ]

You still misunderstand me... (none / 0) (#137)
by ChaosEmer on Sat Aug 06, 2005 at 11:33:01 PM EST

I was contiuning pursuit of this example not because I dislike specs, but because I wanted to see what it would look like.  I feel the article's example of a stack was not complicated enough to demonstrate anything other than syntax.

Right now, there is only one thing that seems odd -- you didn't abstract away the concept of strict partial and non-strict total orders.  I hope that was because you did not want to use such an "advanced" feature and not because the system does not support saying "p< is a non-strict total ordering", where what a non-strict total ordering is is defined elsewhere.

You are right that your spec has requirements expressed a lot more clearly than my reference implementation.  I still believe that for most programs specs are not as useful as reference implementations.  I hold this belief because I believe that for most programs failing is not that big a deal.

[ Parent ]

Sure, whatever. (none / 1) (#139)
by Coryoth on Mon Aug 08, 2005 at 02:32:00 PM EST

Right now, there is only one thing that seems odd -- you didn't abstract away the concept of strict partial and non-strict total orders.  I hope that was because you did not want to use such an "advanced" feature and not because the system does not support saying "p< is a non-strict total ordering", where what a non-strict total ordering is is defined elsewhere.

If I was expecting to reuse partial and total orders, in strict and non-strict versions then yes I would likely abstract them. I was trying to write a simple example that covered everything clearly. In practice I would simply use the CASL library, which has, for example, predefined orders and relations that you can use. Doing so wouldn't make for such a self contained example though.

Jedidiah.

[ Parent ]

Why? (none / 1) (#140)
by GileadGreene on Mon Aug 08, 2005 at 04:06:11 PM EST

I still believe that for most programs specs are not as useful as reference implementations.

Why?

Given a reference implementation, I have two choices:

  1. Try to create an implementation that matches every idiosyncrasy of the "reference implementation".
  2. Attempt to infer what behavior specification was intended by whoever wrote the reference implementation, and then try to create an implementation that matches that inferred spec.
In case #1, I can verify that I have created a compliant implementation by exhaustively testing both implementations, and comparing the outputs for each input (assuming for the moment that there is no nondeterministic initial state involved, and thus that I/O homomorphism ⇒ state homomorphism). In case #2, I can try to compare inputs and outputs - but how will I know whether a disagreement on outputs results from a deviation from acceptable behavior, or is simply an idiosyncrasy of the reference implementation that has no bearing on the acceptable behavior? A trivial example is the priority queue example you've been using: if the reference implementation happens to provide FIFO ordering on items with the same priority, is that actually a requirement, or just an artifact of the implementation? For a simple reference implementation it may be possible to ensure that the reference behavior is identical to the desired behavior. But for more complex behaviors, can you really be sure? How do you verify that your "reference implementation" if there's no spec to check it against?

[ Parent ]
Remember, I'm talking about "most apps" (none / 1) (#141)
by ChaosEmer on Tue Aug 09, 2005 at 11:27:19 PM EST

Because most applications are not mission critical.  To get a fully detailed spec for these apps would take up tons of time (imagine a fully detailed spec for Microsoft Word) and would be difficult enough to translate into a working implementation that it would be nearly unused.

I'd much rather have the buggy version of Word I have right now then a bug-free version of Word that's missing the features I need in 10 years.

[ Parent ]

Then do as much as you need (none / 1) (#142)
by Coryoth on Tue Aug 09, 2005 at 11:37:16 PM EST

Would I bother to spec the GUI of MS word? I'd probably just hand that to a good HCI person to design. So there's a big chunk that's not worth specing at all (unless you have specific requirements in mind). How about the rest? Well a lot of the features probably don't need much (though some contracts might not hurt). It would be nice if the macro execution system was fully specified so we can significantly reduce concerns about viruses and trojans exploiting bugs and buffer overflows there. It would also be nice if the word .doc format renderer was fully specified so that revisions and additions to the .doc format can be kept compatible and so we can guarantee how document parts get rendered. IS formal specification right for everything? No. I said that several times in the article, let alone repeating it many times on comments. Are there a great many projects for which it would be very useful to specify at least some components to some level of formality? Hell yes. A lot more than actually use formal specifiation currently.  Formal specification is not a silver bullet, but it is a powerful tool that a good developer should have available in their toolset for getting things done. It's worth learning how to do formal spec properly so you can know better when to use it.

Jedidiah.

[ Parent ]

Brilliant idea (none / 1) (#136)
by jongleur on Fri Aug 05, 2005 at 12:58:32 PM EST

You could get code from search around the spec, and you could maybe learn shortcuts through your search, in the same way that programmers do. Hrmmmm, what a frikkin worthy area of research.
--
"If you can't imagine a better way let silence bury you" - Midnight Oil
[ Parent ]
How to verify specification's correctness? (none / 1) (#102)
by mfx on Tue Aug 02, 2005 at 03:59:42 PM EST

How can one verify that the (formal) specification correctly models the desired intent?

Formal specifications work well in rigidly defined environments (e.g. embedded/realtime systems). Here, the requirements won't change very often, since they follow from the "physical" restraints of the system.

Specification won't help much to prove the correctness of many typical "business" environments (say, a database-backed web shop that interacts with a back-end ordering service using SOAP), where large parts of the software only exists as "glue" to interact with other software, and to work around the features of third-party libraries, databases, and legacy systems. In such a system, most errors are not "business logic" errors, but "glue problems" -- the software your code interacts with doesn't work as expected (or specified).

"The hardest part of the software task is arriving at a complete and consistent specification, and much of the essence of building a program is in fact the debugging of the specification." (Frederick P. Brooks, No silver bullet)

It's easier than verifying code's correctness (none / 1) (#103)
by Coryoth on Tue Aug 02, 2005 at 04:17:19 PM EST

How can one verify that the (formal) specification correctly models the desired intent?

By going through the specification and determining whether it fulfills the requirements - not this isn't perfect, but it is better tha going through the code to see whether it fulfills the requirements.  A specification is a lot more clear than code, and you can test/prove whether certain desired properties will hold for a specification - you won't be able to do that with code.  IS a specification perfect?  No, but it can often be an improvement, so why not do better if you can?

With regard to business environments - sure a web frontend to a database doesn't need a lot of specification (though some spec on ensuring commit operations are successful, and if not are guaranteed to suitably flag an error might be nice).  On the other hand I would be much happier if I knew the database itself had used specification and could provide explicit guarantees of security and data integrity.  Not every application needs specification.  Not every app is a simple web frontend, or visual basic script either.  There are plenty of places (security, all those "backends and databases your scripts apparently rely on, etc.) where specification does make sensee, and does offer real significant benefits.  Writing it off because it doesn't suit your personal needs given the type of applications you write is foolhardy.

"The hardest part of the software task is arriving at a complete and consistent specification, and much of the essence of building a program is in fact the debugging of the specification." (Frederick P. Brooks, No silver bullet)

Which goes further to making my case than yours.  If arriving at a complete consistent specification is the hardest part, then surely it makes sense to devote your energy to that, using tools designed for it (specification languages).

Jedidiah.

[ Parent ]

Language wars (2.50 / 2) (#104)
by mfx on Tue Aug 02, 2005 at 04:51:45 PM EST

I fear much of this discussion leads to a "language war" thats not really fruitful. Since each executable program is a formal specification (or would be when the programming language and all its libraries had a rigid definition ;-), the argument can be re-written as "my formal specification (programming language) is easier to understand than your programming language (formal specifation)".

This is trivially true when comparing, say, Z to C; but it is not so obvious when comparing a specification language to a "modern" language with a decent type system and garbage collection. Many of the cited examples describe migrations from C or C++ to Eiffel; i suspect any migration from an explicit-memory-allocation language to a managed-memory-language will likely improve productivity by a factor of 10, while decreasing error rates.

For a usable formal specification language, the folling criteria should be met:

  • much more concise than the implementation language: why should a 100-line specification contain less errors than a 100-line implementation? If it's only 10 lines it might be obviously correct.
  • easily understandable: errors in the specification must be obvious; if the description is too "dense", i can't understand it, and my manager and/or customer won't either
  • executable: I don't trust anything written by me (be it a "program" or a "specification") that is not covered by a unit test
The last point is important: i believe that concrete examples are a very good form of specification. Most people are better at giving examples than defining rules, especially when exceptional cases are concerned. So, at least for me, a unit-test based approach to specification works quite well.

To come back to the Brooks quote: what it highlights is the sorry fact that most "specifications" encountered by programmers are incomplete, inconsisten, and don't fully capture the intent of the customer. Programming then consists of translating this "informal specification" into a complete, executable, formal spefication -- which is the program.

The proof of the pudding is in the eating, and the proof of a specifications correctness is the execution of the program.

[ Parent ]

It needn't be (none / 1) (#106)
by Coryoth on Tue Aug 02, 2005 at 05:09:14 PM EST

There is an obvious and natural divide between specification (which define requirements, and intended operation in an abstract manner that allows explicit formal proof) and implementation  which provides a single explicit recipe to follow.  Many formal methods follow this approach and use a specification language specifically designed for the task to develop and refine a formal specification, and then use a known standard implementation language (C, and ML are popular) to provide a particular implementation of the specification.

Z is not superior to C any more than English is superior (or inferior) to C - they are for different tasks.

Sure, some languages like Eiffel integrate some amount of the specification into the language itself - but that needn't be the case at all.  Specification languages aren't really for replacing programming languages, they are for augmenting programming langauges by replacing comments and design documents.

Please note that there is a difference between testing, which samples smattering of very particular cases, and verifying/proving properties of a specification which covers all cases and completely defines valid inputs.  Testing is always a good idea, but if assurance is required it is no replacement for a formal proof: I believe in pythagoras' theorem because I have seen (and constructed my own) proof that it holds - no amount of drawing and measuring triangles is going to be able to come close.

The proof of the pudding is in the eating, and the proof of a specifications correctness is the execution of the program.

And how exactly do you intend to prove the program executes as intended?  If I have a formal specification I can construct formal proofs that certain prperties hold - that the program will meet certain requirements - and I can validate the code against that spec.  If I just have code and some test, then all I know is that the program is correct for the tests I happened to apply.  This is not at all equivalent, nor is a replacement.

If the specfication is necessarily incomplete because the customer can't tell you what they need for that part, so be it.  That doesn't stop you proving the requirements that the customer can specify.

Jedidiah.

[ Parent ]

But what does the specification specify? (none / 1) (#108)
by mfx on Tue Aug 02, 2005 at 05:53:46 PM EST

And how exactly do you intend to prove the program executes as intended? If I have a formal specification I can construct formal proofs that certain prperties hold - that the program will meet certain requirements - and I can validate the code against that spec. If I just have code and some test, then all I know is that the program is correct for the tests I happened to apply. This is not at all equivalent, nor is a replacement.

And how exactly do you intend to prove that the formal specification specifies the intended behaviour? If I have a suite of test cases, i can guarantee that the actual program handles these test cases, i can trivially extend it by new cases, and i can usually get a good code coverage.

If if prove a specification, all i know is that program A and specification B agree. That only helps if specification B is handed down by god (or the customer, which amounts to the same). If it is my own specification, i now have three problems: getting the specification right, getting the program right, and proving that the latter implements the former.

There are programs where the specification is obviously correct and the program is much harder to comprehend (e.g. the specification of a sort routine: "the output is sorted"), but in my practical experience, such problems don't come up very often.

From my student days, i dimly remember my experiences in formal verification - when verifying by hand, i made at least as many errors in my verification proofs than in my original programs; and setting up the proofs (e.g. finding loop invariants) sometimes took a lot of ingenuity (just like in any other proof). Maybe my attitude towards formal verification is tainted by these experiences; i would like to hear about practically usable approaches to verification.

[ Parent ]

What do your tests specify? (none / 1) (#111)
by Coryoth on Tue Aug 02, 2005 at 06:27:16 PM EST

Someone somewhere along the line has to give you some basic set of requirements.  Specification simply says at the point where you're getting those requirements from the customer, you sit down and try and write a spec and go back and forth until you've resolved all the matters that are important requirements to the custmer.  Thus you have your spec.

Such a process can actually be extremely enlightening.  In writing a spec you often find many assumptions that you are taking for granted.  The customer can provide you a set of "rules" for specfic test cases, but what is supposed to happen outside those cases?  If you're writing a spec you'll be forced to ask.  The answer could turn out to be quite specific, or the customer could not care at all.  If the customer doesn't care, then you don't need to constrain your requirements/specification further on that point.

If I prove some of the specification I know that some property holds true.  I then have to validate the code against the spec, which can be done.  But proving part of the specification might be, for example, proving that if x happens then y will always happen, which is the sort of thing that the customer gave you as a requirement.

As to " i now have three problems: getting the specification right, getting the program right, and proving that the latter implements the former.": Getting the specification right is the main problem.  If you can do that then the rest can follow naturally.  Formal specification simply asks that you bother to spend time on the initial part - gathering formalising and making sure you've captured as much of the customers requirements as you can.  It aids you by being abstract and covering all cases, which helps you find weakpoints and areas that need to be better defined.  The aim of the exercise, I thought, was to deliver something that does what the customer wants, not something that passes tests for the couple of cases you talked to the customer about and could do anything for all the other cases.

As to proofs and building specs - there are automated theorem proving tools and simplifiers.  They still require someone to drive them, or wor through the simplified output, but they can take a lot of the work out of proving.  Building the specs is a matter of practice.  Figuring out the right loop invariant can be hard the first time.  Figuring out how to build a linked list, write an effective recursive function, or build a sensible object heirarchy can be hard the first time to.  You learn from experience and it becomes much easier.

Jedidiah.

[ Parent ]

Do your test cases cover the intended behavior? (none / 1) (#112)
by GileadGreene on Tue Aug 02, 2005 at 06:29:45 PM EST

And how exactly do you intend to prove that the formal specification specifies the intended behaviour? If I have a suite of test cases, i can guarantee that the actual program handles these test cases, i can trivially extend it by new cases, and i can usually get a good code coverage.

How exactly do you know that your test cases represent the intended behavior? And assuming they do, how do you know that the intended behavior is preserved outside of the inputs you apply in your test cases? If you can express the "intended behavior" as test cases, why not generalize it into a formal spec that covers all inputs? That way at least the second question is covered, and all you're left with is the first question, which is going to be a problem no matter what you do.

If it is my own specification, i now have three problems: getting the specification right, getting the program right, and proving that the latter implements the former.

Ah. I see. It's better to just "get the program right" without actually having any definition of what constitutes "right". That would certainly make program development much easier... I can see why it's such a popular approach.

From my student days, i dimly remember my experiences in formal verification - when verifying by hand, i made at least as many errors in my verification proofs than in my original programs

Which is presumably why proof-assistants and model-checkers are so popular for formal verification.

Maybe my attitude towards formal verification is tainted by these experiences; i would like to hear about practically usable approaches to verification.

Well, you might start by looking at the formal specification and verification tools that are actually used in practical situations in industry: the B-tool, SPARK, SPIN, and FDR to name just a few.

[ Parent ]

An example (none / 1) (#113)
by mfx on Wed Aug 03, 2005 at 03:17:18 AM EST

How exactly do you know that your test cases represent the intended behavior? And assuming they do, how do you know that the intended behavior is preserved outside of the inputs you apply in your test cases? If you can express the "intended behavior" as test cases, why not generalize it into a formal spec that covers all inputs? That way at least the second question is covered, and all you're left with is the first question, which is going to be a problem no matter what you do.

I believe that it is usually much easier to get a set of test cases right than to get the specification right.

Take a simple example: a sort method for integers. A test-case based example could be as simple as

sorted [] = []
sorted [3,1,2] = [1,2,3]
sorted [1,2,3] = [1,2,3]
sorted [1,2,1] = [1,1,2]
sorted [ 100 .. 1 ] = [ 1 .. 100 ]

A formal specification must capture the conditions

if sorted xs = ys
  then ys is a permutation of xs
if sorted xs = ys and length ys >= 2
  then ys[0] < ys[1] < ... < ys[length xs]

I remember a sort specification where i forgot the permutation part and thus managed to prove the "correctness" of sort method that sorted [1,2,3] into [1,1,1] or [].

That proves my point: it is as easy to make an error in the specification as in any programming language. The "generalize into a formal spec that covers all inputs" part is hard;  possible as hard as programming the stuff in the first place (some might say, it is even harder).

So how do you know that the specification is correct?


[ Parent ]

Huh? (none / 1) (#119)
by GileadGreene on Wed Aug 03, 2005 at 01:12:26 PM EST

How do you know your test cases are right? Because they match a (informally, carried implicitly in your head) specification of what "sorting" should do. You look at the test cases, and they match some internal idea you have of what constitutes sorting. Formal specification is simply the process of making the internal idea into something external and explicit. Nothing says you can't start from some simple examples, like your test cases. Then you say to yourself "what makes these similar?". Having established a spec you can use model-checkers or proof-assistants to explore the logical implications of your spec, and ensure that it doesn't lead to contradictions, and that it doesn't lead to situations that contradict your internal mental model of what tyhe spec should be doing.

How did you know that your "sort" specification was incorrect? Because it didn't provide the behavior you expected from "sort". What was that expected behavior? Express that formally, and you'll have your correct spec.

Is formal specification hard? Sure, it can be. But no harder than programming. The only reason that using test cases seems easier is that you avoid having to precisely state the problem, which makes the range of "acceptable" solutions larger. What should your "test case specified" sort algorithm do when handed [-1, -2]? Or [1]? Or [5,a,4,%]? Who knows: it's unspecified! Makes it a lot easier to write code that meets the spec, right?

[ Parent ]

Simplicity of programming vs. specifying (none / 1) (#122)
by mfx on Wed Aug 03, 2005 at 03:12:19 PM EST

Is formal specification hard? Sure, it can be. But no harder than programming.

But it can only be truly useful if creating a correct specification is much easier than creating a correct program, and if the specification is much easier to comprehend.

When i have to write a program in a given time frame, i can use that time to create a formal specification, an implementation, and a proof (maybe  automatically derived). This may take a while, unless the formal specification is really concise, and the proof mostly automatic.

I can also use said time to write test cases and an implementation, and use the "leftover time" to improve the implementation: refactor it, partition it in better understandable modules, in short: make it more readable.

Don't misunderstand me: i would like to have the option to specify formal semantics for pieces of my code. But currently i know of no tools available to me that don't force me to learn a specification language, change over the implemtnation from Java (which is a requirement) to a different programming language (Ada, Eiffel) and use a new programming environment. OTOH, unit test tools are readily available and easily usable.

[ Parent ]

Try JML then (none / 1) (#123)
by Coryoth on Wed Aug 03, 2005 at 03:48:07 PM EST

Don't misunderstand me: i would like to have the option to specify formal semantics for pieces of my code. But currently i know of no tools available to me that don't force me to learn a specification language, change over the implemtnation from Java (which is a requirement) to a different programming language (Ada, Eiffel) and use a new programming environment.

Then you should be looking at JML which is (trying to be) to Java sort of what SPARK is to Ada.  JML is, of course, a lot younger than SPARK so doesn't have the fully matured toolset.  It does have a fairly large amount of tools readily available right now, and supports other tools like an extended static checker, some automated proof tools, an invariant detector and and Eclipse plug-in.  It also includes a unit testing framework and extensions to javadoc that understand JML specification, thus making your docs more accurate. Sure you have to learn the JML specification semantics, but that's not really very difficult, certainly not for the basic level.  Read some of their examples and see how easy it is to learn.

Jedidiah.

[ Parent ]

On JML and SPARK (none / 0) (#125)
by NoNeeeed on Wed Aug 03, 2005 at 05:20:12 PM EST

JML looks interesting.  Although there is a fundamental difference between SPARK and most other DBC systems, the SPARK tools analyse the code BEFORE you run it.

By the looks of it, JML is performing the contract checks during execution (although the contracts appear to be type-checked etc before execution) .  To my mind this seems to give little more than an extended exception system.  This is a fudamental property of the base language.  Because SPARK is based on a tractably small subset of Ada (although actually quite functional, and getting more so every year as we figure the harder bits out) it is possible to actually perform the analysis prior to execution, in a compiler/platform agnostic manner.

This is why there is no SPARK for C.  It would be possible to create a C-like language, but it would just be SPARK/Ada with some of the C syntax, but less useful.  There is some argument that such a subset could be constructed from C++ due to it having more structural symantics.

Don't get me wrong, JML looks really interesting, much as C/Splint is, there is a fundamental difference between them and SPARK.

Apologies for rambling, getting late here.

Paul

[ Parent ]

Sorry, should have added.... (none / 1) (#126)
by NoNeeeed on Wed Aug 03, 2005 at 05:22:41 PM EST

if I have totally missed something about JML, please feel free to correct me, I will certainly be looking into it more.

Also I (and most of my colleagues) will cheer on anything that make the practice of software engineering better, whatever the language.  There are many kinds of software, and many ways to create it, each should be appropriate for the context.

Paul

[ Parent ]

Sort of. (none / 1) (#127)
by Coryoth on Wed Aug 03, 2005 at 05:58:50 PM EST

My understanding of SPARK and all its capabilities is clearly not as good as yours (I've read Barnes' book, and that's about as far as I've got), and I'm certainly no expert on JML either.  I think, however, that support for JML syntax by the likes of ESC/Java2 and SpEx provide a lot of the static checking that (you quite correctly note) JML alone does not.  How these static checkers compare the the rather impressive checks that SPARK Examiner can perform I don't really know, but it seems to me that the goals of thoses projects are similar to the static checking capabilities available for SPARK.

I woul be interested to know your opinion on such tools, and how they compare.

Jedidiah.

[ Parent ]

Again "huh"? (none / 1) (#124)
by GileadGreene on Wed Aug 03, 2005 at 04:09:14 PM EST

But it can only be truly useful if creating a correct specification is much easier than creating a correct program, and if the specification is much easier to comprehend.

The whole point of this is that without some form of specification it's not possible to determine whether or not your program is correct. The advantage of writing a formal (as opposed to an informal) specification is that the specification is amenable to automatic analysis and verification.

I can also use said time to write test cases and an implementation...

An implementation that is only verifiably correct for the test cases you have specified. Perhaps that is acceptable for the projects that you work on. But not everyone develops that kind of software. In many cases, the fact that an implementation exists matters very little, if the implementation in question does not work correctly. As I've said elsewhere in this thread, the techniques used to build doghouses and skyscrapers are substantially different.

Furthermore, I am highly skeptical that using some minimal formalism (like, e.g. design by contract) will take any longer than creating test cases. But DbC will deliver more rigorous checks of your code, completely automatically (see the links to JML below for an example of this kind of tool).

But currently i know of no tools available to me that don't force me to learn a specification language...

Well yes, if you object to having to learn new things then you probably aren't going to be able to get very far with formal spec. But just because you don't want to learn anything doesn't mean that everyone else feels that way.

...change over the implemtnation from Java (which is a requirement) to a different programming language...

Well, you can get limited extended static checking via ESC for Java. And there are a couple of projects that permit Design by Contract in Java, such as jContractor and JML. JML also includes the capability to automatically generate jUnit tests from specs, the ability to mix formal and informal specs, support for refinement, and all sorts of other neat features. The JML developers state that "It [JML] is designed to be written and read by working software engineers, and should require only modest mathematical training."

OTOH, unit test tools are readily available and easily usable.

Perhaps they seem that way because you are more aware of them. Coryoth's article was attempting raise your awareness of other possibilities.

[ Parent ]

Generate the code from the specifications (none / 0) (#150)
by dcrocker on Sun Sep 18, 2005 at 11:06:14 AM EST

I agree that if you have to write the specification and the code, then the initial development time may increase (althought the debugging and maintenance time should decrease). However, there are some systems that can generate most or all of the code from the specification. This means you are writing just the specification, which is shorter than the code; so the total development time is substantially reduced.

We typically find that the generated code is about 3 times larger than the specification - despite the fact that the specification also contains comments and is better laid out.

[ Parent ]

Proofs of generalised test cases (none / 1) (#151)
by dcrocker on Sun Sep 18, 2005 at 11:23:55 AM EST

If I have a suite of test cases, i can guarantee that the actual program handles these test cases, i can trivially extend it by new cases, and i can usually get a good code coverage. If if prove a specification, all i know is that program A and specification B agree. That only helps if specification B is handed down by god (or the customer, which amounts to the same). If it is my own specification, i now have three problems: getting the specification right, getting the program right, and proving that the latter implements the former.

If you can construct some test cases that you know to be correct, then by implication you know a part of the specification. Even if you are given the test cases, you can use them to check the specification. Just add the test cases to the specification. While you are at it, generalise the test cases to cover a wide range of inputs. So a test case that states "for these particular inputs Xi, the output should be Yi" becomes "for all inputs Xi that satisfy property P, the output Y' is releated to the Xi by the predicate Q".

There are programs where the specification is obviously correct and the program is much harder to comprehend (e.g. the specification of a sort routine: "the output is sorted"), but in my practical experience, such problems don't come up very often.

Try this one. Suppose you are writing a complex program such as a word processor, spreadsheet etc. and you want to provide an "undo" command. Writing code for the undo command is likely to be very difficult if there are lots of different commands that might need to be undone (assuming you can't afford to just take a snapshot of the whole of the previous state). But specifying it is easy.

From my student days, i dimly remember my experiences in formal verification - when verifying by hand, i made at least as many errors in my verification proofs than in my original programs; and setting up the proofs (e.g. finding loop invariants) sometimes took a lot of ingenuity (just like in any other proof). Maybe my attitude towards formal verification is tainted by these experiences; i would like to hear about practically usable approaches to verification.

Manual construction of proofs is not only error prone, it is also impossibly inefficient for all but the most critical applications. Formal methods are only practical for everyday software development if the theorem proving is done automatically. Fortunately, there have in recent years been big advances both in automated reasoning technology and the computer power needed to do it. As for loop invariants, the trick is to have the system generate the loops from specifications, so the user need not be concerned about loop invariants. We find that we only need to manually write about 8% of all the loops in a program; the rest are generated from the specifications.

[ Parent ]

Not a silver bullet, but still a useful tool (none / 1) (#110)
by GileadGreene on Tue Aug 02, 2005 at 06:11:51 PM EST

How can one verify that the (formal) specification correctly models the desired intent?

Depends what you mean by "intent".

Is it possible to perfectly validate (not verify) that a formal specification is a truly accurate reflection of what the customer wants? Not really - at least not in a formal, proof-of-correctness sense. There will always be a transition from informality to formality in a software development project. The point is that by pushing that transition back closer to the customer you are in a better position to catch errors and misunderstandings before they cost too much. If you can precisely express what you think the customer wants, you are more likely to be able to determine whether or not your understanding of the customer's desires is also accurate.

Is it possible to verify that a formal spec preserves some higher level of invariants (which formally express some more abstract intent)? Yes. That's the point of developing a formal spec - it can be analyzed to ensure that the desired properties are preserved in all cases. Of course, those desired properties need to be expressed in a formal language too, and then we're back to the situation described in the preceding paragraph...

Formal specifications work well in rigidly defined environments (e.g. embedded/realtime systems). Here, the requirements won't change very often, since they follow from the "physical" restraints of the system.

Uh, how many embedded/realtime systems have you worked on? I've seen plenty that have involved quite variable requirements sets.

"The hardest part of the software task is arriving at a complete and consistent specification, and much of the essence of building a program is in fact the debugging of the specification." (Frederick P. Brooks, No silver bullet)

Which is precisely why you'd want a formal spec of some kind: it can be analyzed for completeness and consistency, and it is easier to debug because ot is precise rather than ambiguous. Sure, a formal spec is not a silver bullet. But it can help a lot. If we took the attitude to other tools for software development that you are taking to formal specs all code would be developed by randomly punching in 0's and 1's until the resulting program produces a result that looks something like "what the customer wants".

[ Parent ]

no evidence whatsoever (2.50 / 2) (#143)
by jcarnelian on Wed Aug 10, 2005 at 11:12:32 AM EST

"Formal Specification helps build more robust, more maintainable software with fewer bugs and defects."

That isn't even a good hypothesis.  Giving your developers free backrubs probably "helps build more robust, more maintainable software with fewer bugs and defects", but that doesn't make it a cost effective way of producing better software.

The trouble with proponents of formal methods is that they apparently can't even formulate a good hypothesis, let alone know how to test it experimentally.  As a result, articles like yours not only fail to convince people, they actually further damage the credibility of proponents of formal methods.  If proponents and practitioners of those methods are unfamiliar with elementary rules of scientific research and scholarship, why should one take anything you say seriously?

Evidence? Hypothesis? (none / 1) (#144)
by Coryoth on Thu Aug 11, 2005 at 03:32:53 PM EST

If you want evidence of more robust software with fewer bugs try looking at any of the many examples of the successes of formal methods. I can recall at least one case where a project in SPARK deliveerd in the same time as a competing effort in C but had an order of magnitude or two less bugs and errors than the C. There's plenty of evidence if you want to actually look at cases where formal methods have been used.

As for more maintainable - what's more maintainable a large project of dinamically typed code with function having no type signature or similar code that is statically typed? The latter obviously. That's formal specification in action (static typing is just a level of formal spec). Now consider how much easier it is to read and analyse code where the functions have contratcs and the code has explicitly and precisely documented requirements.

So the only remaining question is, is it cost effective? That, surely depends on the needs of the project. If correctness, security, or reliability are of significant concern then formal methods are quite cost effective (and have proven to be so in many real world cases). The amount of testing required to reach the same level of assurance formal specification can provide can easily take far longer and cost more than developing the formal spec.

I've said several times in the article, and numerous times in comments: formal specification isn't right for everything. It isn't a silver bullet, and the software world is not made of of nails begging for a formal specification hammer. That doesn't mean that there are not many projects for which it does make sense, for which it is cost effective, and for which it may well be the best approach.

A good software engineer should use whatever tools he has at his disposal to do the job at hand. Different jobs call for different tools. Formal specification is just another tool, and it's a powerful tool. A wise software engineer will learn a little about it so he can know when it is and isn't appropriate rather than basing his opinion on myths and misnomers.

Jedidiah.

[ Parent ]

still no evidence (none / 1) (#148)
by jcarnelian on Wed Aug 31, 2005 at 07:04:56 PM EST

If you want evidence of more robust software with fewer bugs try looking at any of the many examples of the successes of formal methods. I can recall at least one case where a project in SPARK deliveerd in the same time as a competing effort in C but had an order of magnitude or two less bugs and errors than the C. There's plenty of evidence if you want to actually look at cases where formal methods have been used.

Those are selective anecdotes, not evidence. Even if they were a statistically representative sample, at best, they might show a statistical correlation between the use of formal methods and improvements in quality, but that is far from showing that the formal methods are responsible for the improvements in quality.

I've said several times in the article, and numerous times in comments: formal specification isn't right for everything

You haven't shown that it is useful for anything.

A good software engineer should use whatever tools he has at his disposal to do the job at hand. Different jobs call for different tools. Formal specification is just another tool, and it's a powerful tool.

You have presented no evidence that it is does anything at all, let alone that it is "powerful". (I will stipulate, however, that using "formal methods" will do one thing: consume time and resources.)

A wise software engineer will learn a little about it so he can know when it is and isn't appropriate rather than basing his opinion on myths and misnomers.

So, why are you asking people to do just that? So far, all you have presented in favor of "formal methods" is anecdotes (myths). And, given that "formal methods" apply mathematics that is completely unrelated to the purported goal of the practice, namely quality improvement and error reduction, I contend that the term "formal methods" is a misnomer as well; you might as well call software improvement through the application of juju sticks a "formal method" because there is about as much support for that approach. In fact, I suspect that a lot more people in the world believe in juju sticks than in formal methods.

[ Parent ]

A Case for Formal Specification | 151 comments (142 topical, 9 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!