Specifying Software: A Hands-On Introduction

Pirmais vāks
Cambridge University Press, 2002. gada 25. febr. - 289 lappuses
This innovative volume provides a hands-on introduction to techniques for specifying the behavior of software components. A text for a second-year undergraduate course in Computer Science and Computer Engineering programs, it is also suitable for self-study. This book will help students to improve their programming skills and gain a sound foundation and motivation for subsequent courses in advanced algorithms and data structures, software design, formal methods, compilers, programming languages, and theory. The main topics covered are techniques for using programmer-friendly assertional notations to specify, develop, and verify small but non-trivial algorithms and data representations, and the use of state diagrams, grammars, and regular expressions to specify and develop recognizers for formal languages. The presentation is based on numerous examples and case studies appropriate to the level of programming expertise of the intended readership.
 

Saturs

Specifying Algorithms
15
12 Declarative Interface for Array Search
18
13 Assertions
19
14 Completing the Specification for Array Search
25
15 Correctness of Code
27
16 Additional Reading
29
Verifying Algorithms Basic Techniques
31
22 Correctness Statements
35
Language Recognizers
155
Introduction to Part C
157
Basic Concepts
159
72 Formal Languages
160
73 Basic Operations on Languages
162
74 Classes of Languages
167
75 Additional Reading
168
StateTransition Diagrams
169

23 Simple Assignment Statements
36
24 Substitution into Assertions
38
25 Using Mathematical Facts
40
26 Formal Proofs and Proof Tableaux
42
27 Sequencing
43
28 If Statements
46
29 While Statements
49
210 Termination of Loops
53
211 Local Variables
55
212 Discussion
57
213 Additional Reading
58
Verifying Algorithms Some Examples
61
32 Minimal Entry of an Array
65
33 Powers
67
34 Division
69
35 Binary Search in a Sorted Array
71
36 The Number of Distinct Values in an Array
76
37 Additional Reading
79
Additional Verification Techniques
81
42 ArrayComponent Assignment Statements
83
43 DoWhile Loops
88
44 Sorting an Array
91
45 Combining Correctness Statements
99
46 Additional Exercises
102
47 Additional Reading
105
Data Representations
107
Introduction to Part B
109
Data Representation A Case Study
111
52 Formal Specification
113
53 A Simple Implementation
114
54 Program Organization
116
55 Verification of a Data Representation
119
56 A Caching Implementation
122
57 Additional Reading
124
Data Representation Additional Examples
125
62 Sparse Arrays
131
63 Sequences
136
64 BitString Representation of Sets
138
65 Reachability in a Directed Graph
143
66 Sorting a Partially Ordered Set
146
67 Additional Reading
152
82 Software Realization
172
83 Nondeterminism
176
84 StateTransition Diagrams with e Transitions
183
85 Reactive Systems
184
86 Additional Reading
189
Regular Languages
191
92 From State Diagrams to Regular Expressions
196
93 Additional Operations on Regular Languages
199
94 Nonregular Languages
200
95 Other Formalisms
204
96 Additional Reading
205
ContextFree Languages
207
102 Derivations
210
103 Parse Trees
212
105 PushDown Automata
216
106 NonContextFree Languages
220
107 Other Formalisms
223
108 Additional Reading
224
Parsing
227
112 Deterministic PushDown Automata
228
114 Additional Reading
241
Unimplementable Specifications
243
Introduction to Part D
245
A Taste of Computability Theory
247
122 The ChurchTuring Thesis
249
123 Unsolvability by Reduction
250
124 Additional Reading
252
Appendices
255
Programming Language Reference
257
A2 Basic Types and Constants
259
A3 Strings
261
A5 Enumerated and Structure Types Defined Type Names
262
A7 Some Library Functions
264
A8 Statements
266
A9 Function Definitions
269
A10 More Library Functions
270
A11 Classes
273
A14 Additional Reading
278
Hints for Selected Exercises
279
Index
285
Autortiesības

Citi izdevumi - Skatīt visu

Bieži izmantoti vārdi un frāzes

Populāri fragmenti

8. lappuse - S. Gerhart, D. Craigen, and T. Ralston, "Experience with Formal Methods in Critical Systems,
8. lappuse - JP Bowen and MG Hinchey. Seven more myths of formal methods.
8. lappuse - D. Craigen, S. Gerhart, and T. Ralston, "Formal Methods Reality Check: Industrial Usage," IEEE Transactions on Software Engineering, vol.

Bibliogrāfiskā informācija