3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 86
Текст из файла (страница 86)
H. van, 455, 481Emerson, E. A., 16, 481Engeler, E., 484, 489Ernst, M. D., 480Even, S., 485497498Faber, J., 486Feijen, W. H. J., 13, 478, 481Fernandez, J.-C., 480Filliâtre, J.-C., 125, 126, 481Finance, J. P., 487Fischer, C., 406, 482Fischer, M. J., 426, 482Flanagan, C., 18, 241, 482Flon, L., 370, 482Floyd, R., 12, 122, 452, 482Fokkinga, M., 266, 305, 482Foley, M., 101, 125, 172, 183, 482Francez, N., 12, 305, 403, 405, 455, 478,481–483Futatsugi, K., 486Galloway, A., 482Gasteren, A. J. M.
van, 13, 478, 481Gaudel, M.-C., 484, 487Genuys, F., 481Girard, J.-Y., 51, 483Gordon, M. J. C., 58, 483Gorelick, G. A., 125, 483Grau, A., 150, 183, 483Gries, D., 12–15, 80, 113, 116, 125, 126,257, 261, 262, 266, 268, 276, 292,305, 307, 308, 311, 314, 320, 321,345, 346, 361, 370, 405, 478, 483,486, 488Groote, J. F., 484Grumberg, O., 16, 455, 480, 483Hähnle, R., 17, 18, 241, 479Halbwachs, N., 480Hallerstede, S., 13, 371, 477Halmos, P. R., 26, 483Hankin, C., 16, 487Hannemann, U., 487, 488Harel, D., 17, 125, 483Heide, F.
M. auf der, 485Hennessy, M. C. B., 14, 58, 483Henson, M. C., 490Henzinger, T. A., 455, 477Hill, U., 150, 183, 483Hoare, C. A. R., 12, 14, 15, 17, 65,68, 99, 101, 125, 126, 172, 183,246, 254, 266, 346, 374, 405, 480,482–484Hoenicke, J., 406, 484, 486Hooman, J., 405, 484, 488Huisman, M., 240, 484Hutter, D., 489Hwang, L. J., 480Author IndexJacobs, B., 18, 240, 479, 484Janssen, W., 305, 484Jensen, T., 479Jha, S., 480Jones, C. B., 124, 485Josko, B., 183, 481Jouannaud, J.-P., 487Joung, Y.-J., 455, 485Kaldewaij, A., 13, 183, 485Kariv, O., 485Katoen, J.-P., 16, 478, 479Katz, S., 455, 478Kemmerer, R., 486Kiniry, J. R., 480Knapp, E., 305, 485Knuth, D. E., 272, 485Kozen, D., 17, 483Kurki-Suonio, R., 455, 478, 482König, D., 272, 485Lafont, Y., 51, 483Lakhnech, Y., 488Lamport, L., 12, 266, 281, 305, 371, 485Langenstein, B., 489Langmaack, H., 150, 183, 480, 483Lassez, J.-L., 455, 485Lauer, P.
E., 125, 370, 485Leavens, G. T., 17, 241, 480, 485, 487Leeuwen, J. van, 486Lehmann, D. J., 405, 455, 482, 483, 485Leino, K., 240, 477Leino, K. R. M., 479, 480, 482Lengauer, C., 266, 371, 479, 486Lepistö, T., 478Levin, G., 12, 405, 486Lillibridge, M., 482Lipton, R., 15, 305, 346, 486Loeckx, J., 28, 125, 150, 486Lu, Y., 480Maher, M. J., 455, 485Mahony, B. P., 406, 486Maibaum, T., 479Maibaum, T. S.
E., 484Makowsky, J. A., 483Manna, Z., 13, 325, 370, 478, 486Mason, R. E. A., 485McMillan, K. L., 480Meyer, B., 17, 486Meyer, R., 406, 486Milner, R., 405, 486Misra, J., 13, 370, 478, 480, 486Mitchell, J. C., 51, 486Author IndexMonien, B., 485Morgan, C., 13, 486Morris, J. M., 240, 487Mueller, P., 241, 487Muñoz, C., 488Möller, M., 406, 486Müldner, T., 266, 489Naumann, D. A., 240, 479Nelson, G., 482Neuhold, E. J., 480, 482, 487Newman, M. H. A., 250, 487Nielson, F., 16, 124, 487Nielson, H. R., 16, 124, 487Nieto, L. P., 345, 487Nipkow, T., 17, 345, 487Nonnengart, A., 489Nygaard, K., 240, 481Olderog, E.-R., 15, 183, 305, 325, 406,455, 478–480, 484, 486, 487, 489Owicki, S., 12, 14, 15, 80, 257, 261, 262,266, 268, 276, 292, 305, 307, 308,311, 314, 320, 321, 345, 346, 487,488Owre, S., 17, 488Park, D., 424, 488Paterson, M.
S., 426, 482Paul, M., 480Paulson, L. C., 17, 345, 487Peled, D. A., 16, 480Perrot, R. H., 484Peterson, G. L., 327, 488Pierik, C., 240, 488Plotkin, G. D., 14, 58, 405, 455, 478,483, 488Pnueli, A., 13, 325, 405, 455, 478, 483,485, 486, 488Podelski, A., 16, 455, 479, 487Poel, M., 266, 305, 482, 484, 488Poetzsch-Heffter, A., 241, 487Poll, E., 18, 479, 480Queille, J.-P., 16, 488Rajamani, S., 16, 479Rasch, H., 486Ravn, A.
P., 480Raymond, P., 480Raynal, M., 346, 488Reif, W., 479Reps, T. W., 16, 489Reynolds, J. C., 124, 240, 488499Robinson, K., 490Rock, G., 489Roever, W. P. de, 12, 403, 405, 406, 478,479, 482–484, 488, 489Roscoe, A., 489Roscoe, A. W., 405, 406, 480, 489Rosen, B. K., 266, 489Rozenberg, G., 479, 489Rössig, S., 406, 487Ruby, C., 485Rybalchenko, A., 486Sagiv, S., 16, 489Salomaa, A., 478Salwicki, A., 266, 489Saxe, J. B., 482Schellhorn, G., 479Schenke, M., 406, 489Schmitt, P. H., 17, 18, 241, 479Schneider, F.
B., 345, 489Scholten, C. S., 26, 481Schwartz, J. T., 482Scott, D. S., 58, 150, 489Sevinç, P. E., 406, 479Shankar, N., 17, 488Shepherdson, J. C., 480Sieber, K., 28, 125, 150, 486Sifakis, J., 16, 488Stata, R., 482Stavi, J., 455, 478, 485Steffen, M., 487Stenzel, K., 479Stephan, W., 17, 489Stevens, P., 479Stoy, J. E., 58, 489Strachey, C., 58, 489Suzuki, N., 370, 482Taguchi, K., 482Tarski, A., 448, 489Taylor, P., 51, 483Thums, A., 479Tiuryn, J., 17, 483Torii, K., 486Tucker, J.
V., 51, 124, 490Turing, A. M., 12, 490Veith, H., 16, 480, 483Vito, B. D., 488Wehrheim, H., 406, 482, 486Wenzel, M., 17, 345, 487Wilhelm, R., 16, 489Wirth, N., 125, 484500Author IndexWoodcock, J. C. P., 406, 484, 490Wright, J. von, 13, 370, 478Zwiers, J., 125, 266, 305, 406, 482, 484,488, 490Zucker, J.
I., 51, 124, 490Zöbel, D., 405, 490Symbol IndexSyntaxSemantics=object , 187V ar, 30[u := t], 42[x := new], 220≡, 25new, 217null, 187σ(s̄), 35change(S), 57, 376div, 30, 33divides, 30, 34f ree(p), 41int, 30, 34max, 30min, 30mod, 30, 33p[u := t], 45p[x := new], 220s[u := t], 43s[x := new], 221var(S), 57var(p), 41var(s), 32∆, 34, 311mod, 34⊥, 34init T , 218ν(σ), 219null, 218σ(s), 35σ[u := d], 36σ |= B, 41σ(o), 193σ(o)(x), 193σ[o := τ ], 194σ[u := new], 218τ [u := d], 194fail, 34, 96Mfair [[S]], 412Mwfair [[S]], 453M[[S]], 60Mtot [[S]], 61Mwtot [[S]], 310[[p]], 42, 200, 224<com , 414∅, 21∞∀ , 453card, 22min A, 22[x̄ := t̄], 46s[x̄ := t̄], 46at(T, S), 82∞∃ , 410Verification|=fair {p} S {q}, 430|= {p} S {q}, 64|=tot {p} S {q}, 64|=wtot {p} S {q}, 311N, 21501502⊢P D {p} S {q}, 66Z, 21A ⊢P φ, 39⊢P φ, 39even, 263iter(S, σ), 88odd, 263path(S), 285pre(T ), 80Symbol Indexwlp(S, Φ), 86wlp(S, q), 87wp(S, Φ), 86wp(S, q), 87{bd : t}, 83{inv : p}, 80{p} S ∗ {q}, 80{p} S {q}, 63<lex , 414.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
