The Specification of Computer Programs

Cover......Page __sk_0000.djvu
Copyright......Page __sk_0002.djvu
Contents......Page __sk_0007.djvu
Preface......Page __sk_0003.djvu
1.1 Why specifications are needed......Page __sk_0009.djvu
1.2 How specifications arise......Page __sk_0017.djvu
1.3 The customer\'s role......Page __sk_0027.djvu
1.4 Specifications and software contracts......Page __sk_0034.djvu
2.1.1 Pragmatics......Page __sk_0040.djvu
2.1.2 Deducibility......Page __sk_0048.djvu
2.1.3 Consistency......Page __sk_0053.djvu
2.1.4 Completeness......Page __sk_0054.djvu
2.2.1 Pragmatics......Page __sk_0060.djvu
2.2.2 Level of computable functions and relations......Page __sk_0062.djvu
2.2.3 Definability......Page __sk_0070.djvu
2.2.4 Some practical considerations......Page __sk_0073.djvu
2.3.1 Extensions revisited......Page __sk_0081.djvu
2.3.2 Composability of extensions......Page __sk_0083.djvu
2.3.3 Conservative extension......Page __sk_0084.djvu
2.3.4 Composability of conservative extensions......Page __sk_0086.djvu
2.3.5 Extension by definition......Page __sk_0087.djvu
2.3.6 Translation......Page __sk_0089.djvu
2.3.7 Composability......Page __sk_0094.djvu
2.3.8 Extension to MPC......Page __sk_0095.djvu
3.1 Specification languages and programming languages......Page __sk_0098.djvu
3.2 Permissiveness and its limitations......Page __sk_0106.djvu
3.3 Programs that satisfy specifications......Page __sk_0115.djvu
3.4 Programs as specifications......Page __sk_0130.djvu
3.5 Specifications as programs......Page __sk_0141.djvu
4.1 The step-by-step approach......Page __sk_0154.djvu
4.1.1 The evidence for the step-by-step approach......Page __sk_0156.djvu
4.1.2 Formal development and stepwise refinement......Page __sk_0163.djvu
4.2 The canonical step......Page __sk_0166.djvu
4.2.1 Definition of canonical step......Page __sk_0167.djvu
4.2.2 Another example......Page __sk_0175.djvu
4.3 Chain of specification/program links......Page __sk_0178.djvu
4.3.1 The Modularization Theorem......Page __sk_0182.djvu
4.3.2 Composing implementations......Page __sk_0183.djvu
4.3.4 Requirements for application processing in SIT......Page __sk_0185.djvu
4.3.5 Formal specification......Page __sk_0186.djvu
4.3.6 Canonical implementation steps......Page __sk_0195.djvu
4.4 Preservation of main properties......Page __sk_0200.djvu
4.4.1 Abstraction and main properties......Page __sk_0201.djvu
4.4.2 Modularity and main properties......Page __sk_0204.djvu
4.4.3 Plus ça change, plus c\'est la même chose......Page __sk_0207.djvu
4.5.1 Interpretations and the introduction of detail......Page __sk_0209.djvu
4.5.2 Another notion of refinement......Page __sk_0214.djvu
4.6 Notions of change......Page __sk_0215.djvu
4.7 The nature of useful tools......Page __sk_0219.djvu
A.1 Introduction......Page __sk_0226.djvu
A.2.1 Languages......Page __sk_0229.djvu
A.2.2 Rules of reasoning......Page __sk_0231.djvu
A.2.3 Theories......Page __sk_0235.djvu
A.3 Valuation systems......Page __sk_0237.djvu
A.4.1 The language......Page __sk_0241.djvu
A.4.2 Derivability in PC......Page __sk_0245.djvu
A.4.3 A valuation system for PC......Page __sk_0247.djvu
A.4.4 Theories in PC......Page __sk_0250.djvu
A.5 Modal and programming logics......Page __sk_0252.djvu
A.5.1 Modal logics......Page __sk_0253.djvu
A.5.2 Programming logics......Page __sk_0255.djvu
A.6 Many-sorted theories......Page __sk_0264.djvu
A.6.1 Many-sorted predicate calculus - MPC......Page __sk_0265.djvu
A.7 Interpretations between theories......Page __sk_0271.djvu
References......Page __sk_0280.djvu
Index......Page __sk_0283.djvu