The informal semantics of the most interesting constructs are as follows:
: if interval is non-empty then the value of in the next state of that interval
else an arbitrary value.
: if interval is finite then the value of in the last state of that interval else
an arbitrary value.
unit interval (length 1).
holds if the interval can be decomposed (“chopped”) into a prefix and suffix
interval, such that holds over the prefix and over the suffix, or if the interval
is infinite and holds for that interval.
holds if the interval is decomposable into a finite number of intervals such that
for each of them holds, or the interval is infinite and can be decomposed into an
infinite number of finite intervals for which holds.
Let be the “meaning” (semantic) function from to and let
be the “meaning” function from to (set of Boolean values,
) and let be an interval. We write if the intervals and are
identical with the possible exception of their mappings for the variable . The formal semantics
is listed in Table 2:
Next
: if interval is non-empty then the value of 
in the next state of that interval
else an arbitrary value.
: if interval is finite then the value of 
in the last state of that interval else
an arbitrary value.
unit interval (length 1).
holds if the interval can be decomposed (“chopped”) into a prefix and suffix
interval, such that 
holds over the prefix and 
over the suffix, or if the interval
is infinite and 
holds for that interval.
holds if the interval is decomposable into a finite number of intervals such that
for each of them 
holds, or the interval is infinite and can be decomposed into an
infinite number of finite intervals for which 
holds.![[[ ...]]e](itlhomepage29x.png)
be the “meaning” (semantic) function from 
to 
and let
![[[...]]](itlhomepage32x.png)
be the “meaning” function from 
to 
(set of Boolean values,
) and let 
be an interval. We write 
if the intervals 
and 
are
identical with the possible exception of their mappings for the variable 
. The formal semantics
is listed in Table ![|------------------------------------------------------------------|
|[[ z ]]eσ = ˆz |
|[[ a ]]eσ = σ0(a) and for all 0 < i ≤ |σ |,σi(a) = σ0(a )
|[[ A ]]eσ = σ0(A) |
|[[ g(e1,...,en) ]]e = ˆg([[ e1 ]]e ,...,[[ en]]e) |
| σ { σ σ(A ) σ if |σ | > 0 |
|[[ C A ]]eσ = 1 |
| { choose-any-from (V al) otherwise |
|[[ fin A ]]eσ = σ |σ|(A ) if σ is finite |
| choose-any-from (V al) otherwise |
|[[ true ]]σ = tt |
|[[ q]]σ = σ0(q) and for all 0 < i ≤ |σ |,σi(q) = σ0(q)
|[[ Q ]]σ = σ0(Q) |
|[[ h(e ,...,e ) ]] = tt iff ˆh([[ e ]]e,...,[[ e ]]e) |
| 1 n σ 1 σ n σ |
|[[ ¬f ]]σ = tt iff not ([[ f ]]σ = tt) |
|[[ f1 ∧ f2 ]]σ = tt iff ([[f1 ]]σ = tt) and ([[ f2]]σ = tt) |
|[[ skip ]]σ = tt iff |σ | = 1 |
|[[ ∀v o f]]= tt iff (for all σ′ s.t. σ ~v σ′,[[f ]]σ′ = tt) |
|[[ f1 ;f2 ]]σ = tt iff |
| (exists k, s.t. [[ f1 ]]σ0...σk = tt and [[ f2]]σk...σ = tt) |
| or (σ is infinite and [[ f ]] = tt) |σ| |
| * 1 σ |
|[[ f ]] = tt iff |
|if σ is finite then |
| (exist l0,...,ln s.t. l0 = 0 and ln = |σ| and |
| for all 0 ≤ i < n,li ≤ li+1 and [[ f ]]σli...σli+1 = tt) |
| else |
| (exist l ,...,l s.t. l = 0 and |
| 0 n 0 |
| [[ f ]]σln...|σ| = tt and |
| for all 0 ≤ i < n,li ≤ li+1 and [[ f]]σli...σli+1 = tt) |
| or |
| (exist an infinite number of li s.t. l0 = 0 and |
| for all 0 ≤ i,li ≤ li+1 and [[ f]]σl...σl = tt) |
| i i+1 |
--------------------------------------------------------------------](itlhomepage41x.png)