Beta

Slashdot: News for Nerds

×

Welcome to the Slashdot Beta site -- learn more here. Use the link in the footer or click here to return to the Classic version of Slashdot.

Thank you!

Before you choose to head back to the Classic look of the site, we'd appreciate it if you share your thoughts on the Beta; your feedback is what drives our ongoing development.

Beta is different and we value you taking the time to try it out. Please take a look at the changes we've made in Beta and  learn more about it. Thanks for reading, and for making the site better!

A Case for Formal Specification

Coryoth (254751) writes | more than 8 years ago

Programming 8

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 th

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

For good examples of formal specification at work I would suggest you try this Z case study or the case study for CASL in the CASL user manual. For those who want something more immediate I have a warning: To be short enough to present easily in this space the specifications are necessarily very simple and should be taken as a sample of the flavour of formal specifications rather than a serious example.

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 values for 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 makes the workings of the specification 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, and you can specify as much or as little of the system as you need. Formal specification covers everything from adding contracts to a couple of critical routines to complete specification of the entire project.

Formal specification isn't necessarily significantly more work than you do now. 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 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 and impractical to people who don't know specification languages. Take the time to learn and your perspective will change.

But the Project Requirements are Always Being Changed...

It is true that many projects face ever changing requirements. The question is not whether this renders formal specification useless (it doesn't) but how formal specification compares to informally specified software in such a situation.

First of all it should be noted that engaging in formal specification can help reduce the problem to begin with. By requiring you to rigorously specify at least some portions of the software, formal specification can assist in finding ambiguities, cases that were not covered, and other problems much earlier in the development cycle when changes are easiest to make. Those parts of the system, such as GUIs, that are often the target of more whimsical design or requirements changes are precisely the parts that benefit least from, and are least likely to use, formal specification. Changes to design or requirements for those parts of the system, then, are not likely to be more detrimental than for informally specified projects.

Secondly formal specification is quite capable of dealing with change, and even offers benefits in the face of changing requirements. A change in requirements results in a change in specification, but because the specification is formally written the impact of the changes can be analysed. You can check that new requirements remain consistent with the rest of the system. You can also determine all parts of the system that will be impacted by the change and avoid bugs introduced by the changes. Having a formal specification for the system when a change in requirements occurs makes it easier to see how the change will effect the system and easier to make the changes consistently and completely. Formal specification can make changes in requirements easier to deal with, not harder.

But I Already do Unit Testing...

Unit testing is fantastic, and there's no reason to stop just because you can write proofs for some aspects of your code. Unit testing is not a replacement for formal specification however. Testing only verifies the component for a very limited and specific range of cases. Specifically testing covers the cases that the developer thought of. A great many bugs, however, are those that occur from situations the developer didn't consider, and probably wouldn't have included in his test. You can improve the situation with testing tools like fuzzers, but you're still only checking a sampling of the whole space. Formal specification, on the other hand, allows construction of formal proofs that cover all possible cases. I would much rather specify and prove Pythagoras' theorem than simply assume it is true by testing it on random right angled triangles. Likewise, while testing is valuable (and easy) when assurance matters it is no replacement for proof based on a specification.

Does this mean you should give up Unit testing? In no way shape or form. Just as formal proofs in mathematics are much harder than trying a few cases, formal proofs from specifications require significant work - you most likely can't prove everything. That means the best method is prove those properties that are critical, and continue testing the system much as you normally would. Hopefully you'll see a lot less errors to debug based on the extended static checking of course.

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.

cancel ×

8 comments

Formal Specification (0, Offtopic)

Lando (9348) | more than 7 years ago | (#13317903)

Are you looking for a response to this entry? I'm not sure of your purpose for writing here.

I couldn't agree more (1)

rocker_wannabe (673157) | more than 8 years ago | (#13332362)


I read most of your journal entry and have come to the same conclusion. I've tried to introduce the concept at every job I worked at where it made sense. Unfortunately, I got nothing but blank stares or derision. It didn't help that I was a System Test Engineer and not a Software Developer at some of the companies. Most of the companies that I read about that seemed to adopt some formal methods where defense contractors. I've only worked in the "Wild West", "shoot from the hip", "stay up late hacking", commercial world so I was probably doomed from the start.

Les Hatton (1)

sleepingsquirrel (587025) | more than 8 years ago | (#13333209)

I'd be interested to hear your thoughts on papers about software failure by Les Hatton [leshatton.org] . Especially What is a formal method, (and what is an informal method) ? [leshatton.org] ...
Describes personal experiences in the use of formal methods over a 15 year period. Summarises by making the statement that there are probably worse problems to tackle first before formal methods could have a significant impact on system quality.

Re:Les Hatton (1)

Coryoth (254751) | more than 8 years ago | (#13334021)

I think he makes some good points, but I think the most important point is: what is informal specification? There isn't any such thing. All programming is some level of formal specification. Using static types and type signatures for function is formal specification. Going a little further and, say, adding "in/out" semantics like in SPARK allows for further static checking that can catch errors in the same way that static types catches errors at compile time. Adding contracts can allow for more effctive runtime error checking, and can allow for better static checking. Knowing a specification language can let you do a quick "back of the envelope" analysis of a function - you may never write the full formal spec for the function, but it can be beneficial in clarifying your reasoning. The act of writing a full formal spec can assist greatly with catching errors and assumptions early, and with maintainability by providing very precise documentation, as well as with extended static checking, and proof.

Each of those represents some level of formal specifiation, and each, in turn, has added benefits that come with added costs.

All I'm really trying to argue is that it is worth learning about formal specification (which isn't that hard) so you can decide what amount of it is right for the problem at hand. Each and every level can be useful, it's a matter of what sort of tradeoff suits the problem at hand. Most serious programmers bother to learn and have used static types. It only seems sensible to learn and have at least some experience with some of the techniques further up the specification hierarchy.

Jedidiah.

I don't get it. (1)

Chris Burke (6130) | more than 8 years ago | (#13335414)

I've seen examples like this of formal specification (in fact, the specification of a stack in CASL looks familiar). What I have yet to see is an example of an implementation of a stack and how that relates to the formal specification. Why do I use static typing and compile time checking? Because I can give specific examples of programming bugs that these things will catch in my implementation.

That is what this journal is missing, and why just a rote algebraic specification of a stack doesn't convince me that this is a good idea (though it would make a fantastic comment block above my real push/pop functions). Show me a stack implementation and what bugs the formal specification could catch.

Re:I don't get it. (1)

Coryoth (254751) | more than 8 years ago | (#13335636)

Okay, while sticking to simple easily and quickly understood examples, here's one that cropped up in discussion elsewhere: a priority queue. That can be specified as an extension of a stack as follows:
spec PriortiyQueue = Stack[Elem]
then
    ops
        priority_pop: stack ->? stack
        priority_top: stack ->? elem
    preds _<_: elem * elem
    axioms
        &#183; not def priority_pop(empty)
        &#183; not def priority_top(empty)
        forall x,y,z: elem
            &#183; x < y => not (y < x) % strict
            &#183; x < y \/ y < x \/ x = y % total
            &#183; x < y /\ y < z => x < z % order
        forall s: stack, e: elem
            &#183; priority_top(priority_pop(s)) < priority_top(s)
end
while someone gae the ollowing as their implementaion of a priority queue:
(defun priority-queue-push (pqueue val)
  (sort (cons val pqueue) #'<))
(defun priority-queue-pop (pqueue val)
  (values (cdr pqueue) (car pqueue)))
The obvious questions are, how does this not meet the spec, and what bugs does it catch. For starters the spec requires a strict total order (in terms of priority) on anything that can be added to the queue (if you try and write the spec you'll see why) in fact that's mostly what the extension to the stack is doing. The implementation, of course, has no guarantees on the order being either total, or strict. What happens if I push on object with priorities '1' then 'a'? They probably aren't comparable (and if they are, potentially not in the way we mean). What about with priorities '1' then '2' then '1'? What order should those priority 1 objects come off in? FIFO, or LIFO?

Now please don't say "but those are simple bugs!", - this is a simple example, so mostly what you get are simple bugs. It should give you some idea of the flavour of how things will work, remembering that specs can scale well.

As an alternative I suggest you try checking out SPARK, or for something similar JML [iastate.edu] and ESC/Java2 [secure.ucd.ie] which allows you to mark up Java code with specification and then run extended static checking, catching a whole lot more bugs statically than static types alone will get you.

Jedidiah.

Re:I don't get it. (1)

Chris Burke (6130) | more than 8 years ago | (#13341274)

Now please don't say "but those are simple bugs!"

No, no. This is perfect. I'd like to keep talking about it. In general the question "does this program do what it is supposed to?" is a variant of the halting problem. Seeing how formal specification allows you to answer that question in specific cases is what will make it worthwhile. The priority queue case is easy enough for a human to see, but no compiler I have used could possibly detect the problem.

Specifically, how does the specification allow you to detect that the implementation does not create a strict total order? You say that the implementation does not follow the spec, and indeed it does not, but I'm still not seeing the connection between spec and program. How does the tool verify that "priority_top(priority_pop(s)) < priority_top(s)" for all possible elements that could be pushed onto the queue without trying them? Do you have to wait until someone tries to push '1' and 'a' or two '1's before you detect the error?

I presume that a compiler could know, say, that < over integers (and 'a' would presumeably be some kind of integer) isn't a strict total order when used in sort(), though it isn't clear how it would automatically deduce this. But how does this work for an arbitrary comparison function between arbitrary element types? How would you change the implementation such that the spec could detect that you -are- creating a total order? If you do enforce LIFO or FIFO removal for equal elements, then that would be a total ordering, but how does the tool know that?

This is interesting, but still not quite clicking for me. I'm seeing the spec, I'm seeing what it says, I'm seeing the implementation, but I'm not seeing how the tool determines that the implementation does or does not meet the spec.

Re:I don't get it. (1)

Coryoth (254751) | more than 8 years ago | (#13344581)

Well, this isn't such a good example for showing exactly how that would work - the code is not written in a way that really allows verification/static analysis. Such things can be done (see for example HasCASL) and in fact that's how it's usually done - this was just a simple example of a spec and code with bugs in it that I had on hand.

Roughly speaking the analysis would go something along the lines of: take the condition on priority_pop function - that what get's popped has (strictly, by the axioms on the priority relation) lower priority that what's now on top. You can, in a sense, hoist that condition back through the code to see what the corresponding least precondition is. Presuming you had suitably annotated to code to do that which was similar to the LISP that someone offered, you would find that the valuation giving the priority would be required to return a unique priority for each object (and you can then check if the code does that) and that objects pushed onto the stack need to be able to be valuated to give a priority which is comparable to other priorities.

That's, as I say, not so clear with that example - it doesn't have a lot of the things that make automated static analysis easier (like, for instance, static types!). Here are a couple examples of bugs that SPARK can catch automatically. Again, the examples are simple, so the bugs are very simple, but the concept scales and it should give you some idea.

Imagine we have a suitably specified/annotated function for multiplying matrices in SPARK. It might look like (leaving out a lot of the details that aren't relevant here):
procedure Multiple(X, Y: in Matrix; Z: out Matrix)
--# derives Z from X, Y;
is
begin
    Z := Matrix'(Matrix_Index => (Matrix_Index => 0)); -- initialize Z
...
end
Now with the extra specification (in and out annotations, and derives) if somewhere later in the code you accidentally do something silly like try to square a matrix with
Multiply(A,A,A)
Then the SPARK Examniner will throw an error:
Semantic Error:165: This parameter is overlapped by another one which is exported.
for each of the first two paramters, in effect warning you that you are about to zero A prior to doing the mutliplication. Likewise you'll get an error if you fail to properly initialize Z in the procedure. Those are errors that static types alone won't catch.

For a different example, let's presume we have a very simple procedure to exchange two variables, and add a deliberate error so we can see how verification might work:
procedure Exchange(X, Y:in out Float)
--# derives X from Y &
--# Y from X;
--# post X = Y~ and Y = X~;
is
    T: Float;
begin
    T := X; X := Y; Y := T + 1.0;
end Exchange;
Now our in/out and derives annotations are consistent with the code, no errors there. SPARK Examiner will produce the following verification conditions though:
Hypothesis 1: true .
              ->
Conclusion 1: y = y .
Conclusion 2: x + 1 = x .
Which you can see is clearly not going to work - SPARK provides another tool (called Simplifier) which reduces/simplifies such conditions. It's results, making the whole situation more obvious, are:
Hypothesis: true .
            ->
Conclusion: false .
Again, this is a very simple example, but hopefully you can see how hoisting post conditions back through the code (which can be done in an automated fashion) can highlight problems without having to do any runtime checking.

Finally, Another very simple example:
type T is range -128 .. 128
 
procedure Inc(X: in out T)
--# derives X from X
begin
    X := X + 1;
end Inc;
Now there are implicit post conditions in the return type - it must be of type T. Run Examiner (and Simplifier) over this code and you'll get the following verification conditions:
H1: x >= -128 .
H2: x <= 128 .
    ->
C1: x <= 127 .
Now the conclusion is completely unsupported by the hypothesis, thus we have a potential runtime error if x = 128. Okay, that's a very simple overflow, but again it's more a matter of demonstrating how generating verification conditions from the spec and code can find runtime errors without having to resort to testing (which may or may not catch the problem case). The principle scales fairly well.

In general the very simple principle is this: if you can write a few extra precise statements explaining exactly what you intend the software to do in a language that automated tools can understand, they can often do a lot of static analysis and verification as to whether the code fits with the specificied intention, and if it doesn't, where it doesn't. Lint is great and can catch a lot of errors. If you give the tools a little more information, then there's more they can do, and more errors they can catch.

Jedidiah.
Check for New Comments
Slashdot Account

Need an Account?

Forgot your password?

Don't worry, we never post anything without your permission.

Submission Text Formatting Tips

We support a small subset of HTML, namely these tags:

  • b
  • i
  • p
  • br
  • a
  • ol
  • ul
  • li
  • dl
  • dt
  • dd
  • em
  • strong
  • tt
  • blockquote
  • div
  • quote
  • ecode

"ecode" can be used for code snippets, for example:

<ecode>    while(1) { do_something(); } </ecode>
Create a Slashdot Account

Loading...