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
4 - Program set
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
As mentioned before, by inserting a constraint into a program, we shrink the domain for which it is defined. To reverse this process, we need to be able to speak of, and make use of, a set of subprograms. To this end, a new programming construct called a program set is now introduced. The meaning of a program set, or a set of programs, is identical to the conventional notion of a set of other objects. As usual, a set of n programs is denoted by {P1, P2, …, Pn}. When used as a programming construct, it describes the computation prescribed by its elements. Formally, the semantics of such a set is defined in Axiom 4.1.
Axiom 4.1
wp({P1, P2, …, Pn}, R) ≡ wp(P1, R) ⋁ wp(P2, R) ⋁ … ⋁ wp(Pn, R).
The choice of this particular semantics is explained in detail at the end of this chapter. A program set so defined has all properties commonly found in an ordinary set. For instance, because the logical operation of disjunction is commutative, a direct consequence of Axiom 4.1 is Corollary 4.2.
Corollary 4.2
The ordering of elements in a program set is immaterial, i.e.,
{P1, P2} ⇔ {P2, P1}.
Furthermore, because every proposition is an idempotent under the operation of disjunction, we have Corollary 4.3.
Corollary 4.3
P ⇔ {P} ⇔ {P, P} for any program P.
In words, a set is unchanged by listing any of its elements more than once.
- Type
- Chapter
- Information
- Path-Oriented Program Analysis , pp. 31 - 38Publisher: Cambridge University PressPrint publication year: 2007
- 1
- Cited by