Kvantifikované tvrdenia
program F
1. ? ?S: S in F :: {p} S {q} ?
2. ? ?S: S in F :: {p} S {q} ?
Príklad: nech F ? ? j: b(j) :: t(j) ?
1. treba ukázat, ze {p ? b(j)} t(j) {q}
2. treba ukázat, ze existuje j také, ze b(j) platí a súcasne {p ? b(j)} t(j) {q}
Príklady
1. Hodnota x neklesá: univerzálne kvantifikované cez všetky císelné hodnoty k
? ?S :: {x = k} S {x ? k} ?
2. Správa ostáva v kanáli az kým nie je prijatá
- inch = in channel (v kanáli)
- rcvd = received (prijatá)
? ?S :: {inch} S {inch ? rcvd} ?
3. Ako 2 ale prijaté správy sú odstránené z kanálu
? ?S :: {inch ? ?rcvd} S {(inch ? ?rcvd) ? (?inch ? rcvd)} ?
4. Hodnota x je neklesajúca a stúpne
? ?S :: {x = k} S {x ? k} ?
? ?S :: {x = k} S {x > k} ?