Àâòîðèçàöèÿ
Ïîèñê ïî óêàçàòåëÿì
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
Ïðåäìåòíûé óêàçàòåëü
Function, Z notation 35 51 88—92 268 280 301 314 Function, Z notation, bijective 176 301 314 Function, Z notation, hash 251—252 324—325 Function, Z notation, higher-order 212 Function, Z notation, injective 92 176 301 314 325 Function, Z notation, partial 91—92 301 314 Function, Z notation, total 92 224 301 314 Functional programming 31 298 genealogy 87—90 Generalized intersection 304 Generalized union 304 Generic definition 146—147 302 Generic operators 73 Generic schema 147 Geometry, computational 180—188 241 Given set see "Basic type" Global variable, C programming language 257 268 271 280—281 Global variable, Z notation 50 67 Glue 209 Goal-driven 196 Graph 87 Graphical user interface (GUI) 199—210 Graphics, computer 180—188 241 Greater than 151 302 313 Greater than or equal 302 313 Greek letters, delta 53 124—125 144 Greek letters, lambda 114 Greek letters, mu 304 Greek letters, phi 225 Greek letters, theta 143—144 Greek letters, xi 125 guard 260—261 see Guarded command 276 320 GUI (Graphical User Interface) 199—210 Handler 238 Hash function 251—252 324—325 Haskell 298 Head, sequence operator 54 93 302 314 header file 286 290 Hiding, schema operator 304 Higher-order function 212 Hoare triple 256—257 264 Home page, formal methods 327 Home page, Z notation 60 Horizontal schema format 126—127 IBM 59 Identifiers 71 Identity relation 304 Idiom, Z notation 225—226 233 IEEE floating point arithmetic standard 59 if see "Implication" If and only if see "Equivalence" If statement 258—259 276 319 320 IF THEN ELSE see "Conditional expression" Image, relational 83 90 192 228 301 311 Imperative programming language 31 298 Implication and refinement 247—248 Implication, logical connective 103—105 117 250 300 Implication, schema operator 304 In, sequence operator 183 302 315 Include, C programming language 286 290 Include, Z notation 123 Inclusion, file 286 290 Inclusion, schema 123 Incommensurable number 35 Inconsistent, predicates 97—98 154 Inconsistent, rules 193—194 Induction 162 Inequality 75 151 300 323 Inference Engine 190 Infix syntax 74 94 98—99 299 305 318 Informal requirements 25—26 39—44 115—116 165 174 296 inheritance 31 231—232 286 Initial state 51—52 123 154 322 Initialization, schema 51—52 123 154 Initialization, theorem 154 Injective function 92—93 176 301 314 325 Injective sequence 183 302 315 324 INMOS 59 Input variable 53 124 196 303 Inspection 4 6 26 265 270 296 Instance variable 31 INTEGER 35 64—65 162 301 Integer square root 33—48 118 255 259—262 280 Interface languages, Larch 327 Interleaving model of concurrency 235 243 Interlock 40—47 211—217 220—221 229 International Organization for Standardization (ISO) 31 Interrupt 238 Interrupt-driven 237 Intersection of line segments 180—188 Intersection of sets 73 300 309 Intersection of sets, generalized 304 Intuition 3 11 158—159 255 258 Invariant loop 260—262 Invariant state 51 54 154 156 269 Inverse relation 85 240 301 311 Irrational number 35 ISO (International Organization for Standardization) 31 Iteration, loop 259—262 Iteration, relational 304 Iterator 279 Kernel, operating system 59 162 Key, data base 268 Knight's tour problem 179 324 Knowledge base 190 Lambda expression 114 LARCH 327 Last, sequence operator 302 315 Law 76—77 152—154 laws 153 316—321 Laws, de Morgan 136 153 316 Laws, Excluded Middle 153 316 Laws, Leibniz 154 317 323 Laws, one-point rule 157 317 Laws, refinement 262—264 270—280 319—320 layout 71 126—127 leap year 120 140 143 Leibniz' law 154 317 323 Less than 151 301 313 Less than or equal 301 313 Library, of types and functions 32 Line segment 180—188 Lines of Code 12 lines of text 91 171 Linked data structure 87—88 148 162 Lisp 58 298 literate programming 13 liveness 243 Local Definition 118 278 289 300 317 320 Local variable, C programming language 284 285 Local variable, Z notation 51 106 Logic 96—111 300 306 316—317 Logical connectives 100—105 300 316 Logical connectives, conjunction 100—102 117 Logical connectives, disjunction 101—102 320 Logical connectives, equivalence 103 152 Logical connectives, implication 103—105 117 250 Logical connectives, negation 102 Logical constant 96 300 Loop 256 259—262 277 279 320 321 Loop invariant 260—262 Loose definition 67 Lotus 17 Macro 32 50 123 138 Main program 56 286—287 make utility 59 242 management, project 5 21—28 Many-to-many relation 82 89 many-to-one relation 82 89 Maplet 81 224 301 310 Mathematical tool-kit 32 176 308—315 Maximal set 65 Maximum 302 313 Member of a C structure 268 Member of a set 63 Membership predicate 96 98—99 109 Menu 199 Message 233 Method, object-oriented programming 31 231 Methodology see "Methods software development" Methods, software development, B 326 Methods, software development, Cleanroom 297 Methods, software development, VDM (Vienna Development Method) 326 Methods, software development, Z 31 38 56—58 172—173 209—210 211 218 230 252—253 265—266 285—287 290—296 Microcode 12 Microprocessor 12 59 Microsoft 16 17 Military software 28 Minimization 172 Minimum 172 302 313 Miranda 298 Mixfix syntax 83 ML 298 Mnemonic names 287 MODE 200—227 227—229 291—295 Model 6—10 28 231 Model checking 160 162 327 Model-based notation 31 326 Modula-3 327 Module 31 199 285—286 Modulus 72 107 115 153 271—273 280 301 313 318 Monotonic reasoning 192 195 MooZ 233 326 Mouse 199 200 Move, Chess 179 323—324 mu 304 Multiplication 37 72 116 153 271 301 313 318 Multiset 304 mutable data 268 Mutex 236—237 Mutual exclusion 236—237 Natural deduction 162 Natural language 105—106 161 see Natural number 35 64 113 301 313 Negation, logical connective 102 300 306 316—317 Negation, schema operator 135—137 303 New variable 278 320 Node 87 Nonconstructive definition 37—38 252 nondeterministic 170 172—173 235 253 Nonexecutable 31—32 37—38 Nonmembership, set 136 300 309 Normalize 68—69 128 135—136 139—141 NOT see "Negation" Nuclear reactor shutdown software 326 Number, complex 65 252 Number, counting 64 Number, even 66 68—69 Number, floating point 59 185 212 221 Number, incommensurable 35 Number, integer 35 64—65 301 313 Number, irrational 35 Number, natural 35 64 113 301 313 Number, odd 66 68—69 112 273 280 Number, positive 64 Number, prime 66 115—116 161 Number, rational 65 Number, real 65 252 Number, strictly positive 64 301 313 Numerical computation see also "Floating point" "Accuracy" Object 31 138 231—233 Object Z 233 326 Object-Oriented Programming 5 31 231—233 285—286 odd number 66 68—69 112 273 280 One point rule 157 317 One-to-many relation 89 One-to-one relation 82 89 92 176 OOZE 233 326 Operating System 17 18 70 234 254 Operating system, kernel 59 162 Operation schema 52—53 124—126 280—289 Operational reasoning 254 Operator, arithmetic see "Arithmetic operators" Operator, C programming language see "Programming language constructs" Operator, generic 73 Operator, projection see "Projection operators" Operator, relational see "Relational operators" Operator, schema see "Schema operators" Operator, sequence see "Sequence operators" Operator, set see "Set operators" OR see "Disjunction" Oracle 9—10 149 198 Oscilloscope 59 Outfix syntax 119 Output variable 195—196 303 Overflow 158 overriding 84—85 208 216 235 295—296 301 311 Oxford University 31 59 Package 285 pair 81 300 310 Paper and pencil 32 Paragraph, abbreviation definition 49 68 113 118 266 299 Paragraph, axiomatic definition 35 38 50 56 66—68 302 Paragraph, basic type definition 70—71 299 Paragraph, free type definition 70 148 266 299 Paragraph, generic definition 146—147 302 Paragraph, predicate 75 Paragraph, schema 49—58 122—145 Paragraph, text 171—173 Paragraph, Z notation 32 49 66 266 PARAMETER 67 221—222 232—233 Partial function 91—92 301 314 Partial operation 54—55 127 283—284 Participatory design 27 Partition of design 10 211 Partition, operator 304 Pascal 7 9 256 297 298 Pattern matching 107 113—114 120 147 170 PC (personal computer) 60 Personal Computer 60 Petri nets 326 Phi 225 Pi calculus 326 Piping 134—135 POINTER 88 282—283 321 Polygon 180—188 Positive integer 64 Postcondition 256—261 271 Postfix syntax 193 299 Power set 69 192 300 PRECISION 34—35 Precondition 53 135 149 155 256—261 271 276 283 285 286 see Precondition, calculation 155—158 Precondition, implicit 53—55 Precondition, weakest 257 Predicate 36 38 50—51 63 66—67 74—77 96—111 see "Precondition" "Postcondition" Predicate calculus 108 Predicate, descriptive 271 Predicate, equality 74—75 96 Predicate, inconsistent 97—98 Predicate, membership 75 96 Predicate, prescriptive 271 Predicate, quantified 106—108 Predicate, relational 98—99 Predicate, schema as 133—134 Predicate, stronger 97 Predicate, weaker 101 Prefix 304 Prefix syntax 74 95 98—99 194 299 318
Ðåêëàìà
|
|
Î ïðîåêòå