6 - Theory of Abstract Machines

Summary

This chapter is devoted to the study of various theoretical developments concerning Generalized Substitutions and Abstract Machines. Our ultimate goal is to construct some set-theoretic models for Abstract Machines and Generalized Substitutions. By doing so, we shall be able to conduct further developments of Abstract Machines (i.e. loop and refinement in chapters 9 and 11 respectively) on these models rather than on the notation itself. This will prove to be very convenient.

In section 6.1, we prove that any generalized substitution defined in terms of the basic constructs of the previous chapter can be put into a certain normalized form. An outcome of this result is that any proof involving a generalized substitution can be done by assuming, without any loss of generality, that the substitution in question is in normalized form.

In section 6.2, we prove two convenient properties of generalized substitutions: namely, that the establishment of a post-condition distributes through conjunction and that it is monotonic under universal implication. The first will have a clear practical impact whereas the second is useful for theoretical developments. These properties were named by E.W. Dijkstra the Healthiness Conditions.

In section 6.3, we study the problem of termination and that of feasibility. We give a simple characterization of these properties. We also explain how the Generalized Substitution Language has exactly the same expressive power as the Before-after Predicates as introduced in section 4.4.