© 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 inﬁnite interval isinf(f) ≜ inf ∧ f is inﬁnite ﬁnite ≜ ¬inf ﬁnite interval isﬁn(f) ≜ ﬁnite ∧ f is ﬁnite fmore ≜ more ∧ ﬁnite non-empty ﬁnite interval f ≜ ﬁnite ; f sometimes f ≜ ¬¬f always f ≜ ¬¬f weak next f ≜ f ; true some initial subinterval f ≜ ¬( ¬f) all initial subintervals f ≜ ﬁnite ; 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 ﬁn f ≜ (empty ⊃f) ﬁnal state sﬁn f ≜ ¬(ﬁn(¬f)) strong ﬁnal 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(isﬁn(f)∗) inﬁnite chopstar fstar(f) ≜ isﬁn(isﬁn(f)∗) ∨ isﬁn(isﬁn(f)∗) ; isinf(f) ﬁnite chopstar while f0 do f1 ≜ (f0 ∧ f1)∗∧ ﬁn ¬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 ≜ ﬁnite ∧ (ﬁn 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-05-10 Contact | Home | ITL home | Course | Proofs | Algebra | FL