ITL
© 1996-2015







20 Syntax First Order ITL

Syntax of Integer Expressions:

  • Integer values: 0,1,... ,
  • Static integer variable: a,b,...
  • State integer variable: A, B,...
  • Integer operators: +, - ,*,**, mod,div,...
  • Temporal integer variable: CA (nextA),CB, ... , finA (finA ),fin B,...

Syntax of Formulae:

  • Boolean values: true,false
  • Boolean static variables: p,q,...
  • Boolean state variables: P,Q, ...
  • Boolean predicates: e1 = e2,e1 ⁄= e2,e1 < e2,e1 ≤ e2  , e1 > e2,e1 ≥ e2,...
  • Boolean operators: ∧,∨,, ⊃, ≡,∀v  o f
  • Temporal operators: skip,;,* ,C,!,  ,...

Syntax of Integer Expressions in BNF:

e ::=   z|a |A |g (e1,...,en )|C A|finA

where z is an integer constant and g an integer operator.

Syntax of First Order Formulae in BNF:

f ::=   true|q|Q|h (e ,...,e )|f |f  ∧ f |∀v o f|
       skip|f ;f  |f1*      n      1    2
            1   2

where h is a Boolean predicate.

Derived formulae:

false     =^  tru e
f1 ∨ f2  =^  (f1 ∧ f2 )
f1 ⊃ f2  =^  f1 ∨ f2
f1 ≡ f2  =^  (f1 ⊃ f2) ∧ (f2 ⊃ f1)
∃v  o f  =^  ∀v  o f
C f      =^  skip ;f
inf      =^  true ;false
finite     =^  inf
  f      =^  finite;f
! f      =^  (  f )
...