Reasoning about programs by exploiting the environment

A method for making aspects of a computational model explicit in the formulas of a programming logic is given. The method is based on a new notion of environment -an environment augments the state transitions defined by a program''s atomic actions rather than being interleaved with them. Two simple semantic principles are presented for extending a programming logic in order to reason about executions feasible in various environments. The approach is illustrated by (i) discussing a new way to reason in TLA and Hoare-style programming logics about real-time and by (ii) deriving the first TLA and Hoare-style proof rules for reasoning about schedulers.