© 1996-2019







1.3 Derived Constructs

Frequently used derived constructs are listed in Table 36.


Table 3: Frequently used non-temporal derived constructs
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



Table 4: Frequently used temporal derived constructs
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)
empty ((f) ; skip)

all strict initial intervals

(f)
¬((¬f))

some strict initial interval

(f)
f (¬f)

first occurrence



Table 5: Frequently used concrete derived constructs
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



Table 6: Frequently used derived constructs related to expressions
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








2019-01-03
Contact | Home | ITL home | Course | Proofs | Algebra | FL