Comments on ''Always-true is not invariant'': Assertional reasoning about invariance (Q1183477): Difference between revisions

\textit{A. J. M. van Gasteren} and \textit{G. Tel} [Inf. Process. Lett. 35(6), 277-279 (1990; Zbl 0705.68059)] seem to suggest that avoiding operational arguments in reasoning about program correctness means avoiding reasoning about always-true. However, in UNITY \textit{K. M. Chandy} and \textit{J. Misra} [Parallel program design. A foundation, Reading/MA: Addison Wesley (1988; Zbl 0717.68034)]; \textit{J. S. Pettersson} [Assertional reasoning about invariance, Inf. Process. Lett. 40(5), 231-233 (1991)] reasoning about always-true can be performed by assertional means. \textit{T. Sanders} [Formal Aspects Comput. 3(2), 189-205 (1991; Zbl 0715.68059)] provides a semantic basis for this; a unifying framework, which contains both invariant and always-true. The author reformulates the relevant parts of this unifying framework using Hoare logic and assertions as the underlying model instead of the theory of predicate transformers, which is used by \textit{Sanders}. A complete exposition can be found in \textit{Pettersson's} work. \textit{van Gasteren} and \textit{Tel} also state that invariance is preserved under composition of programs, whereas always-true is not. However, under certain conditions always-true is also preserved under composition of programs. From \textit{Sanders'} theorem for composition of (UNITY) programs a theorem is obtained which shows this.