Àâòîðèçàöèÿ
Ïîèñê ïî óêàçàòåëÿì
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
Ïðåäìåòíûé óêàçàòåëü
Premises 190 Prescription, radiation therapy: 40 212 214 296 Prescriptive predicate 271 Prime number 66 115—116 161 Primed variable 53 124 303 Procedure 31 280—281 Process 70 234—240 Process algebra 326 Production rule 191 Program derivation 254—296 Program unit 286 290 Program, main 56 286—287 Programming language constructs 33—38 254—296 319—321 Programming language constructs, array 93 251 266 268 270 272 274 275 279 283 292—294 319—320 Programming language constructs, assignment 76 257—258 263—264 274—276 319—320 Programming language constructs, attribute 231 Programming language constructs, class 31 231—232 285 Programming language constructs, comments 35 64 255 261 Programming language constructs, conditional expression 259 262—263 277 320 321 Programming language constructs, control structure 56 258—259 Programming language constructs, data file 266—267 Programming language constructs, data structure 32 78 265—268 290—292 Programming language constructs, data types 31 35—36 266 Programming language constructs, declaration 35 266 Programming language constructs, enumeration 266 269 270 283 290—295 Programming language constructs, expression 257 271—272 Programming language constructs, for loop 33—36 255 256 277 279 283 294 296 320 321 Programming language constructs, function 31 33—38 280—281 286 Programming language constructs, global variables 257 268 271 280—281 Programming language constructs, header file 286 290 Programming language constructs, if statement 258—259 276 319 320 Programming language constructs, include file 286 290 Programming language constructs, iterator 279 Programming language constructs, library 32 Programming language constructs, local variables 284 285 Programming language constructs, loop 256 259—262 277 279 320 321 Programming language constructs, macro 32 50 123 132 Programming language constructs, main program 56 286—287 Programming language constructs, member 268 Programming language constructs, message 233 Programming language constructs, method 31 231 Programming language constructs, module 31 285—286 Programming language constructs, operator 271—272 Programming language constructs, pointer 88 282—283 321 Programming language constructs, procedure 31 280—281 Programming language constructs, program file 286 290 Programming language constructs, program unit 286 290 Programming language constructs, record 79 138 142 267—270 282—283 Programming language constructs, structure 79 138 142 267—270 282—283 Programming language constructs, type definition 269 289 290 292 Programming language constructs, while loop 256 321 Programming languages, Ada 256 327 Programming languages, C 33—38 254—297 319—321 327 Programming languages, C++ 231 Programming languages, Haskell 298 Programming languages, LISP 298 Programming languages, Miranda 298 Programming languages, ML 298 Programming languages, Modula-3 327 Programming languages, Pascal 7 9 256 297 298 Programming languages, Smalltalk 231 Project management 5 21—28 Projection operator 81 120 233 Projection operator, first 81 301 310 Projection operator, second 81 301 310 Projection, schema operator 304 Promotion 225—226 proof 11 149—162 249—252 254—264 294—298 327 Proof as a social process 159 Proof, correctness of code 11 254—264 294—298 Proof, equational 161—162 Proof, formal 149—150 Proof, informal 159 Proof, machine-checked 159—160 162 327 Proof, natural deduction 162 Proof, refinement 249—252 Proof, sequent calculus 162 Proper subset 300 309 PROSE see "Informal requirements" Protection system 211—217 Prototype, executable 7 32 327 Prototype, nonexecutable 149 Pythagorean triple 322 Quadratic formula 252 Quantification, schema operator 304 Quantifier 106—108 116—119 279 317 320 Quantifier, definite description 304 Quantifier, existential 108 142 154 157—158 Quantifier, restricted 116—117 Quantifier, unique existential 304 Quantifier, universal 106 133—134 Query 83—84 196—198 Quotient 128—129 277 Race condition 235 Radiation therapy, accidents 15—16 27 214 Radiation therapy, machines 39—48 60 199—218 Radiation therapy, prescription 40 212 214 296 Radiation therapy, treatment planning 180 182 241 242 Railway controls 12 Range anti-restriction 84 238 301 311 Range of a relation 82—83 301 310 Range of numbers 64 95 302 313 Range restriction 84—86 301 311 Rank 174—179 Rational number 65 Reachability 327 Real number 65 252 Real Time 239 Reasoning, equational 161—162 Reasoning, formal 149—160 Reasoning, informal 159 Reasoning, intuitive 159 Reasoning, monotonic 192 195 Reasoning, operational 254 Record 267—268 Recursive data structure 148 Recursive definition 170 Reference Manual 31 59 161 162 297—298 304 308 Referential transparency 67 refinement 10 211 214 216 247—253 297—298 Refinement, calculus 255 262—264 270—279 Refinement, law 262—264 270 319—320 Refinement, proof 249—252 Reflexive transitive closure 304 Reification see "Refinement" Relation 80—88 98—99 301 309—312 Relation syntax, infix 74 94 98—99 299 305 318 Relation syntax, mixfix 83 Relation syntax, postfix 193 299 Relation syntax, prefix 304 Relation, asymmetric 184 Relation, binary 81—88 98—99 301 310—312 Relation, identity 304 Relation, inverse 85 240 Relation, many-to-many 82 89 Relation, many-to-one 82 89 Relation, one-to-many 89 Relation, one-to-one 82 89 92 176 Relation, schema as 144—145 Relation, symmetric 183 Relation, unary 98—99 109 140 Relational database 80 Relational operators 80—88 301 309—312 Relational operators, backward composition 301 312 Relational operators, composition 86—87 301 312 Relational operators, domain 82—83 301 311 Relational operators, domain anti-restriction 84 225 237 295 301 311 Relational operators, domain restriction 83—86 301 311 Relational operators, image 83 90 192 228 301 311 Relational operators, inverse 85 240 301 311 Relational operators, iteration 304 Relational operators, overriding 84—85 208 216 235 295—296 301 311 Relational operators, range 82—86 301 310 Relational operators, range anti-restriction 84 225 237 295 301 311 Relational operators, range restriction 83—86 301 311 Relational operators, reflexive transitive closure 304 Relational operators, transitive closure 193 242 301 311 Relations as predicates 98—100 Remainder 128—129 277 see Renaming, schema component 304 Requirements 18—19 23—26 27 Resource 147 234—236 Resource exhaustion (or limitation) 158 Restricted quantifier 116—117 Restriction, domain 82—83 301 311 Restriction, range 82—83 301 311 Reuse 10 173 Reverse, sequence operator 304 review 4 296 right triangle 114 322 Risks Digest 27 Rule 190—191 Rule interpreter 190 Rule-based programming 189—198 Safety assertion 219 243 Safety interlock see "Interlock" Safety protection system 211—217 Safety requirement 27 104 214 217 Safety-critical systems 12 15—16 27 39—48 211—230 242 326 Safety-critical systems, programming languages for 297 Satisfy, of predicates 97 Scheduler 235 Schema 32 49—58 122—145 Schema as declaration 133—134 Schema as expression 145 Schema as predicate 133—134 Schema as relation 144—145 Schema as set 141 Schema calculus 32 55—56 122—137 303 Schema component 52 142 303 see Schema expansion 123 Schema expression 56 127 Schema format, horizontal 127 Schema format, vertical 126 Schema inclusion 123 Schema operators, component renaming 304 Schema operators, component selection 142 303 Schema operators, composition 134 303 Schema operators, conjunction 128—129 303 Schema operators, disjunction 130 303 Schema operators, equivalence 304 Schema operators, hiding 304 Schema operators, implication 304 Schema operators, negation 135—137 303 Schema operators, piping 134—135 303 Schema operators, projection 304 Schema operators, quantification 304 Schema reference 56 128 133 145 Schema text 132 299 Schema type 138—145 Schema, history of 161 Schema, initialization 51—52 123 154 Schema, operation 52—53 124—126 280—289 Schema, state 50—52 122—123 266 268—270 Schema, top level 56—57 286—287 Schemas, compatible 128 Scope 106 118 133 143—144 307 Search control 195 secure communications 20 28 Security 27 Segment, line 114 183 Segment, sequence operator 183 302 315 Selection, schema component 142 303 Selector 142 Semantics 4 45 138 142 161 Semaphore 236 SEQUENCE 93—94 248—251 302 315 318 Sequence display 93 302 Sequence operators, compaction 304 Sequence operators, concatenation 51 93 146—147 158 302 315 318 Sequence operators, distributed concatenation 304 Sequence operators, extraction 304 Sequence operators, filtering 304 Sequence operators, first see "Head" Sequence operators, front 302 315 Sequence operators, head 54 93 302 315 Sequence operators, in 183 302 315 Sequence operators, last 302 315 Sequence operators, prefix 304 Sequence operators, reverse 304 Sequence operators, segment see "In" Sequence operators, squash 304 Sequence operators, suffix 304 Sequence operators, tail 54 302 315 Sequence, empty 52 54—55 123 302 Sequent calculus 162 Servomotor 222—224 Set comprehension 112—114 300 318 Set display 63 300 Set expression 56 127 Set operators, cardinality 73 Set operators, difference 73 116 140 300 309 Set operators, generalized intersection 304 Set operators, generalized union 304 Set operators, intersection 73 300 309 Set operators, membership 63 Set operators, non-membership 136 300 309 Set operators, proper subset 300 309 Set operators, size 51 73 94 158 300 313 318 Set operators, subset 73 300 309 Set operators, union 73 300 309 Set type 69—71 138 Set, empty 63 300 308 Set, schema as 141 Shared language, Larch 327 short circuit evaluation 258—259 263 Shutdown software 326 Side effect 257 271 280 Sieve of Eratosthenes 116 Signature 68—69 128 140 Singleton sequence 158 159 318 Situation 97 138 Size, set operator 51 73 94 158 300 313 318 skip 274 319 Social process 159 software component 10 Source language transformation 256 273 321 Source set 82 Specialization 96—97 173 Specification languages, B 326 Specification languages, CCS 326 Specification languages, CSP 326 Specification languages, EVES 162 327 Specification languages, Larch 327 Specification languages, MooZ 233 326 Specification languages, Object Z 233 326 Specification languages, OOZE 233 326 Specification languages, Petri nets 326 Specification languages, Pi calculus 326 Specification languages, statechart 206—208 242 326 Specification languages, TLA 326 Specification languages, Unity 326 Specification languages, VDM 241 242 326 Specification languages, Z 31—32 59—60 161—162 Specification languages, Z++ 233 326 Square 114—115 Square root see "Integer square root" Squash 304 State 50—51 57 138 State schema 50—52 122—123 266 268—270
Ðåêëàìà
|
|
Î ïðîåêòå