Book contents
- Frontmatter
- Contents
- Preface
- 1 Introduction
- 2 State constraints
- 3 Subprogram simplification
- 4 Program set
- 5 Pathwise decomposition
- 6 Tautological constraints
- 7 Program recomposition
- 8 Discussion
- 9 Automatic generation of symbolic traces
- Appendix A Examples
- Appendix B Logico-mathematical background
- References
- Index
2 - State constraints
Published online by Cambridge University Press: 03 September 2009
- Frontmatter
- Contents
- Preface
- 1 Introduction
- 2 State constraints
- 3 Subprogram simplification
- 4 Program set
- 5 Pathwise decomposition
- 6 Tautological constraints
- 7 Program recomposition
- 8 Discussion
- 9 Automatic generation of symbolic traces
- Appendix A Examples
- Appendix B Logico-mathematical background
- References
- Index
Summary
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
S1; S2.
Program 2.2
S1; /\C; S2.
Program 2.2 is said to be created from Program 2.1 by constraining the program states to C prior to execution of S2. 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.
- Type
- Chapter
- Information
- Path-Oriented Program Analysis , pp. 15 - 20Publisher: Cambridge University PressPrint publication year: 2007