Formal Methods

There's a battle going on in computer science that will probably never be fully resolved, between those who think programs are fundamentally mathematical, and those who eschew mathy techniques as being too tedious for use with real-world programs. Despite a layperson misperception to the contrary, most programmers avoid math just as most nonprogrammers do, with the result that more than 99% of software is developed today as nonmath.

Formal methods is the name for the techniques of mathematically proving that programs do what they're supposed to. The theory is that programs aren't physical objects, they are ideas; they don't break down, and they don't wear out, the way physical objects do. A perfect program will therefore remain perfect forever. Formal methods exist to make such perfect programs, compared to which even the most well-crafted nonmath program is fundamentally a buggy slapped-together sloppy mess.

It would be nice if formal methods were more widely accepted, because as programs grow larger and larger the interspersed bugs make them more and more unreliable. But formal methods slow the pace of program development so much, and fit so poorly into the messy but productive real world, that they are used only rarely even in potentially life-threatening systems.


A Logical Assertion

A subroutine consists of two parts: the desired final state (the specification, or spec), and the algorithm for bringing about that state. Theoretically the latter is redundant; one could implement any subroutine as "try all possible final states, and return with the one that satisfies the spec". This might be astronomically inefficient, since even a subroutine that changes only a single 32-bit value would have to try 4 billion combinations, but that's beside the point: if performance issues are ignored, assertions can much more concisely specify a program than can the code. This is just a corollary of something all programmers know, namely that it is often easier to write an inefficient program than an efficient one. Assertions are the ultimate in inefficiency and writing ease.

Prolog proponents have long used these same arguments, since Prolog makes it easy to concentrate on the spec and leave the implementation up to the compiler. But this approach misses the fact that much of the necessary creative work of programming is in coming up with a good implementation, not just in making a spec. It is valuable to separate a program into spec and implementation, as a divide-and-conquer way of simplifying the work, but that doesn't mean we can do away with the implementation programming altogether! Practical Prolog programs address implementation issues too, with the result that while a Prolog program is shorter than a typical imperative one, is still much longer than a proper specification.

There are many different formal methods, but all share the same fundamental idea: document the spec unambiguously, and ignore everything else. All tend to use mathematical thinking and the notation of first-order logic to achieve concise specifications. For instance, the spec for a routine to determine whether a number is nonprime might read (usually using standard mathematical symbols), "Given an integer x>=1, return whether there exist integers i and j, where 1<i<x and 1<j<x, such that i*j = x." A simple program is handily specified using such assertions, statements about the state of the program's variables before and after the program runs. These types of assertions are respectively called preconditions and postconditions.

Different formal methods use different variations of formal logic: witness Parnas' LD-relations vs Dijkstra's predicate transformers. But the differences are subtle and of interest only to those who make a living from writing academic papers. The substantial differences between formal methods arise in the more complex cases that first-order logic can't address, such as:

Most formal methods ignore the latter two issues, but stored-values are so fundamental that they must be addressed. The main differentiators among formal methods are superficial notation and representation of storage.


Representing Storage

There are two main approaches: making a mathematical model of the program object being specified, and interpreting the program's actions in terms of operations on the model; or keeping a history of operations on the program object, and defining future results in terms of that history. In the former, a mathematical concept like a set might be used to represent a program array. This is the more common approach; for instance, the formal method Z (pronounced "zed") is based on mathematical relations.

Use an operation history to define a program is even more circuitous, but provides a clever way to describe what a program does without ever actually representing storage. For instance, one knows that is the last call to a stack object was "push(5)", the result of a "pop()" call will be 5. The only state information the spec knows about is the complete history of calls to the object.

In truth, an operation history is just another sort of model, a list of calls. A good in-between example to show the connection is Parnas' trace assertion method (referenced in [Bauer]), in which the state of an object is maintained in its "trace", a sort of cleaned-up call history. For a stack object, the trace would contain only push calls; a pop call being defined as removing the last push call from the end of the trace.

Although unambiguous, the models used in formal methods are tedious, and the need to describe the program in two languages (models, and code) is part of what causes formal methods to sap productivity. I use models based on the program itself to ameliorate this effect.


Unified Specification Theory

A program is fully described by time sequences of possible inputs to and state changes from it. In the case of an object in an object-oriented program, this means the time sequence of calls to it, values returned and changed, and calls from it. For instance, an allowed time sequence might be:
  1. Someone calls obj.start(x).
  2. Within 1 second, obj calls x.whatever().
  3. It waits for x.whatever() to return.
  4. obj.start(x) allocates up to 1000 bytes from the global memory pool.
  5. The call to obj.start(x) returns with some changes to obj's state.
  6. Someone calls to obj.findOutSomething(x).
  7. obj.findOutSomething(x) returns with some value from obj's state.
Because most of these details don't matter in most programs, the full specification can be simplified. In most programs, the amount of time taken by the calls is assumed to be fast enough, normal allocations of memory are considered insignificant, the order of calls during processing (like the one to x.whatever()) is considered unimportant, and methods like findOutSomething(x) are assumed to do the same thing in each of the time sequences in which they occur.

As a result, object specs can usually be a more understandable and concise set of sequences of allowed calls (obj.start, obj.findOutSomething), along with assertions saying what each call does.

It's important to remember that this form is just a simplification of the more complete form, because sometimes the simplified form isn't sufficient. For instance, some methods must do things in a particular sequence, as in the internal sequencing example that queried the user: in that case a sequence spec must be used rather than a simple assertion. Other methods must act within a time period, and so the time value must be specified. The action of a method might be so different in its use in different sequences that it's best to describe its return value as part of the overall allowed call sequences to the object rather than as an assertion for all uses of the method.


References

Bauer, Brian; Documenting Complicated Programs, CRL Report No. 316, McMaster University, CRL (Communications Research Laboratory), TRIO (Telecommunications Research Institute of Ontario), Hamilton, ON, Canada, Dec 1995,

Gehani, N. and McGettrick, A.D.; Software Specification Techniques, ISBN 0-201-14230-9, Addison-Wesley, 1986.

Jacky, J.; The Way of Z, ISBN 0-521-55976-6, Cambridge University Press, 1997.

Liskov, B. and Guttag, J.; Abstraction and Specification in Program Development, ISBN 0-262-12112-3, MIT Press, 1986.

Scharbach, P.N.; Formal Methods: Theory and Practice, ISBN 0-8493-7140-6, CRC Press, 1989.

 
 
Substantive changes:
    Apr 12, 1997: created.
    May 31, 1997: added unified spec theory.
Copyright © 1997, Steve Colwell, All Rights Reserved
Home page