Building mathematically correct programs

Utworzono: poniedziałek, 29 kwiecień 2019 14:55

Poprawiono: wtorek, 20 sierpień 2024 15:11

Odsłony: 6600

The issue of mathematically provable program correctness appeared for the first time in a work by Alan Turing published in conference proceedings On High-Speed Calculating Machines, which took place at Cambridge University in 1949. Later, that subject was investigated for several decades under the name of “proving program correctness”, but the developed methods never became a standard tool for the software industry. Consequently, many people concluded that research in this field is not worth the effort. A particularly explicit formulation of this opinion we found in a monograph, Deductive Software Verification, published in 2016:

For a long time, the term formal verification was almost synonymous with functional verification. In the last years, it became more and more clear that full functional verification is an elusive goal for almost all application scenarios. Ironically, this happened because of advances in verification technology: with the advent of verifiers, such as KeY, that mostly cover and precisely model industrial languages and that can handle realistic systems, it finally became obvious just how difficult and time-consuming the specification of the functionality of real systems is. Not verification, but specification is the real bottleneck in functional verification.

We strongly believe that the failure to prove program correctness in practical scenarios has two primary sources.

The first is an obvious observation that proofs of theorems are usually longer than the theorems themselves. Therefore, proofs of program correctness may contain thousands, if not millions of lines, which makes “hand-made proofs” unrealistic. Additionally, fully formalized proofs for “practical” programs are hardly possible due to the lack of formal semantics of the languages in which they have been written.

The second cause is even more critical — programs that are supposed to be proven correct are usually incorrect! Consequently, correctness proofs are regarded as methods of identifying errors in programs. Besides, the order, first a program and then the proof of its correctness, may seem natural for mathematicians — first a hypothesis and then its proof — but is somewhat awkward for engineers, who first prepare blueprints and calculations and only then build “their bridges”.

To our knowledge, the inadequacy of the approach of first writing a program and only then trying to prove its correctness was pointed out for the first time by Edsger Dijkstra in 1976 in his book A Discipline of Programming where he writes:

Between the lines (of his book) the reader may have caught a few more general messages. The first message is that it does not suffice to design a mechanism of which we hope that it will meet its requirements, but we must design it is such a form that we can convince ourselves — and anyone else for that matter — that it will, indeed, meet its requirements. And, therefore, instead of first designing a program and then trying to prove its correctness, we develop correctness proof and program hand in hand (our emphasis). (In actual fact, the correctness proof is developed slightly ahead of the program: after having chosen the form of the correctness proof, make the program so that it satisfies the proof’s requirements.)

Dijkstra formalized this idea using his weakest preconditions. A little later (1997 – 1981), Andrzej Blikle published a few papers technically different from Dijkstra’s approach but in a similar spirit. In recent years, Dijkstra’s ideas have been implemented by the authors of Dafny Environment and their followers under the name correct-by-construction. In Dijkstra’s approaches, the authors tacitly assume that their proposed program constructors are sound. They do not prove this soundness since their languages lack mathematical semantics. In our approach, we first show how to build programming languages with fully mathematical semantics and then how to develop sound program construction rules for such languages.

An early version of our project is also documented on ResearchGate