Proof obligations
From Successor ML
Contents |
Preamble
Each function or module generates proof obligations. While Hindley-Milner type checking guarantees no ‘wrongness’ at run-time, there are still very many ways that a program may fail:
- computer suffers a cosmic ray hit;
- operating system glitch;
- run-time support system or library module glitch;
- fails to terminate;
- process does terminate, but its not supposed to;
- partially incorrect.
For the first two and maybe three of these, there is (currently) nothing to be done but to introduce some form of fault-tolerance [1] into the program. This leads to redundancy, degrading the readability of the original program. Often enough, termination, or a lack thereof, is treated this way as well.
Often assertions [2] are used. However, some programming languages and associated run-time systems fail to allow for graceful recovery. Joe Armstrong, for the design of POTS switches, on the other hand, states these are just more trouble and code to be tested, in effect generating more proof obligations. He recommends simply trying again, and this seems to have worked for Ericsson, with code written in the (mostly) functional language Erlang [3].
Avoiding code obscuration
Sticking in assertions again obscures the central algorithm. One means of avoiding this is by variations on Design by Contract [4] (the name a trademark of Eiffel Software, Inc.). A good solution is found in papers by Findler and Felleisen (FF).
When handled properly, assertions form a subclass of fault tolerance techniques. The FF solution is one of the few instances, in fault tolerance, of avoiding overly obscure code.
When we assume no computer, operating system or run-time support failures, it is then possible, at least in principle, to automate most proof obligations. However, it is necessary to provide some linguistic support for this, and in a manner which clarifies the code rather than obscuring it.
Example
Standard ML’s fun is divisible into three cases:
- total functions;
- partial functions, which may or may not terminate, depending on argument;
- immortal processes, never terminating.
fun which are declared to be immortal processes should be easy to check for immortality with existing Hindley-Milner technology. fun declared to be partial might receive no termination checking. If a compiler is equipped with a prover of termination, fun declared to be total could then be checked for totality. Perhaps A. Abel’s Termination Checking with Types, Theoretical Informatics and Applications, 2004, is a suitable starting point.
Declaring totality
While the application of a minor variation of Occam’s razor implies one should to proliferate keywords, nonetheless this provides one means, not obscuring, of stating the totality expectation. For example, in an sML one might have,
- fun—total function declaration
- pfn—partial function declaration, SML’s fun
- agt—immortal agents
Other syntax may be preferable, but some means of expressing the intent is required.
Invariants
Both loop invariants and data structure invariants either enhance the clarity of algorithms or else, all too often, clutter the code to the point of obscurity.
By way of an analogy, the noweb tool offers a means to produce both a program and documentation about the program. A better analogy is the FF contract module. What can be done for important, but auxiliary, statements such as invariants to express these but avoiding code clutter?
As before, how to automatically discharge (some of) these proof obligations?
Concurrency
Since CMOS circuits are not going ever become much faster, just smaller, more programs are going to have to exploit so-called multi-core machines and distributed computing. This raises even more proof obligations, perhaps even harder to discharge.
