#### 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) ﬁrst 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 ﬁn f ≜ (empty ⊃f) ﬁnal 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)∗∧ ﬁn ¬f0 while loop repeat f0 until f1 ≜ f0 ; (while ¬f1 do f0) repeat loop f1 ↦ f0 ≜ (f1 ⊃ ﬁn f0) always followed by f1 ↔f0 ≜ (f1 ≡ ﬁn 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 ≜ (ﬁ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-03-16 Contact | Home | ITL home | Course | Proofs | Algebra | FL