TABLE OF CONTENTS Here b is a Boolean expression, p, q properties, L a list of values, j, k integers, and x an identifier; p(x) indicates a property p that uses identifier x.
| Property | Intuitive Meaning |
|---|---|
| b | b holds at the current cycle |
| !p | p does not hold at the current cycle |
| p && q | both p and q hold at the current cycle |
| p q | either p or q holds at the current cycle |
| p -> q | if p holds at the current cycle then q holds at the current cycle as well |
| p <-> q | shortcut for (p -> q) && (q -> p) |
| for x in boolean: && p(x) | shortcut for p('true) && p('false) |
| for x in {L}: && p(x) | shortcut for p(l 1) && p(l 2) && ... && p(l n) where l 1, l 2, etc. are items from list L |
| for x in {j:k}: && p(x) | shortcut for p(j) && p(j+1) && ... && p(k) |
| for x in boolean: p(x) | shortcut for p('true) p('false) |
| for x in {L}: p(x) | shortcut for p(l 1) p(l 2) ... p(l n) where l 1, l 2, etc. are items from list L |
| for x in {j:k}: p(x) | shortcut for p(j) p(j+1) ... |
