√лавна€    Ex Libris     ниги    ∆урналы    —татьи    —ерии     аталог    Wanted    «агрузка    ’удЋит    —правка    ѕоиск по индексам    ѕоиск    ‘орум   
blank
јвторизаци€

       
blank
ѕоиск по указател€м

blank
blank
blank
 расота
blank
Jacky J. Ч The Way of Z: Practical Programming with Formal Methods
Jacky J. Ч The Way of Z: Practical Programming with Formal Methods

„итать книгу
бесплатно

—качать книгу с нашего сайта нельз€

ќбсудите книгу на научном форуме



Ќашли опечатку?
¬ыделите ее мышкой и нажмите Ctrl+Enter


Ќазвание: 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.


язык: en

–убрика: Computer science/

—татус предметного указател€: √отов указатель с номерами страниц

ed2k: ed2k stats

√од издани€: 1997

 оличество страниц: 370

ƒобавлена в каталог: 18.08.2014

ќперации: ѕоложить на полку | —копировать ссылку дл€ форума | —копировать ID
blank
ѕредметный указатель
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
1 2 3 4
blank
–еклама
blank
blank
HR
@Mail.ru
       © Ёлектронна€ библиотека попечительского совета мехмата ћ√”, 2004-2017
Ёлектронна€ библиотека мехмата ћ√” | Valid HTML 4.01! | Valid CSS! ќ проекте