The book

Utworzono: poniedziałek, 29 kwiecień 2019 15:12

Poprawiono: czwartek, 21 listopad 2024 12:32

Odsłony: 10260

A Denotational Engineering of Programming Languages

Preprint version (improved and modified) by Novebmer 21^st, 2024 Download
Preprint version by 2019 09 30 has been registered as DOI  10.13140/RG.2.2.27499.39201/3

As mentioned in the preceding pages, our book contains many thoughts developed during 1960-1990 but later abandoned. One of the teams developing these ideas was working at the Institute of Computer Science of the Polish Academy of Sciences, and two of us — A.Blikle and A.Tarlecki — enjoyed working there. We then created a semi-formal metalanguage called MetaSoft dedicated to formal definitions of programming languages.

Sec.2 introduces general mathematical tools used later in describing our basic model. In particular, they include:
a formal, but not formalized, definition of MetaSoft,

• fixed-point theory in partially ordered sets,
• the calculus of binary relations,
• formal-language theory,
• fixed-point domain equations based on so-called naive denotational semantics (rather than Scott and Strachey’s reflexive domains),
• many-sorted algebras,
• abstract errors as tools for the description of error-handling mechanisms,
• three-valued predicate calculi of McCarthy and Kleene,
• equational grammars (equivalent to Chomsky’s grammars and BNF’s),
• syntactical algebras based on equational grammars,
• a short half-formal reminder of LL(k) grammars.

It should be emphasized in this place that Sec.2 may discourage less mathematically oriented readers. These readers may skip reading this section, maybe except Sec. 2.1 where notational conventions are explained. All mathematical tools and facts mentioned there are necessary to prove the mathematical soundness of our approach but are not prerequisites to understanding it.

Sec. 3 includes an intuitive description of our model and defines significant milestones to be passed through in its construction.

Sec. 4 is devoted to developing a general model of data structures and their types. Types, which are frequently regarded as sets of data, in our model are finitistic structures that indicate the “shapes” of the corresponding data. This approach allows for a definition of an algebra of types at a data level and an algebra of the denotations of type expressions at the level of denotations.

In Sec. 5 we introduce three fundamental concepts: a class, an object, and a state. We also discuss the visibility (privacy) issues of objects’ attributes, typical of object-oriented mechanisms.

Sec. 6 describes the core of our model and is devoted to denotations. Here, we define the carriers and the constructors of an algebra of denotations. From a practical viewpoint, when we design an algebra of denotations, we make significant decisions on the tools offered by a language to programmers.

Once denotations are defined, we proceed in Sec. 7 to the derivation of syntax. Here, given a description of the algebra of denotations, we derive step-by-step three syntaxes: an abstract syntax, a concrete syntax, and a colloquial syntax. Formally, these syntaxes constitute algebras and are described by equational gram-mars. We also show how to derive a formal definition of a function of semantics once we are given an algebra of denotations and “its” algebra of syntax.

Sec.8 is devoted to an abstract theory of partial and total correctness of programs. This theory bases on an algebra of binary relations, making it universal for many programming languages.

In Sec. 9, starting from Lingua, we develop a corresponding language for validated programming, Lingua-V. In this case, however, we do not build a logic of programs — as C.A.R. Hoare or E. Dijkstra did — but we define a list of (proved) rules for the construction of correct programs.

Sec. Sec. 10 and 11 are devoted to enriching Lingua with SQL mechanisms. Since we do not expect our reader to be familiar with SQL details, we provide in Sec. 10 an intuitive introduction to its primary tools. In Sec 11, we give these tools a denotational model. As it turns out, extending Lingua to Lingua-SQL is more than just a simple enrichment of a source algebra of denotations by new carriers and constructors. It requires profound modifications and, therefore, offers a non-trivial example of enhancing a denotational model by new mechanisms.

Even more substantial changes to our model are necessary when, in Sec. 12, we introduce some concurrency mechanisms into Lingua. In this case, the flowchart-like structures of our programs are replaced by simple Petri nets enriched by the trace languages of Mazurkiewicz.

In Sec. 13, we included short remarks about what remains to be done in our project. In particular, we are talking about two computer-assisted work environments: one for the designers of languages using our method and another for programmers in such languages.

The aspect of designing programming languages has been summarised in a paper described on the site On the development of a denotational model.