In his book A practical theory of programming [10] , [12] , Eric Hehner proposes and applies a radical reformulation of set theory in which the collection and packaging of elements are seen as separate activities. This provides for unpackaged collections, referred to as “bunches”. Bunches allow us to reason about non-determinism at the level of terms, and, very remarkably, allow us to reason about the conceptual entity “nothing”, which is just an empty bunch (and very different from an empty set). This eliminates mathematical “gaps” caused by undefined terms. We have made use of bunches in a number of papers that develop a refinement calculus for backtracking programs. We formulate our bunch theory as an extension of the set theory used in the B-Method, and provide a denotational model to give this formulation a sound mathematical basis. We replace the classical logic that underpins B with a version that is still able to prove the laws of our logic toolkit, but is unable to prove the property, derivable in classical logic, that every term denotes an element, which for us is pathological since we hold that terms such as 1/0 simply denote “nothing”. This change facilitates our ability to reason about partial functions and backtracking programs. We include a section on our backtracking program calculus, showing how it is derived from WP and how bunch theory simplifies its formulation. We illustrate its use with two small case studies .

Abstract Hoare and He’s unifying theories of programming (UTP) is a model of alphabetised relations expressed as predicates; it supports development in several programming paradigms. The aim of Hoare and He’s work is the unification of languages and techniques, so that we can benefit from results in different contexts. In this paper, we investigate the integration of angelic nondeterminism in the UTP; we propose the unification of a model of binary multirelations, which is isomorphic to the monotonic predicate transformers model and can express angelic and demonic nondeterminism.