ISSN:
1433-299X
Keywords:
Weakest (liberal) preconditions
;
Refinement
;
Fixed point transformations
;
Smyth power domain
;
Egli-Milner power domain
;
Recursion
;
Denotational semantics
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract An extension of Dijkstra's guarded command language is studied, including unbounded demonic choice and a backtrack operator. We consider three orderings on this language: a refinement ordering defined by Back, a new deadlock ordering, and an approximation ordering of Nelson. The deadlock ordering is in between the two other orderings. All operators are monotonic in Nelson's ordering, but backtracking is not monotonic in Back's ordering and sequential composition is not monotonic for the deadlock ordering. At first sight recursion can only be added using Nelson's ordering. We show that, under certain circumstances, least fixed points for non-monotonic functions can be obtained by iteration from the least element. This permits the addition of recursion even using Back's ordering or the deadlock ordering in a fully compositional way. In order to give a semantic characterization of the three orderings that relates initial states to possible outcomes of the computation, the relation between predicate transformers and discrete power domains is studied. We consider (two versions of) the Smyth power domain and the Egli-Milner power domain.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF01213603
Permalink