3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 85
Текст из файла (страница 85)
Morris and C. B. Jones, An early programproof by Alan Turing, Annals of the History of Computing 6 pages 139–143, 1984. Cited on page 12.J. C. P. Woodcock and A. L. C. Cavalcanti[2002] The semantics of Circus, in: ZB2002: Formal Specification and Development in Z and B, D. Bert, J. P. Bowen, M.
C. Henson, and K. Robinson,eds., vol. 2272 of Lecture Notes in Computer Science, Springer, pp. 184–203. Cited on page 406.D. Zöbel[1988] Normalform-Transformationen für CSP-Programme, Informatik: Forschung und Entwicklung, 3, pp. 64–76. Cited on page 405.J. Zwiers[1989] Compositionality, Concurrency and Partial Correctness – Proof Theoriesfor Networks of Processes and Their Relationship, Lecture Notes in Computer Science 321, Springer, New York. Cited on pages 125 and 406.Indexabstract interpretation, 16abstraction refinement, 16actionatomic, 269private, 384action systems, 370alias, 43aliasing, 240alphabet, 25alternative command, 351arity, 30array, 30arraysordered, 361assertion, 39holding in a state, 41pure, 220assignment, 57associativityright, 40assumption, 39, 132atomic region, 268, 270conditional, 309atomic statement, 271atomicity, 272, 294, 334grain of, 273virtual, 273, 281auxiliary rule, 97auxiliary variables, 256axiom, 38B-method, 371bijection, 24bijective, 24binding order, 31block statement, 152Boolean conditionof a joint transition, 390bound function, 71busy waiting, 327calculus, 38callee, 186cardinality, 22Cartesian product, 22chain, 25, 448stabilizing, 448check set, 420co-domain, 24communication, 376asynchronous, 374synchronous, 373communication channel, 375commutativity, 384of relations, 265, 297, 384completepartial order, 447proof system, 85completeness, 85, 89compositionality, 66, 255, 275computation, 59almost good, 295, 388diverging, 59extension of, 429fair, 411good, 295, 385restriction of, 429terminating, 59concatenation, 26conclusion, 38conditional statement, 57configuration, 58confluence, 250conjunction, 31491492connective, 31consistent, 219constantBoolean, 30denoting a value, 33integer, 30cooperation test, 405copy rule, 129, 159, 183correctness formula, 63critical reference, 273critical regionconditional, 346CSP, 374deadlock, 310, 377freedom, 310, 315freedom relative to p, 310, 394potential, 314deductive verification, 17definabilityof sets of states, 87design by contract, 17determinism, 60, 252diamond property, 249dimensionof an array, 30disjointprocesses, 376programs, 247sets, 22disjunction, 31distributed programs, 373, 376distributed systems, 373divergence, 61domainof a function, 24semantic, 32dynamic control, 455dynamic logic, 17embedding, 429empty set, 21equivalence, 31input/output or i/o, 252of assertions, 42permutation, 296Z-, 429Event-B, 371expressibility, 88expression, 31Boolean, 31global, 198integer, 31local, 187Indexnavigation, 198pure, 218, 220typed, 31failure, 96failure admitting program, 95failure statement, 95fair scheduling, 422fair total correctness, 430sound for, 438fairness, 410finitary, 455strong, 410weak, 409, 453finite chain property, 448fixed point, 24least, 448fixed point computationasynchronous, 449synchronous, 449formation rule, 80function, 23bijective, 24injective, 24one-to-one, 24surjective, 24function symbol, 30global invariant, 105, 390relative to p, 390grammar, 29guard, 95, 351generalized, 375guarded command, 351handshake, 373Hoare’s logic, 124i/o command, 375iff, 26implication, 31incompleteness theorem, 86induction, 27structural, 27infix notation, 23injective, 24input/outputcommand, 375equivalence, 252integer, 21interference, 267freedom, 276, 286, 312points of, 294, 334interleaving, 248, 270Index493intersection, 21interval, 21closed, 21half-open, 21open, 21invariant, 66free, 41one-to-one, 24ordercomponentwise, 414lexicographic, 414overspecification, 349Java Modeling Language, 17joint transition, 390pair, 22parallel assignment, 92parallel compositiondisjoint, 247parallel programscomponents of, 247disjoint, 247with shared variables, 270with synchronization, 309parameteractual, 152formal, 152parameter mechanismcall-by-value, 155partial correctness, 64complete for, 85of disjoint parallel programs, 253of distributed programs, 390of nondeterministic programs, 357of object-oriented programs, 201of object-oriented programs withparameters, 208of parallel programs with synchronization, 311of recursive programs, 133of recursive programs with parameters,162, 166of while programs, 65sound for, 74partial order, 447complete, 447irreflexive, 414postcondition, 63precondition, 63weakest, 86weakest liberal, 86prefix, 25premise, 38priorities, 422procedurebody, 129, 152call, 129, 152declaration of, 129, 152identifier, 129non-recursive, 149procedure callrecursive, 129König’s Lemma, 272layer, 305lengthof a proof, 39of a sequence, 24liveness, 325loop, 57invariant, 66rule, 71transition, 411main loop, 375exit, 384main statement, 129, 152mapping, 23matchingof i/o commands, 376method, 188body, 188call, 188call with parameters, 207definition, 188, 206with parameters, 208minimum-sum section, 116model checking, 406monotonic, 62, 354, 448mutual exclusion problem, 324natural number, 21negation, 31nondeterminismunbounded, 412nondeterminism semanticsweakly fair, 453nondeterministic programsone-level, 410objectcreation of, 217identity, 193OCCAM, 374occurrence, 26bound, 41494process, 375producer/consumer problem, 319program analysis, 16program counter, 281, 363program transformation, 294, 298, 334,335, 363, 382, 413, 427programswhile, 57distributed, 376nondeterministic, 351object-oriented, 188parallel, 247, 270, 309recursive, 129, 152proof, 38proof outline, 80for fair total correctness, 433for nondeterministic programs, 358for partial correctness, 80for total correctness, 83standard, 80proof outlines, 274interference free, 277, 312, 314standard, 274proof rule, 38adaptation, 125auxiliary, 97proof system, 38quantifierexistential, 40universal, 40random assignment, 414recursion, 129reduction system, 249relation, 23antisymmetric, 23inverse, 23irreflexive, 23reflexive, 23symmetric, 23transitive, 23relation symbol, 30relational composition, 23rendezvous, 373repetitive command, 351restrictionof a computation, 429of a function, 24run, 410fair, 410monotonic, 425of a computation, 411of a program, 411Indexof components, 410safety property, 325scheduler, 420fair, 421round robin, 424states, 420universal, 421weakly fair, 454schedulingrelation, 420sectionof an array, 30, 116selection, 410of components, 410semantic domain, 33semantics, 32denotational, 58fair nondeterminism, 412of expressions, 35operational, 58partial correctness, 60, 249total correctness, 60, 249transformational, 413, 427semaphore, 331binary, 331sequence, 24sequential composition, 57sequentialization, 253, 254, 383set, 21set difference, 21set partition, 403shape analysis, 16skip statement, 57soundness, 74strong, 82state, 34consistent, 219error, 34local, 192, 193proper, 34satisfying an assertion, 41state space explosion, 16static scope, 153, 183string, 25structure, 33subassertion, 41subexpression, 32subprogram, 57normal, 271, 309subset, 21substitution, 42backward, 66simultaneous, 45Indexsubstring, 26suffix, 25surjective, 24swap property, 94syntactic identity, 25syntax-directed, 65Temporal Logic of Actions, 371theorem, 39total correctness, 64complete for, 85of disjoint parallel programs, 253of distributed systems, 391of nondeterministic programs, 357of object-oriented programs, 204of recursive programs, 136of while programs, 70, 71sound for, 74transition, 58relation, 58sequence, 59system, 59transitive, reflexive closure, 23transputer, 406tuple, 22components of, 22type, 29argument, 29basic, 29495higher, 29value, 29UNITY, 370updateof a state, 36, 218upper bound, 447least, 447variable, 30Boolean, 30can be modified, 57global, 153instance, 187integer, 30local, 153normal, 187subscripted, 32void reference, 187weak total correctnessof distributed systems, 391well-foundedon a subset, 414structure, 414zerononpositive, 4positive, 4Author IndexAbadi, M., 240, 477Abrial, J.-R., 13, 371, 477Alur, R., 455, 477America, P., 12, 150, 183, 477Andrews, G.
R., 345, 489Apt, K. R., 12, 15, 124, 125, 150, 182,305, 325, 370, 390, 403, 405, 455,477, 478, 487Araki, K., 482Archer, M., 488Ashcroft, E., 370, 478Attali, I., 479Back, R.-J., 13, 370, 455, 478, 482Backhouse, R. C., 13, 478Baeten, J. C. M., 484Baier, C., 16, 478Bakker, J. W. de, 52, 87, 122, 124, 125,150, 370, 478, 479, 489Ball, T., 16, 479Balser, M., 17, 346, 479Banerjee, A., 240, 479Barnett, M., 240, 479Basin, D., 406, 479Beckert, B., 17, 18, 241, 479Ben-Ari, M., 346, 479Berg, J.
van den, 18, 479Bert, D., 490Best, E., 266, 479, 482, 486Bjørner, D., 488Boer, F. S. de, 12, 150, 183, 240, 305,477–479, 488Bouajjani, A., 16, 480Bougé, L., 405, 478Bowen, J. P., 406, 480, 490Bowman, H., 482Brookes, S. D., 305, 405, 480Burch, J. R., 16, 480Burdy, L., 240, 480Cardelli, L., 51, 480Cavalcanti, A. L. C., 406, 490Chandy, K. M., 370, 480Chang, B.-Y. E., 479Cheon, Y., 480, 485Clarke, E.
M., 16, 125, 183, 266, 480,481Clermont, P., 405, 478Clifton, C., 485Clint, M., 266, 480Cok, D. R., 480, 485Cook, S. A., 125, 481Cousot, P., 16, 449, 481Cousot, R., 16, 449, 481Dahl, O.-J., 240, 481Dalen, D. van, 52, 481Damm, W., 183, 481Dams, D., 487DeLine, R., 479Derrick, J., 482Dershowitz, N., 477Dijkstra, E. W., 13–15, 26, 56, 86, 113,125, 126, 324, 331, 346, 349, 350,370, 403, 424, 481Dill, D. L., 480Dong, J. S., 406, 486Elrad, T., 305, 481Emden, M.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
