What is new in the project

Utworzono: poniedziałek, 29 kwiecień 2019 15:07
Poprawiono: środa, 01 maj 2019 11:56
Odsłony: 5726

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.