Unification of Four Versions of Program Semantics |
| |
Authors: | Ingrid Rewitzky Chris Brink |
| |
Affiliation: | (1) Department of Mathematics and Applied Mathematics, University of Cape Town, South Africa, ZA |
| |
Abstract: | Computing Science is a new subject, and we have not yet achieved the unification of theories that should support a proper
understanding of its structure. CAR Hoare and He Jifeng, 1998.
In this paper we use Priestley duality and Jónsson/Tarski duality to translate between four versions of program semantics: the relational model, predicate transformer semantics, information
systems, and powerdomains. Our point of entry is the relational model, a kind of Kripke semantics, in which programs are thought
of as input-output relations over a structured state space. Specifically, we present the state space as a certain kind of
Priestley space, and programs as certain structure-preserving relations over such a space. We then derive, in circular fashion,
a predicate transformer semantics from the relational model, an information system from the predicate transformer semantics,
a powerdomain from the information system, and the original relational model back again from the powerdomain. The information
system is also shown to be related to Hoare logic. To clarify the intuition behind this approach we present a case study,
which is a ‘Priestley version’ of the so-called universal domain due to Plotkin, and we explicate various ideas about properties of programs and predicates in terms of this case study.
Received April 1997 / Accepted in revised form February 1998 |
| |
Keywords: | : Priestley duality Jónsson/Tarski duality Program semantics Relational model Predicate transformer semantics Information system Hoare logic Powerdomain |
本文献已被 SpringerLink 等数据库收录! |
|