Frequently used derived constructs are listed in Table 11–14.
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 |
inf |
≜ |
true ; false |
infinite interval |
isinf (f) |
≜ |
inf ∧ f |
is infinite |
finite |
≜ |
¬inf |
finite interval |
isfin (f) |
≜ |
finite ∧ f |
is finite |
fmore |
≜ |
more ∧ finite |
non-empty finite interval |
f ⌢ g |
≜ |
(f ∧ finite) ; g |
strong chop |
f | ≜ | finite ; f | sometimes |
f |
≜ |
¬¬f |
always |
f |
≜ |
¬¬f |
weak next |
f |
≜ |
f ; true |
some initial subinterval |
f |
≜ |
¬( ¬f) |
all initial subintervals |
f |
≜ |
f ⌢ true |
some finite initial subinterval |
f |
≜ |
¬( ¬f) |
all finite initial subintervals |
f |
≜ |
finite ; f ; true |
some subinterval |
f |
≜ |
¬( ¬f) |
all subintervals |
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 |
sfin f |
≜ |
¬(fin (¬f)) |
strong final state |
halt f |
≜ |
(empty ≡ f) |
terminate interval when |
keep f | ≜ | (skip ⊃ f) | all unit subintervals |
fω |
≜ |
isinf ((isfin (f))∗) |
infinite chopstar |
fstar (f) |
≜ |
isfin (f∗) ; (empty ∨ isinf (f)) |
finite chopstar |
f⋆ |
≜ |
isfin (f∗) ∨ fω |
strong chopstar |
while f0 do f1 |
≜ |
(f0 ∧ f1)∗∧ fin ¬f0 |
while loop |
repeat f0 until f1 |
≜ |
f0 ; (while ¬f1 do f0) |
repeat loop |
Y := e |
≜ |
( Y ) = e |
assignment |
Y ≈ e |
≜ |
(Y = e) |
equal in interval |
Y ← e |
≜ |
finite ⊃ (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 |