Next Prev Up

#### 2.2 Semantics

Each state σi is the union of the mapping from the set of integer variables IntVar to the set of integer values and the mapping from propositional variables PropVar to set of Boolean values {tt, }.

Each interval has at least one state. 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. Let σ = σ0σ1σ2 be an interval then

• σ0…σk (where 0 k ≤|σ|) denotes a preﬁx interval of σ
• σk…σ|σ| (where 0 k ≤|σ|) denotes a suﬃx interval of σ
• σk…σl (where 0 k l ≤|σ|) denotes a sub interval of σ

The informal semantics of the most interesting constructs are as follows:

• A: if the interval is non-empty then the value of A in the next state of that interval else an arbitrary value.
• ﬁn A: the value of A in the last state of the interval.
• skip unit interval (length 1).
• f1 ; f2 holds if the interval can be decomposed (“chopped”) into a preﬁx and suﬃx interval, such that f1 holds over the preﬁx interval and f2 over the suﬃx interval.
• f holds if the interval is decomposable into a ﬁnite number of intervals such that for each of them f holds.

Let Σ+ denote the set of all ﬁnite intervals.
Let Expressions denote the set of (integer or Boolean) expressions.
Let Val denote the set of integer or Boolean values (Bool).
Let E( ) denote the meaning function from Expressions × Σ+ to Val.
Let Formulae denote the set of ITL formulae.
Let M( ) denote the meaning function from Formulae × Σ+ to Bool (set of Boolean values, {tt, }).
Let σ = σ0σ1 denote an interval.
We write σ V σif the intervals σ and σare identical with the possible exception of their mappings for the variable V .
Let choose-any-from(Val) denote the choice function that selects an arbitrary value from Val.
The formal semantics is listed in Table 2:

 Next Prev Up

 2023-09-14 Contact | Home | ITL home | Course | Proofs | Algebra | FL © 1996-2023