by Andrzej Blikle (Institute of Computer Science, Polish Academy of Sciences)
This project is devoted to the development of programming languages in a way that guarantees the existence of denotational semantics for them. Once such a language has been developed, we can derive such program-construction rules, which guarantee the correctness of programs constructed by their means.
It is a well-known fact that every user of a software application has to accept a disclaimer, such as, “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 … ”.
I believe that the cause of this situation is a lack of mathematical tools for software engineers (commonly available for all other engineers) that would guarantee the functional reliability of programs based on how they have been designed and developed. Even though a lot of research has addressed this problem since 1960, and several mathematical methods have been developed, none has become a standard in the software industry.
The project is devoted to the elaboration of two methods. The first concerns the development of programming languages along with their denotational models (semantics) and is called “denotational engineering”. The second is devoted to developing programs that are correct with respect to their specifications, the latter nested in the codes of programs.
In our approach, the design process of a programming language starts from the development of its algebra of denotations, called AlgDen, described in a metalanguage, MetaSoft. Once such a description is completed, we derive from it a corresponding syntax described by an equational grammar. The syntax also constitutes an algebra that we call AlgSyn. Our method guarantees the following:
- There exists a (unique) denotational semantics of AlgSyn, which is a homomorphism – let's denote it by Sem – from AlgSyn into AlgDen.
- A context-free grammar corresponding to AlgSyn may be half-algorithmically derived from the description (in MetaSoft) of AlgDen.
- A denotational definition of Sem (in MetaSoft) may be algorithmically derived from the definitions of both algebras.
- The definition of Sem may be transformed into an interpreter of the designed language. Again, this task may be performed, to a large extent, algorithmically.
Once we have a language with full denotational semantics, we can derive a repertoire of program constructors that guarantee the correctness of constructed programs. In this approach, each program consists of a “programming layer”, which is a code, and a “descriptive layer”, which constitutes this program's specification written in a formalised dialect of MetaSoft. A program is called “correct” if its programming layer is totally correct with clean termination (no error messages) [1] with respect to its descriptive layer. This approach offers an alternative to first developing programs and only then trying to prove them correct.
It is a well-known fact that the method of proving programs correct faces two significant challenges:
- Since a proof is usually longer than a theorem, a proof of program correctness must be longer than the program itself. That is, frankly speaking, somewhat discouraging.
- Even more discouraging is that programs whose correctness we intend to prove are practically never correct.
In our method of developing correct programs, rather than proving programs correct, we do not avoid proofs at all, but we simplify them to a large extent. Whenever we intend to apply a correctness-preserving constructor to some earlier-developed correct programs, we usually have to prove an implication between two formulas that are mathematically relatively simple but may contain many variables. There may be as many variables as declared in the program, which can make the corresponding proof hardly manageable by hand. In this case, however, we may easily use a theorem prover.
The project's current state has been described in a draft version of a book [L1] and in an article published by Springer [L2]. The book includes material taught twice as a facultative one-semester course at the Department of Mathematics, Informatics, and Mechanics of the University of Warsaw in the years 2020 and 2021. The first course ended with the development (by students) of an interpreter (written in OCaml) of a programming language, Lingua-WU (WU for Warsaw University), developed by the method of denotational engineering. The language is imperative, strongly typed, and includes recursive procedures with mutual recursion. The book also contains a list of sound program-construction rules, with appropriate logical background based on three-valued predicates, and a denotational model of a subset of Stuctured Query Language (SQL). Further research in progress tackles denotational models of:
- concurrency at the level of simple Petri nets;
- object-oriented mechanisms;
- a subset of OCaml to study its mechanism of parametric types.
At the mathematical level, denotational engineering is based on the following:
- Fixed-point theory in partially ordered sets
- A calculus of binary relations
- Formal-language theory and equational grammars
- Fixed-point domain equations based on so-called “naive denotational semantics” [3], where denotational domains are usual sets rather than Scott-Strachey reflexive domains
- Many-sorted algebras
- The development of a language from denotations to syntax [2]
- Abstract errors as a tool for the description of error-handling mechanisms
- Three-valued predicate calculi
- A theory of total correctness of programs with clean termination [1].
The project is currently not associated with any institution and is developed by me with two colleagues from the University of Warsaw. The project offers several opportunities for MS and PhD dissertations in theory and software engineering as well as several research problems to be addressed [L3]. It is open to all interested parties.
Links:
[L1] https://moznainaczej.com.pl/what-has-been-done/the-book
[L2] https://moznainaczej.com.pl/what-has-been-done/on-the-development-of-a-denotational-model
[L3] https://moznainaczej.com.pl/what-remains-to-be-done
References:
[1] A. Blikle, “The Clean Termination of Iterative Programs,” Acta Informatica, vol. 16, pp. 199-217, 1981.
[2] A. Blikle, “Denotational Engineering,” Science of Computer Programming, vol. 12, North-Holland, 1989.
[3] A. Blikle A. Tarlecki, “Naïve denotational semantics,” Information Processing 83, R.E.A.Mason, Ed, Elsevier Science Publishers BV (North-Holland), 1983.
Please contact:
Andrzej Blikle, Institute of Computer Science, Polish Academy of Sciences, Poland
