Specifying Software: A Hands-On Introduction

Cover......Page __sk_0000.djvu
Copyright......Page __sk_0004.djvu
Contents......Page __sk_0005.djvu
Preface......Page __sk_0009.djvu
Introduction......Page __sk_0013.djvu
A Algorithms......Page __sk_0023.djvu
Introduction to Part A......Page __sk_0025.djvu
1.1 Case Study: Searching an Array......Page __sk_0027.djvu
1.2 Declarative Interface for Array Search......Page __sk_0030.djvu
1.3 Assertions......Page __sk_0031.djvu
1.4 Completing the Specification for Array Search......Page __sk_0037.djvu
1.5 Correctness of Code......Page __sk_0039.djvu
1.6 Additional Reading......Page __sk_0041.djvu
2.1 Some Programs for Array Searching......Page __sk_0043.djvu
2.2 Correctness Statements......Page __sk_0047.djvu
2.3 Simple Assignment Statements......Page __sk_0048.djvu
2.4 Substitution into Assertions......Page __sk_0050.djvu
2.5 Using Mathematical Facts......Page __sk_0052.djvu
2.6 Formal Proofs and Proof Tableaux......Page __sk_0054.djvu
2.7 Sequencing......Page __sk_0055.djvu
2.8 If Statements......Page __sk_0058.djvu
2.9 While Statements......Page __sk_0061.djvu
2.10 Termination of Loops......Page __sk_0065.djvu
2.11 Local Variables......Page __sk_0067.djvu
2.12 Discussion......Page __sk_0069.djvu
2.13 Additional Reading......Page __sk_0070.djvu
3.1 Searching an Array......Page __sk_0073.djvu
3.2 Minimal Entry of an Array......Page __sk_0077.djvu
3.3 Powers......Page __sk_0079.djvu
3.4 Division......Page __sk_0081.djvu
3.5 Binary Search in a Sorted Array......Page __sk_0083.djvu
3.6 The Number of Distinct Values in an Array......Page __sk_0088.djvu
3.7 Additional Reading......Page __sk_0091.djvu
4.1 For Loops......Page __sk_0093.djvu
4.2 Array-Component Assignment Statements......Page __sk_0095.djvu
4.3 Do-While Loops......Page __sk_0100.djvu
4.4 Sorting an Array......Page __sk_0103.djvu
4.5 Combining Correctness Statements......Page __sk_0111.djvu
4.6 Additional Exercises......Page __sk_0114.djvu
4.7 Additional Reading......Page __sk_0117.djvu
B Data Representations......Page __sk_0119.djvu
Introduction to Part B......Page __sk_0121.djvu
5.1 Informal Specification......Page __sk_0123.djvu
5.2 Formal Specification......Page __sk_0125.djvu
5.3 A Simple Implementation......Page __sk_0126.djvu
5.4 Program Organization......Page __sk_0128.djvu
5.5 Verification of a Data Representation......Page __sk_0131.djvu
5.6 A Caching Implementation......Page __sk_0134.djvu
5.7 Additional Reading......Page __sk_0136.djvu
6.1 Traversing a Sparse Set......Page __sk_0137.djvu
6.2 Sparse Arrays......Page __sk_0143.djvu
6.3 Sequences......Page __sk_0148.djvu
6.4 Bit-String Representation of Sets......Page __sk_0150.djvu
6.5 Reachability in a Directed Graph......Page __sk_0155.djvu
6.6 Sorting a Partially Ordered Set......Page __sk_0158.djvu
6.7 Additional Reading......Page __sk_0164.djvu
C Language Recognizers......Page __sk_0167.djvu
Introduction to Part C......Page __sk_0169.djvu
7.1 Strings......Page __sk_0171.djvu
7.2 Formal Languages......Page __sk_0172.djvu
7.3 Basic Operations on Languages......Page __sk_0174.djvu
7.4 Classes of Languages......Page __sk_0179.djvu
7.5 Additional Reading......Page __sk_0180.djvu
8.1 Basic Definitions......Page __sk_0181.djvu
8.2 Software Realization......Page __sk_0184.djvu
8.3 N ondeterminism......Page __sk_0188.djvu
8.4 State-Transition Diagrams with ε Transitions......Page __sk_0195.djvu
8.5 Reactive Systems......Page __sk_0196.djvu
8.6 Additional Reading......Page __sk_0201.djvu
9.1 From Regular Expressions to State Diagrams......Page __sk_0203.djvu
9.2 From State Diagrams to Regular Expressions......Page __sk_0208.djvu
9.3 Additional Operations on Regular Languages......Page __sk_0211.djvu
9.4 Nonregular Languages......Page __sk_0212.djvu
9.5 Other Formalisms......Page __sk_0216.djvu
9.6 Additional Reading......Page __sk_0217.djvu
10.1 Backus-Naur Formalism......Page __sk_0219.djvu
10.2 Derivations......Page __sk_0222.djvu
10.4 Ambiguity......Page __sk_0224.djvu
10.5 Push-Down Automata......Page __sk_0228.djvu
10.6 Non-Context-Free Languages......Page __sk_0232.djvu
10.7 Other Formalisms......Page __sk_0235.djvu
10.8 Additional Reading......Page __sk_0236.djvu
11.1 General Methods......Page __sk_0239.djvu
11.3 Recursive Descent......Page __sk_0240.djvu
11.4 Additional Reading......Page __sk_0253.djvu
D Unimplementable Specifications......Page __sk_0255.djvu
Introduction to Part D......Page __sk_0257.djvu
12.1 The Halting Problem......Page __sk_0259.djvu
12.2 The Church-Turing Thesis......Page __sk_0261.djvu
12.3 Unsolvability by Reduction......Page __sk_0262.djvu
12.4 Additional Reading......Page __sk_0264.djvu
Appendices......Page __sk_0267.djvu
A.1 Lexical Conventions......Page __sk_0269.djvu
A.2 Basic Types and Constants......Page __sk_0271.djvu
A.4 Variable Declarations......Page __sk_0273.djvu
A.6 Expressions......Page __sk_0274.djvu
A.7 Some Library Functions......Page __sk_0276.djvu
A.8 Statements......Page __sk_0278.djvu
A.9 Function Definitions......Page __sk_0281.djvu
A.10 More Library Functions......Page __sk_0282.djvu
A.13 Grammar......Page __sk_0285.djvu
A.14 Additional Reading......Page __sk_0290.djvu
B Hints for Selected Exercises......Page __sk_0291.djvu
Index......Page __sk_0297.djvu