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
5 - Pathwise decomposition
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
In this chapter we discuss the concept of pathwise decomposition in more detail. First, we need to formally define some terms so that we can speak precisely and concisely.
In abstract, by pathwise decomposition we mean the process of rewriting a program into an equivalent program set, consisting of more than one element. To be more precise, we have the following definition.
Definition 5.1a
Given a piece of source code /\C;S, to decompose it pathwise is to find a program set {/\C1;S1, /\C2;S2, …, /\Cn;Sn} such that
/\C;S ⇔ {/\C1;S1, /\C2;S2, …, /\Cn;Sn},
n > 1,
Ci ⋀ Cj ≡ F for any i ≠ j, and
C1 ⋁ C2 ⋁… ⋁ Cn. ≡ C.
Presumably, it is written to implement a function that can be decomposed pathwise, as subsequently described.
Definition 5.1b
Given a function, say, f, to decompose it pathwise is to rewrite it in such a way that it includes a description of the following elements:
f: X → Y,
f = {f1, f2,…, fm},
X = X1 ⋃ X2 ⋃… ⋃ Xm,
fi: Xi → Y for all 1 ≤ i ≤ m.
Definition 5.2a
A set {/\C1;S1, /\C2;S2,…, /\Cn;Sn} of subprograms is said to be compact if, for any i ≠ j, Ci ⋀ Cj ≡ F implies that Si is not logically equivalent to Sj.
Intuitively, a program set is said to be compact if every subprogram computes a different function. We can characterize a set of subfunctions in a similar manner.
- Type
- Chapter
- Information
- Path-Oriented Program Analysis , pp. 39 - 54Publisher: Cambridge University PressPrint publication year: 2007
- 1
- Cited by