© 1996-2019







2.1 Syntax

The syntax of ITL is defined in Table 9 where
z denotes an integer value,
a denotes a static integer variable,
A denotes a state integer variable,
b denotes a Boolean value,
q denotes a static propositional variable,
Q denotes a state propositional variable,
ig denotes a integer function symbol,
bg denotes a Boolean function symbol,
v denotes static or 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|A|ig(ie1,,ien)|A| fin A
Boolean Expressions
be ::=
b|q|Q|bg(be1,,ben)|Q| fin Q
Formulae
f ::=
true|h(e1,,en)|¬f|f1 f2|v f|skip|f1 ; f2|f







2019-03-16
Contact | Home | ITL home | Course | Proofs | Algebra | FL