DUALITY: A Simple Formalism for the Analysis of UNITY

摘要

The authors present the programming language DUALITY and demonstrate its utilityfor the analysis of UNITY. DUALITY is a simple language supporting demonic and angelic choice and two forms of tail-recursion. Starting from the predicate transformer approach to the semantics of parallel programs, they show that, given a UNITY program, they can write a program in DUALITY that has the same formal characteristics. This they use to reformulate and reprove some important theorems from the UNITY theory, viz. the 'PSP-rule' and the 'completion rule'. Finally the authors show that the conjunctive predicate transformers for reasoning about concurrent computation also fit nicely within this framework.