- Utworzono: poniedziałek, 29 kwiecień 2019 15:12
- Poprawiono: wtorek, 26 maj 2020 14:13
- Odsłony: 3797

**A Denotational Engineering of Programming Languages**

Preprint version (improved and modified) by May 26^{th}, 2020 Download

Preprint version by 2019 09 30 registered as DOI 10.13140/RG.2.2.27499.39201/3

**Keywords:** Set-theoretic denotational semantics, many-sorted algebras, three-valued predicate calculus, a denotational model of types, abstract syntax, concrete syntax, total correctness with clean termination, sound program-construction rules.

The book is so far the main contribution to the project and is devoted to two research areas:

**Designing programming languages**along with their denotational models. A denotational model of a language consists of two many-sorted algebras — an algebra of syntax and an algebra of denotations — and a (unique) homomorphism from syntax to denotations called the semantics of the language. The algebra of denotation is defined in the first step, and syntax is derived from it later. This way guarantees the existence of a denotational semantics for the derived syntax. Mathematically this semantics is a homomorphism from syntax to denotations.**Designing sound program-constructors**for languages with denotational models. In my approach programs syntactically contain their total-correctness specifications. A program is said to be correct if it is correct wrt its specification. A program-constructor is sound if given correct component-programs it yields a correct resulting program.

Both methods are illustrated on an example of a virtual language **Lingua**. The first aspect of the book has been summarised in a paper described on the site On the development of a denotational model.