What makes our approach different from the others?

Utworzono: wtorek, 20 sierpień 2024 16:11

Poprawiono: wtorek, 20 sierpień 2024 16:18

Odsłony: 23

Historically, the ideas of denotational engineering emerged from the early works of A. Blikle, A.Blikle with A. Mazurkiewicz, and A.Blikle with A. Tarlecki. In turn, these works followed various approaches in this or another way. Below, we give credit to the authors that we have followed:

• generative grammars of N. Chomsky,
• denotational semantics of D. Scott’s and Ch. Strachey’s,
• C.A.R Hoare’s logic of programs,
• E. Dijkstra’s total correctness of programs and the derivation of correct programs,
• many-sorted algebras in computer science by J. A Goguen, J.W, Thatcher, E. G. Wagner and J. B. Wright,
• three-valued propositional calculus of J. McCarthy,
• abstract errors in program’s semantics originally introduced by Joe Goguen, and later also investigated from a perspective of a Hoare’s logic by J. V. Tucker and J. I. Zucker.

The main differences between our approach and other approaches to denotational semantics and program correctness are the following:

In the field of programming language design:

• our denotational models are based on set theory rather than D. Scott’s and Ch. Strachey reflexive domains,
• the denotations of programs are state-to-state functions rather than continuation-to-continuation,
• denotations are developed in the first place, and syntax is derived from them later; the process of the derivation of syntax is highly algorithmizable,
• the idea of a colloquial syntax allows making syntax user-friendly without damaging mathematical rigor,
• our denotational models include:
• error-detection mechanisms supported by three-valued boolean expressions and predicates, 
• objects and classes,
• SQL databases,
• simple Petri nets concurrency.

In the field of correct program development:

• the soundness of program construction rules is proved on the grounds of a denotation semantics of the involved language,
• the use of three-valued predicates enriches Dijkstra’s total correctness approach by a clean-termination property.