Logogram strony

Myśliciel A.Rodin

Rozmiar tekstu

Why this book?

Dowload the current working version of the book dated December 26th, 2018: A denotational engineering of programming languages.

Download a pdf version of this article.

 

It is a well-known fact that every user of a software application has to accept a disclaimer. Here is a typical example dating from 2018:

There is no warranty for the program, to the extent permitted by applicable law.  Except when otherwise stated in writing the copyright holders and/or other parties provide the program "as is" without warranty of any kind….

Is it thinkable that a producer of a car, a dishwasher or a building could request such a disclaimer from his client? Why then is the software industry an exception?

In my opinion, the cause of this situation is a lack of such mathematical models and tools for software engineers that would guarantee the functional reliability of products based on the way they have been designed and manufactured. The lack of mathematical models for programming languages also affects user-manuals of these languages which again contributes to a low quality of programs.

The problem of mathematically-provable program-correctness (i.e. reliability) appeared for the first time in a work of Alan Turing [4] in 1949. Later, for several decades, that subject was investigated usually as proving program correctness, but the developed methods never became everyday tools of software engineers. Finally, all these efforts were abandoned what has been commented in 2016 by the authors of a monography Deductive Software Verification [1]:

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.

In my opinion, the failure of constructing a practical system for proving programs correct has two sources.

The first lies in the fact that in building a programming language we start from syntax and only later — if at all — define its semantics. The second source is somehow similar but concerns programs: we first write a program and only then try to prove it correct.

To build a logic of programs for a programming language, one must first define its semantics on a mathematical ground. Since 1970-ties it was rather clear for mathematicians that such semantics to be “practical” must be compositional, i.e., the meaning of a whole must be a composition of the meanings of its parts. Later such semantics were called denotational — the meaning of a program is its denotation — and for about two decades researchers investigated the possibilities of defining denotational semantics for existing programming languages. Two most complete such semantics were written in 1980 for Ada [2] and for CHILL [3] in using a metalanguage VDM [3]. A little later, but in the same decade, a minor exercise in this field was a semantics of a subset of Pascal written in MetaSoft [4].

Unfortunately, none of these attempts resulted in the creation of software-engineering tools that would be widely accepted by the IT industry. In my opinion that fact was unavoidable since for the existing programming languages a full denotational semantics simply cannot be defined. That was, in turn, the consequence of the fact that historically syntaxes were coming first and only later researchers were trying to give them a mathematical meaning. In other words — the decision of how to describe things was before what to describe.

The second group of problems followed from a tacit assumption that in the development of mathematically correct programs the development of programs should precede the proofs of their correctness. Although this order is quite obvious in mathematics — first theorem and then its proof — it is rather unusual for an engineer who usually first performs all necessary calculations (the proof) and only then builds his bridge or aeroplane.

The idea “first a program and correctness-proof later” seems not only irrational but also practically unfeasible for two reasons.

First reason follows from the fact that a proof of a theorem is usually longer than the theorem itself. Consequently, proofs of program correctness should contain thousands if not millions of lines. It makes “hand-made proofs” rather unrealistic. On the other hand, automated proofs were not available by the lack of formal semantics for existing programming languages.

Even more important seem, however, the fact that programs that are supposed to be proved correct are usually incorrect! Consequently, correctness proofs are regarded as a method of detecting errors in programs. It means that we are first doing things wrong to correct them later. Such an approach does not seem very rational either.

As an attempt to cope with the mentioned problems I show in my book some mathematical methods that may be suitable for designing programming languages with denotational semantics. To illustrate the method an exemplary programming language, Lingua is developed from denotations to syntax. In this way, the decision of what to do (denotations) precedes the decision of how to express that (syntax).

Mathematically both the denotations and the syntaxes constitute many-sorted algebras, and the associated semantics is the homomorphism from syntax to denotations. As turns out there is a simple method — to a large extend algorithmizable — of deriving syntax from (the description of) denotations and the semantics from both of them.

At the level of data structures, Lingua covers Booleans, numbers, texts, records, arrays and their arbitrary combinations plus SQL databases. At the imperative level, this language contains structured instructions, type definitions, procedures with recursion and multi-recursion and some preliminaries of object programming. Of course, Lingua is not a real language since otherwise, the book would become unreadable. It is only supposed to illustrate the method which (hopefully) may be used in the future to design and implement a real language.

Ones we have a language with denotational semantics, we can define program-construction rules that guarantee the correctness of programs developed in using these rules. This approach consists in developing so-called specified metaprograms which are programs that syntactically include their specifications. The method guarantees that if we compose two or more correct programs into a new program or if we transform a correct program, we get a correct program again. The correctness proof of a program is hence implicit in the way the program is developed.

Basic mathematical tools used in this book are the following:

  1. fixed-point theory in partially ordered sets,
  2. the calculus of binary relations,
  3. formal-language theory and equational grammars,
  4. fixed-point domain-equations based on naive denotational semantics,
  5. many-sorted algebras,
  6. abstract errors as a tool for the description of error-handling mechanisms,
  7. three-valued predicate calculi of McCarthy and Kleene,
  8. the theory of total correctness of programs with clean termination.

References

[1]    Ahrent Wolfgang, Beckert Bernhard, Bubel Richard, Hähnle Reiner; Schmitt Peter H., Ulbrich Mattias (Eds.), Deductive Software Verification — The KeY Book; From Theory to Practice, Lecture Notes in Computer Science 10001, Springer 2016

[2]    Bjorner D., Oest O.N. (ed.), Towards a Formal Description of Ada, Lecture Notes in Computer Science vol. 98, Springer-Verlag 1980

[3]    Bjorner Dines, Jones B. Clif, The Vienna development method: The metalanguage, Prentice Hall International 1982

[4]    Blikle Andrzej, MetaSoft Primer ? Towards a Metalanguage for Applied Denotational Semantics, Lecture Notes in Computer Science, Springer Verlag 1987

[5]    Branquart Paul, Luis Georges, Wodon Pierre, An Analytical Description of CHILL, the CCITT High-Level Language, Lecture Notes in Computer Science vol. 128, Springer-Verlag 1982

[6]    Turing Alan, On checking a large routine, Report of a Conference on High-Speed Calculating Machines, University Mathematical Laboratory, Cambridge 1949, pp. 67-69.