Junctive Compositions of Specifications in Total and General Correctness

AbstractFirst against a conventional total-correctness background of wp semantics, we define a small family of compositions for predicate-pair specifications based on simple logical conjunction and disjunction, discussing the formal properties and offering an intuitive operational interpretation of each. Three of these compositions we recognise as familiar; the fourth one, our concert, is new but lacks any apparent use. Then we re-interpret our compositions in the context of general correctness to very useful effect