This paper compares two verification methods for inevitability properties of nondeterministic transition systems, the “always” method and the “sometime” method. These methods are abstractions of program-verification techniques due to Floyd and Burstall, respectively.

The main research contribution of this paper is a translation that transforms proofs in the rich “sometime” method into proofs in the simpler “always” method. While this general translation avowedly does not yield natural proofs of correctness, it is mathematically satisfying. Unavoidably, some of the examples and constructions seem rather complex and make for arduous reading. Nevertheless, the paper should be of interest to researchers in the formal aspects of program verification.