What is new in the project

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

Poprawiono: środa, 01 maj 2019 11:56

Odsłony: 5376

The project covers ideas and techniques described in my early papers published in the years 1971-1996 and recently summarised and extended in a preprinted book A Denotational Engineering of Programming Languages. All these contents base on concepts which have been well-known for years (see Sec.1.4 of the book for references):

• denotational semantics of D. Scott’s and Ch. Strachey’s,
• generative grammars of N. Chomsky’s,
• T. Hoare’s logic of programs,
• many-sorted algebras introduced to the mathematical foundations of computer science by J. A Goguen, J.W, Thatcher, E.G Wagner and J.B Wright,
• three-valued propositional calculus of J. McCarthy.

What — I believe — is new in the project, is the following:

1. Programming language design and development:
   1. A formal, and to a large extent an algorithmic method of systematic development of syntax from denotations and of a denotational semantics from both of them.
   2. The idea of a colloquial syntax which allows making syntax user-friendly without damaging a denotational model to much.
   3. The systematic use of error-elaboration in programs supported by a three-valued predicate calculus.
   4. A denotational model based on set-theory rather than on Scott-Strachey reflexive domains which makes the model much simpler.
   5. A model of data-types that covers not only structured and user-defined types but also SQL integrity constraints.
2. The development of correct programs
   
   1. A method of systematic development of correct programs with their specifications, rather than developing programs first and trying to prove them correct later.
   2. The use of three-valued predicates to extend Hoare’s logic by a clean termination property and to describe error elaboration mechanisms.
3. General mathematical tools
   1. Equational grammars applied in defining the syntax of programming languages.
   2. A three-valued calculus of predicates applied in designing programming languages and in defining sound program constructors for such languages.