### 2 Semantics

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

• A: if interval is non-empty then the value of A in the next state of that interval else an arbitrary value.
• ﬁn A: if interval is ﬁnite then the value of A in the last state of that interval else an arbitrary value.
• 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 and f2 over the suﬃx, or if the interval is inﬁnite and f1 holds for that interval.
• f holds if the interval is decomposable into a ﬁnite number of intervals such that for each of them f holds, or the interval is inﬁnite and can be decomposed into an inﬁnite number of ﬁnite intervals for which f holds.

Let E( ) be the “meaning” (semantic) function from Expressions × + Σω) to Val and let M( ) be the “meaning” function from Formulae × + Σω) to Bool (set of Boolean values, {tt,}) and let σ = σ0σ1 be an interval. We write σ vσif the intervals σ and σare identical with the possible exception of their mappings for the variable v. The formal semantics is listed in Table 2:

Table 2: Semantics of ITL
Ez(σ)
=
Ea(σ)
=
σ0(a) and for all 0 < i |σ|i(a) = σ0(a)
EA(σ)
=
σ0(A)
Eg(e1,,en)(σ)
=
ĝ(Ee1(σ),, Een(σ))
EA(σ)
=
 σ1(A) if |σ| > 0 choose-any-from(Val) otherwise
Eﬁn A(σ)
=
 σ|σ|(A) if σ is ﬁnite choose-any-from(Val) otherwise
Mtrue(σ)
=
tt
Mq(σ)
=
σ0(q) and for all 0 < i |σ|i(q) = σ0(q)
MQ(σ)
=
σ0(Q)
Mh(e1,,en)(σ) = tt
iﬀ
ĥ(Ee1(σ),, Een(σ))
M¬f(σ) = tt
iﬀ
not (Mf(σ) = tt)
Mf1 f2(σ) = tt
iﬀ
(Mf1(σ) = tt) and (Mf2(σ) = tt)
Mskip(σ) = tt
iﬀ
|σ| = 1
Mv f(σ) = tt
iﬀ
(for all σ s.t. σ vσ, Mf(σ) = tt)
Mf1 ; f2(σ) = tt
iﬀ
(exists k, s.t. Mf1(σ0σk) = tt and Mf2(σkσ|σ|) = tt)
or (σ is inﬁnite and Mf1(σ) = tt)
Mf(σ) = tt
iﬀ
if σ is ﬁnite then
(exist l0,,ln s.t. l0 = 0 and ln = |σ| and
for all 0 i < n,li li+1 and Mf(σliσli+1) = tt)
else
(exist l0,,ln s.t. l0 = 0 and
Mf(σlnσ|σ|) = tt and
for all 0 i < n,li li+1 and Mf(σliσli+1) = tt)
or
(exist an inﬁnite number of li s.t. l0 = 0 and
for all 0 i,li li+1 and Mf(σliσli+1) = tt)

 2018-03-10 Contact | Home | ITL home | Course | Proofs | Algebra | FL