Eternity variables to simulate specifications

Simulation of specifications is introduced as a unification and generalisation of refinement mappings, history variables, forward simulations, prophecy variables, and backward simulations. Eternity variables are introduced as a more powerful alternative for prophecy variables and backward simulations. This formalism is semantically complete: every simulation is a composition of a forward simulation, an extension with eternity variables, and a refinement mapping. The finiteness and continuity conditions of the Abadi-Lamport Theorem are unnecessary for this result.