DUALITY: A simple formalism for the analysis of UNITY
Rutger M. Dijkstra · Formal Aspects of Computing · 1995
Abstract The ‘programming’ language DUALITY is presented and its utility for the description and analysis of UNITY is demonstrated. DUALITY is a simple language supporting demonic and angelic choice and two forms of tail-recursion. Starting from the predicate transformer semantics that was developed by C.S. Jutla, E. Knapp, and J.R. Rao for UNITY, we show that, given a UNITY program, we can write a program in DUALITY that has the same formal characteristics. This we use to reformulate and reprove some important theorems from the UNITY theory, viz. the ‘PSP-rule’ and the ‘completion rule’. Finally we show that the predicate transformers proposed by K.M. Chandy and B.A. Sanders for reasoning about concurrent computation also fit nicely within this framework.