Semantics, Orderings and Recursion in the Weakest Precondition Calculus

摘要

An extension of Dijkstra's guarded command language is studied, includingsequential composition, demonic choice and a backtrack operator. Three orderings on this language are considered: a refinement ordering defined by Back, a 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. By extending the theory of fixed points in partial orderings, it is shown 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 order to give a semantic characterization of the three orderings that relates initial states to possible outcomes of the computation, the relations between predicate transformers and discrete powerdomains are studied. Three powerdomains are considered: two versions of the Smyth powerdomain and the Egli-Milner powerdomain. For each of them an isomorphism is proved with a suitable domain of predicate transformers.