Specifying Software: A Hands-On IntroductionCambridge 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 |
259 | |
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 |
285 | |
Citi izdevumi - Skatīt visu
Bieži izmantoti vārdi un frāzes
accepting Additional Reading algorithm allow application array segment assignment assume Attr automata automaton axiom scheme bool C. A. R. Hoare Chapter char code fragment components concatenation consider const int construct context-free grammar context-free languages correctness statement data representations database defined definition described discussed efficient elements empty string example execution EXERCISE false finite ForAll formal languages func function gettoken identifier implementation implies inference rule initially input token integer INVAR labeled loop body loop condition loop invariant nDist nodes nonterminal notation number of entries occurrences operations output palindrome parse tree poset post-condition power x,n pre-condition Prentice Hall International problem Professor Higgins programming language pumping lemma push-down push-down automaton recursive regular expression regular language representation invariant Section sequence sorted sparse set specification stack state-transition diagram student numbers techniques terminal terminal symbols tion transitions traversal true typedef variable verify vocab void include
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.