© 1996-2019







2.3 Derived Constructs

Frequently used derived constructs are listed in Table 1114.


Table 11: 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 12: Frequently used temporal derived constructs
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
finite ; f

sometimes

f
¬¬f

always

f
¬¬f

weak next

f
f ; true

some initial subinterval

f
¬( ¬f)

all initial subintervals

f
finite ; f ; true

some subinterval

f
¬( ¬f)

all subintervals



Table 13: 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

sfin f
¬(fin(¬f))

strong final state

halt f
(empty f)

terminate interval when

shalt f
¬(halt(¬f))

strong terminate interval when

keep f
(skip f)

all unit subintervals

fω
isinf(isfin(f))

infinite chopstar

fstar(f)
isfin(isfin(f))

isfin(isfin(f)) ; isinf(f)

finite chopstar

while f0 do f1
(f0 f1) fin ¬f0

while loop

repeat f0 until f1
f0 ; (while ¬f1 do f0)

repeat loop



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








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