ITL
© 1996-2018







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

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 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

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

keepnow f
(skip f)

initial unit subinterval

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

assignment

A exp
(A = exp)

equal in interval

A exp
finite (fin A) = exp

temporal assignment

A gets exp
keep(A exp)

gets

stable A
A gets A

stability

padded A
(stable(A) ; skip) empty

padded expression

A < exp
(A exp) padded A

padded temporal assignment

goodindex A
keep(A A A A + 1)

increasing index

intlen(exp)
I (I = 0) (I gets I + 1) (I exp)

interval length








2018-02-25
Contact | Home | ITL home | Course | Proofs | Algebra | FL