State constraints
J. C. Huang · Cambridge University Press eBooks · 2007
Consider a restrictive clause of this form: The program state at this point must satisfy predicate C, or else the program becomes undefined. By program state here we mean the aggregate of values assumed by all variables involved. Because this clause constrains the states assumable by the program, it is called a state constraint , or a constraint for short, and is denoted by /\C. State constraints are designed to be inserted into a program to create another program. For instance, given a program of the form of Program 2.1, a new program can be created, as shown in Program 2.2. Program 2.1 S 1 ; S 2 . Program 2.2 S 1 ; /\C; S 2 . Program 2.2 is said to be created from Program 2.1 by constraining the program states to C prior to execution of S 2 . Intuitively, 2.2 is a subprogram of 2.1 because its definition is that of 2.1 restricted to C. Within that restriction, 2.2 performs the same computation as 2.1. A state constraint is a semantic modifier. The meaning of a program modified by a state constraint can be formally defined in terms of Dijkstra's (1976) weakest precondition as follows. Let S be a programming construct and C be a predicate, then for any postcondition R, Axiom 2.3 wp(/\C;S, R) ≡ C ⋀ wp(S, R). Of course a constraint can also be inserted after a program.