Temporal operators viewed as predicate transformers
In this paper we present a calculus of temporal operators that is intended as an alternative to temporal logic in program verification. Temporal logic is a form of modal logic, designed for the description of time-dependent phenomena. Several different kinds of temporal logic have been proposed, but in the present paper only the linear time version [13] is treated. A common characteristic of all kinds of temporal logic is that they require a large number of irregularly-shaped axioms; as a result, proofs within such a system tend to be tortuous and mystifying. The cause of this problem is that these logics were designed to satisfy theoretical demands such as completeness, not to optimize ease of manipulation. It is our contention that the calculus proposed below, while equivalent in its descriptive power, places less of a burden on the user. Our approach was inspired by work of Boute [3] and Hehner [8], but diverges from these in that we refrain from explicit mention of time coordinates. In [5], E.W. Dijkstra and C.S. Scholten presented a version of predicate calculus based on equational reasoning rather than natural deduction. Their work, whose style owes more to algebra than to logic, leads to very smooth calculational proofs. We emphasize that their calculus, although quite rigorous in a mathematical sense, is not a formal system: for instance, it allows every theorem from mathematics to be used in proofs without the addition of anything like ‘domain axioms’. This may be a disadvantage if one is interested in proving properties of the calculus itself, but it is a great advantage when the calculus is being used as a tool in proving properties of actual programs [4]. When the same principles are applied to program semantics, the axioms and inference rules of Floyd-Hoare logic are replaced with the definition of a class of predicate transformers called weakest preconditions. In the present paper, we shall follow a similar path and enrich the calculus of Dijkstra and Scholten with the definition of a class of predicate transformers called shift operators, to be used as a replacement for the axioms and inference rules of temporal logic. The organization of the paper is as follows. In section 2 we define the concept of a shift operator, and in section 3 we show how a shift operator can be used to construct a predicatetransformer model for the axioms of temporal logic. In section 4 we prove that, in fact, every such model can be obtained from a shift operator, which establishes the equivalence of both approaches. Finally, in section 5, examples demonstrate that reasoning with shift operators