Frequently used derived constructs are listed in Table 3–6.
false |
≜ |
¬true |
false value |
f1 ∨ f2 |
≜ |
¬(¬f1 ∧¬f2) |
or |
f1 ⊃ f2 | ≜ | ¬f1 ∨ f2 | implies |
f1 ≡ f2 |
≜ |
(f1 ⊃ f2) ∧ (f2 ⊃ f1) |
equivalent |
∃V f |
≜ |
¬∀V ¬f |
exists |
f |
≜ |
skip ; f |
next |
more |
≜ |
true |
non-empty interval |
empty |
≜ |
¬more |
empty interval |
f |
≜ |
true ; f |
sometimes |
f |
≜ |
¬¬f |
always |
f |
≜ |
¬¬f |
weak next |
f |
≜ |
f ; true |
some initial subinterval |
f | ≜ | ¬( ¬f) | all initial subintervals |
f |
≜ |
true ; f ; true |
some subinterval |
f |
≜ |
¬( ¬f) |
all subintervals |
f g |
≜ |
¬(f ; (¬g)) |
yields |
f g |
≜ |
¬((¬f) ; g) |
reverse yields |
(f) |
≜ |
empty ∨ ( (f) ; skip) |
all strict initial intervals |
(f) |
≜ |
¬( (¬f)) |
some strict initial interval |
(f) |
≜ |
f ∧ (¬f) |
first occurrence |
if f0 then f1 else f2 |
≜ |
(f0 ∧ f1) ∨ (¬f0 ∧ f2) |
if then else |
if f0 then f1 |
≜ |
if f0 then f1 else true |
if then |
fin f |
≜ |
(empty ⊃ f) |
final state |
halt f |
≜ |
(empty ≡ f) |
terminate interval when |
keep f |
≜ |
(skip ⊃ f) |
all unit subintervals |
keepnow f | ≜ | (skip ∧ f) | initial unit subinterval |
while f0 do f1 |
≜ |
(f0 ∧ f1)∗∧ fin ¬f0 |
while loop |
repeat f0 until f1 |
≜ |
f0 ; (while ¬f1 do f0) |
repeat loop |
f1 ↦ f0 |
≜ |
(f1 ⊃ fin f0) |
always followed by |
f1 ↔ f0 |
≜ |
(f1 ≡ fin f0) |
strong followed by |
Y := e |
≜ |
( Y ) = e |
assignment |
Y ≈ e |
≜ |
(Y = e) |
equal in interval |
Y ← e |
≜ |
(fin Y ) = e |
temporal assignment |
Y gets e | ≜ |
keep (Y ← e) | gets |
stable Y | ≜ | Y gets Y | stability |
padded Y |
≜ |
(stable (Y ) ; skip) ∨ empty |
padded expression |
Y <∼ e |
≜ |
(Y ← e) ∧ padded Y |
padded temporal assignment |
intlen (e) |
≜ |
∃I (I = 0) ∧ (I gets I + 1) ∧ (I ← e) |
interval length |