Základné pojmy

• unless (a špeciálne prípady stable a invariant)

• ensures

• leads-to (oznacenie ?)

• Safety: p unless q, p is stable, p is invariant

• Progress: p ensures q, p ? q

• pouzívame univerzálnu kvantifikáciu; x = k unless x > k znamená ? ?k :: x = k unless x > k ?

Previous slide

Next slide

Back to first slide

View graphic version