Eliminating the substitution axiom from UNITY logic

Abstract

The UNITY substitution axiom, “if (x=y) is an invariant of a program, then x can be replaced by y in any property of the program”, is problematic for several reasons. In this paper, dual predicate transformers sst and wst are introduced that allow the strongest invariant of a program to be expressed, and these are used to give new definitions for the temporal operators unless and ensures . With the new definitions, the substitution axiom is no longer needed, and can be replaced by a derived rule of inference which is formally justified in the logic. One important advantage is that the effects of the initial conditions on the properties of a program are formally captured in a convenient way, and one can forget about substitution in formal treatments of the UNITY proof system while still having it available when desirable to use during the derivation of programs. Composibility and completeness of the modified logic are also discussed.