Logogram strony

Myśliciel A.Rodin

Narodziny gwiazdy

Rozmiar tekstu

What is the project about

My project Denotational Engineering has started in 2015 with writing the book described on the site The book. So far it is a “private” project, i.e. not assigned to any institution.

Mathematically the current project is a follower of an earlier project MetaSoft developed in the years 1971-1996 in the Institute of Computer Science of the Polish Academy of Sciences. A list of major contributions to that project has been listed on the site References to MetaSoft.

In my current project I concentrate on two fields:

  1. Denotational models of programming languages developed in “reverse order,” i.e. from denotations to syntax. This method of designing programming languages guarantees that the developed languages have fully formalised denotational semantics.
  2. The development of correct programs rather than proving programs correct. Given a language with denotational semantics, one can define program-construction rules that preserve program correctness. Each such rule, given correct programs as arguments yields a correct program as a result. Consequently proving program correctness is limited to initial modules in a bottom-up program development.

The following mathematical techniques are used in this project:

  1. Denotational semantics where domains are sets rather than Scott-Strachey reflexive domains.
  2. Many-sorted algebras. A denotational model of a programming language consists of three such algebras: of denotations, of the corresponding abstract syntax and of a concrete syntax (programmer’s syntax). The way of constructing this model guarantees the existence of a homomorphism from concrete syntax to denotations. This homomorphism constitutes the denotational semantics of concrete syntax.
  3. Three-valued predicate calculus based on a three-valued propositional calculus of J. McCarthy. This calculus allows for the description of an error-elaboration mechanism in a denotational framework.
  4. Program-construction rules based on Hoare’s logic with clean termination (no error message). Here three-valued predicates are involved again.
  5. Equational grammars as a certain generalization of context-free grammars.

I am currently working on the development of a denotational model, and of program-construction rules, for a virtual programming language Lingua.

On the applicative level, this language is offering Booleans, numbers, texts, lists, multilevel arrays, records and their arbitrary combinations. Besides that also SQL data — rows, tables and databases. All data are associated with types. The latter are regarded as independent entities, i.e. they are user-definable, structured and storable. The types of Lingua also provide a framework for SQL integrity constraints.

On the imperative level, Lingua offers typical structured-instructions (including SQL mechanisms) plus procedures with recursion and mutual recursion. Object programming has been only sketched. Concurrency has not been tackled so far.

Actually, I am seeking potential partners who would be willing to cooperate in the further development of the project, both on its theoretical level as well as on the implementation of Lingua and on the development of an appropriate environment for language designers and for programmers. See: What remains to be done and An invitation to the project.

The project is also documented on ResearchGate