Àâòîðèçàöèÿ
Ïîèñê ïî óêàçàòåëÿì
Jacky J. — The Way of Z: Practical Programming with Formal Methods
Îáñóäèòå êíèãó íà íàó÷íîì ôîðóìå Íàøëè îïå÷àòêó?
Íàçâàíèå: The Way of Z: Practical Programming with Formal MethodsÀâòîð: Jacky J. Àííîòàöèÿ: This self-contained tutorial on Z presents realistic case studies emphasizing safety-critical systems, with examples drawn from embedded controls, real-time and concurrent programming, computer graphics, games, text processing, databases, artificial intelligence, and object-oriented programming. It motivates the use of formal methods and discusses practical issues concerning how to apply them in real projects. It also teaches how to apply formal program derivation and verification to implement Z specifications in real programming languages with examples in C. The book includes exercises with solutions, reference materials, and a guide to further reading.
ßçûê: Ðóáðèêà: Computer science /Ñòàòóñ ïðåäìåòíîãî óêàçàòåëÿ: Ãîòîâ óêàçàòåëü ñ íîìåðàìè ñòðàíèö ed2k: ed2k stats Ãîä èçäàíèÿ: 1997Êîëè÷åñòâî ñòðàíèö: 370Äîáàâëåíà â êàòàëîã: 18.08.2014Îïåðàöèè: Ïîëîæèòü íà ïîëêó |
Ñêîïèðîâàòü ññûëêó äëÿ ôîðóìà | Ñêîïèðîâàòü ID
Ïðåäìåòíûé óêàçàòåëü
Abbreviation definition 49 68 113 118 266 299 Abbreviation definition, generic 147 Absolute value 119 215 220 abstract data type (ADT) 31 208 Abstract operation 248 Abstract state 248 Abstraction schema 251 Accelerator 218 see "Radiation Acceptance test 28 37 Accuracy 35 185 Ada 256 327 Addition 37 72 94 301 313 ADT (abstract data type) 31 208 After, state 124 256 303 After, variable 124 274 303 Aircraft collision avoidance 326 Algebra, process 326 American National Standards Institute (ANSI) 31 Analysis 4 Analysis of cases 57 101—102 130 276 320 Analysis, exhaustive 327 Analysis, reachability 327 Analytic style, Z notation 32 AND see "Conjunction" AND/OR table 326 Annotated bibliography, Z notation 59 ANSI (American National Standards Institute) 31 Antecedent in implication 104 Antecedent in proof technique 250 317 325 Anti-restriction, domain 84 237 255 295 301 311 Anti-restriction, range 84 238 301 311 Applications of formal methods 12 28 326 Arc, of a graph 87 Arithmetic expression 72 Arithmetic operator 37 72 94 150—153 271—272 301—302 313 318 Arithmetic operator, absolute value 119 215 220 Arithmetic operator, addition 37 72 94 301 313 Arithmetic operator, division 72 Arithmetic operator, greater than 151 302 313 Arithmetic operator, greater than or equal 302 313 Arithmetic operator, less than 151 301 313 Arithmetic operator, less than or equal 301 313 Arithmetic operator, maximum 302 313 Arithmetic operator, minimum 172 302 313 Arithmetic operator, modulus 72 107 153 271—273 280 301 313 318 Arithmetic operator, multiplication 37 72 116 153 271 301 313 318 Arithmetic operator, range 64 95 302 313 Arithmetic operator, remainder 128—129 277 Arithmetic operator, subtraction 72 271 277 301 313 Array 93 251 266 268 270 272 274 275 279 283 292—294 319—320 artificial intelligence 189 242 Ashton-Tate 19 Assembler 59 Assertion in program verification 256 261 Assertion, liveness 243 Assertion, safety 219 assignment statement 76 257—258 263—264 274—276 319—320 Associate 306—307 Associativity 307 316—317 Assume antecedent 250 317 325 Asymmetric relation 184 Asymmetry 81 86 89 104 ATM (automated teller machine) 15 27 Atomic operation 236 Attributes of an object 231 automated teller machine (ATM) 15 27 Axiomatic definition 35 38 50 56 66—68 266 302 Axiomatic description see "Axiomatic definition" Axiomatic program derivation 255—264 278 Axiomatic semantics 256 B method 326 Backward chaining 191 196—198 Backward relational composition 301 312 Bag 262 304 base class 232 Basic type 70—71 266 299 Before, state 124 256 303 Before, variable 124 274 303 Bibliography, annotated, Z notation 59 Bijection 176 301 314 Binary relation 81—88 98—99 301 310—312 Binary semaphore 236 Binding 138—145 224 281—283 Binding formation operator 143—144 281—282 303 BOOLEAN data type 108—110 272 275 319 320 Boolean function 109 280 286 Bottom-up declaration order 188 Bottom-up design 10 Bound variable 106—108 112 118 172 226 294 Bound, in loop verification 260—263 325 Bounding function see "Bound" Branch see "If statement" British Standards Institute (BSI) 31 BSI (British Standards Institute) 31 Bubbles and arrows 44—45 206—207 327 C programming language see also "Programming language constructs" C programming language and safety-critical systems 297 C programming language, axiomatic semantics 256—262 319 C programming language, programming from Z specifications 254—296 C programming language, refinement laws 262—264 270—279 319—320 C programming language, source language transformations 256 273 321 C programming language, square root example 33—38 255 280 C++ 231 calendar 119—121 Cardinality 73 Carrier set 64 Cartesian product type 79 300 Case analysis 57 101—102 130 170 276 320 Case studies, Z notation 59 CASE tools 10 CCS 326 Characteristic tuple 113 318 323 Chess 174—179 323—324 CICS transaction processing system 59 class 31 199 231—232 285 Cleanroom method 297 clock 239—240 Closure, transitive 193 242 301 311 Code see "C programming language" "Programming Collision avoidance, aircraft 326 Comments 35 64 255 261 Compaction, sequence 304 Compatible schemas 128 Compiler 7—8 17 18 33 37—38 59 254 Completeness, requirements 24 27 207 242 Complex number 65 252 Component, schema 50 142 303 Component, software 10 Composition of relations 86—87 301 312 Composition of schemas 134 303 Comprehension, set 112—116 144 273 300 318 Computational geometry 180—188 241 Computer graphics 114 180—188 Concatenation 51 93 146—147 158 302 315 318 Concatenation, distributed 304 Conclusion (of a rule) 190 Concrete operation 249 Concrete state 249 Concurrency 234—240 243 326—327 Condition 227—228 Conditional expression, C programming language 259 262—263 277 320 321 Conditional expression, Z notation 119 276—277 317 Conjunct 100 Conjunction, implementation 277 Conjunction, logical connective 100—102 117 300 316 Conjunction, schema operator 128—129 Consensus 159 Consequent in implication 104 Consequent in proof technique 250 Consistent predicates 97—98 Consistent rules 193—194 Constant 68 266 Constraint 66 74 Constructive definition 37 116 252 274 contour 180—183 187 Control console 39—48 199—210 Control law 219 Control Panel 232 Control parameter 221—222 232—233 Control strategy 191 195 Control structure 56 258—259 Controls, cyclotron 218—230 Controls, nuclear reactor 326 Controls, radiation therapy machine 15—16 27 39—48 199—230 Controls, railway 12 Convention, notational 31 94—95 116 124—126 225 303 Correctness, proof of 11 254—264 Counting numbers 64 Coupling 209—210 Cross product 79 300 Cryptography 20 CSP 326 Cyclotron 218—230 see data file 266 267 Data flow, analysis 274 285 Data flow, diagram 4 44 87 Data structure 32 78—95 265—268 290—292 Data type 31 35—36 64—66 138—149 266 Data-driven 196 Database 79—87 Database, query 83—84 Database, update 84—85 Date example 78—79 119—121 138—145 Deadline 158 239—240 Decision table 106 declaration 63 65—66 106 113 132 266 299 Declaration before use 67 188 Declaration, schema as 133—134 Decoration 124 303 Definite description quantifier 304 Definition symbol 49—50 68 147 299 Delta 53 124—125 144 DeMorgan's law 136 153 316 Denotational semantics 142 161 denote 65 142 derived class 232 description 28 Descriptive predicate 271 Descriptive style, Z notation 32 Design 10—11 27—28 209—210 211 218 230 252—253 265—266 285—287 290—296 Design, participatory 27 Deterministic 253 Diagonal 174—179 Diagram 7—9 25 Diagram, data flow 4 44 87 Diagram, state transition 45—46 87 Dialog box 199 203—206 Dice 66—69 71 73 97 Difference, set 73 116 140 300 309 Discrete mathematics 11 122 161 326 Disjoint 304 Disjunct 101 Disjunction, implementation 276—277 286 Disjunction, logical connective 101—102 300 316 317 320 Disjunction, schema calculus operator 130 Display, sequence 93 302 Display, set 63 300 Distributive law 131 153 316 Division, arithmetic operator 72 74 110 128 152 153 271 301 313 318 Division, example C code 271 277 Division, example schema 128—130 133—134 277 Document control system 165—168 Domain anti-restriction 84 225 237 295 301 311 Domain of relation 82—83 301 310 Domain restriction 83—86 301 311 Dose calculation 7—8 180 Dummy variable 36 Efficiency 58 191 196 265 Eight queens problem 174—179 241 Electronic instruments 12 59 Element, set 63 else see "Conditional expression" Embedded controller 12 59 Empty sequence 52 54—55 123 302 Empty set 63 300 308 End of file 54—56 130—132 English see "Natural language" Entry condition 53 Enumerated type, C programming language 266 269 270 283 290—295 Enumerated type, Z notation 70 148 266 Equality 74—76 96 150 257 300 317 equation see "Equality" Equivalence class 57 Equivalence, logical connective 103 152 300 317 Equivalence, schema operator 304 Eratosthenes, sieve of 116 Erroneous expression 74 Euclid's Algorithm 20 Even number 66 68—69 Event 199—200 237—240 event-driven programming 199—200 237 Eves 162 327 Executable specification 327 Existential quantifier 108 117—118 154 157—158 279 300 317 Expansion, schema 123 125—126 130—132 136 Expert system 189 Expression, C programming language 257 271—272 Expression, schema 56 Expression, schema as 145 Expression, Z notation 63 71—74 Expression, Z notation, arithmetic 72 Expression, Z notation, conditional 119 Expression, Z notation, erroneous 74 Expression, Z notation, lambda 114 Expression, Z notation, schema 56 127 Expression, Z notation, set 73 Expression, Z notation, undefined 74 110—111 Extraction, sequence 304 Fact 190 Fair 235 FALSE 96 300 316 File in Chess 174—179 File, C code 286 290 File, data 267 Fill, text 171—173 Filtering, sequence 304 Finite state machine 45—48 206—208 First, of sequence 54 93 302 315 First, projection operator 81 300 310 Floating point arithmetic 185 Floating point arithmetic, IEEE standards 59 Floating point microcode 59 Floating point number 59 212 221 For loop 33—36 255 256 279 283 294 296 320 321 Formal generic parameter 147 Formal methods 3—28 326—327 Formal methods, applications 12 28 326 Formal methods, home page 327 Formal methods, mandated 328 Formal notations see "Specification languages" Formal reasoning 149—160 254 Formal specification 7—10 31 33 38 Formula 3 Forward chaining 191 196—198 Forward relational composition 86—87 301 312 Free type 70 148 266 299 Free variable 106—107 172 271 Front, sequence 302 315 Function application 90—91 273—274 301 319 Function, C programming language 31 33—38 280—281 286
Ðåêëàìà
|
|
Î ïðîåêòå