© 1996-2021







2.1 Syntax

The syntax of ITL is defined in Table 9 where
z denotes an integer value,
A denotes a state integer variable,
b denotes a Boolean value,
Q denotes a state propositional variable,
ig denotes a integer function symbol,
bg denotes a Boolean function symbol,
V denotes state integer variable,
ei denotes a Boolean or integer expression,
h denotes a predicate symbol.

Table 9:Syntax of finite and infinite ITL
Expressions
ie ::=
z | A | ig(ie1,,ien) | A | fin A
Boolean Expressions
be ::=
b | Q | bg(be1,,ben) | Q | fin Q
Formulae
f ::=
true | h(e1,,en) f | f1 f2 |V f |skip | f1 ; f2 | f







2021-04-09
Contact | Home | ITL home | Course | Proofs | Algebra | FL