Partially defined computer instructions and guards

AbstractWe here extend our earlier work on the theory of computer instructions to consider instructions which are only partially defined. For every such instruction, we assume that it is defined whenever a certain Boolean expression is true; we refer to such a Boolean expression as a guard, following Dijkstra. This is a special case of a more general function on the set of states of a computer, representing an expression in a programming language. Many constructs for instructions now generalize to partially defined instructions; in particular, we define the notion of conditional input and output regions, as well as the relevant region of a more general expression. Fundamental theorems about instructions generalize to theorems about guards and about partially defined instructions. We also define the parallel execution of such instructions, which is useful in validating a generalized instruction commutativity criterion