ITL
© 1996-2018







1 Syntax

The key notion of ITL is an interval. An interval σ is considered to be a (in)finite sequence of states σ01, where a state σi is a mapping from the set of variables Val to the set of values Val. The length |σ| of an interval σ0σn is equal to n, one less than the number of states in the interval (this has always been a convention in ITL), i.e., a one state interval has length 0. The syntax of ITL is defined in Table 1 where
z is an integer value,
a is a static integer variable (doesn’t change within an interval),
A is a state integer variable (can change within an interval),
v a static or state integer variable,
g is a integer function symbol,
q is a static Boolean variable (doesn’t change within an interval),
Q is a state Boolean variable (can change within an interval),
h is a predicate symbol.


Table 1: Syntax of ITL
Expressions
e ::=
z|a|A|g(e1,,en)|A| fin A
Formulae
f ::=
true|q|Q| h(e1,,en)|¬f|f1 f2|v f|skip|f1 ; f2|f







2018-02-25
Contact | Home | ITL home | Course | Proofs | Algebra | FL