Go backward to Denotational Semantics
Go up to Top
Go forward to Example
- Answer is set of (tag, store) pairs.
- tag=true: store is valid.
- tag=false: error has occured.
- (f_1 then f_2)(s) sequences commands.
- f_1 operates on s producing set of stores.
- Each answer store is passed through f_2 producing an answer set.
- The answer sets are unioned.
- C represents non-determinism.
- T determines if at least one of the guards holds.
- Conditional: failure of all guards causes abortion.
- Loop: failure of all guards causes exit.
- G joins the effects of all those commands whose guards hold.
Id: intro.tex,v 1.2 1996/01/31 15:37:03 schreine Exp schreine