Formal Methods

Intro
Formal methods are a type of software engineering that deals with logically rigorous ("formal")
methods of specification and proof. Actually the methods are much more broad than simply for
software engineering. Anything that must be specified, or described in an unambiguous manner is a
good candidate for a formal language. That's the first part: the specification. The second part is proving
certain properties of the specification, such as a certain thing must always be true. In the jargon, this
would be an invariant, because it must always be so but in general it is a type of theory.

The specification describes what the system must do, the theories describe what it should do. Not as
optional details but what it should do if the specification is correct. The theories form a check on the
specification, and the proof is that check. You may find that your specification is not sufficient to
describe the real operation.

Example
For example, if we were designing a dynamic memory allocator, we would specify the memory itself, a
system for record-keeping and some operations on that allocate and free memory. Now suppose we
want to prevent memory leaks. In this context I mean there should never be a request for memory that
gets refused when enough memory is actually available. (Fragmentation does not count in this
example. I consider each fragment a separate unit too small to satisfy the request). This would be a
failure of the record-keeper to appropriately log when memory is freed up. We could just put in a
requirement in the specification that says 'the allocator must never refuse a request when there is
actually enough memory free'. But that does the programmer no good. Its possible you specified a
record keeping mechanism that does not fulfill the task. This could happen if a task ended, and no
specification was written that the OS manually free any memory allocated to that task. The memory is
actually free, but it is recorded as used.

Each specification is written similarly to a computer program, in that it has a formal language with
well-defined semantics. However, its not your usual type of development. Instead of describing the
function of a particular module as a sequence of operations (how it should do its job), we focus all our
efforts onto describing what it should do. Each operation is then a set of operations on its inputs
(some languages have explicit outputs, others any input may also be altered...I prefer the former). The
dance is then to specify enough in general terms to obtain the goal (we check this with proving) but
not so much that we start specifying implementation.

Formal Tools

For generic theorem proving, I like to use PVS, a (recently open-source) free theorem prover and
specification language from SRI international. I like PVS because it is free, it is extremely powerful,
and its really made for professional use. It was made with the concept that previous effort could be
reused and proofs in-progress could be saved. It also has a neato TeX output that converts the code
into mathematical notation. You can find it here.

I have used a program called SPIN for temporal logic, but not extensively. SPIN is kind of neat for
modelling concurrency, such as multiple threads in a given program. Actually SPIN was the first
formal methods tool I ever used, and sort of got me interested in the field. For an introduction to SPIN,
see the book:
The SPIN Model Checker: Primer and Reference Manual by Gerard J Holtzmann, Boston:
Addison-Wesley, 2004. ISBN 0-321-22862-6

A really cool software tool called Spark has been developed by the good folks at Praxis. This is a
formal language that rides in comments of Ada programs. By defining each subroutine as a set of
inputs, outputs, external (global) variables and invariants, Spark can actually analyze your source
code to see if it meets the specification. A limited free version is available with the book:
High Integrity Software: The SPARK Approach to Safety and Security by John Barnes,
Boston:Addison-Wesley, 2003. ISBN: 0321136160

Reference Pages
http://www.macs.hw.ac.uk/~lilia/ar/ar.html - An excellent set of courses at on automated proof that
emphasize PVS. Great to start you off in the dizzying world of proofs. Just found this today!

Hints to Specifiers - CMU-CS-95-118R - Prof. Wing at Carnegie Mellon has this excellent paper on the
pitfalls of specification writing. Once you go to writing your own these pointers are invaluable.

Programming from Specifications - Caroll Morgan's textbook on-line. The other side of the coin: how to
translate a particular programming construct (such as a for loop) into a formal specification. I like to
think of it as a programmer's view of formal specification.