B. Moszkowski
University of Newcastle upon Tyne. 1994
A logic for reasoning about sequential and parallel behaviour must support some form of compositionality. That is, much of the proof of a system should be decomposible into proofs of its parts. We discuss some important and easily described classes of properties which are readily imported and exported between temporal scopes. We call such properties very compositional since they support a methodology of specification and proof which is especially modular and reusable. Our presentation uses Interval Temporal Logic [13, 7, 14] as the notation in which all behaviour is described and proved. We give a powerful and elegant ITL proof system. It has been used by us to rigorously prove hundreds of theorems and derived inference rules, including a number for parallel systems involving message-passing, timing constraints and shared write-access. We believe that very compositional properties will be of interest to anyone involved with the specification and verification of computer systems.