ITL
© 1996-2018







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.
  • fin A: if interval is finite 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 prefix and suffix interval, such that f1 holds over the prefix and f2 over the suffix, or if the interval is infinite and f1 holds for that interval.
  • f holds if the interval is decomposable into a finite number of intervals such that for each of them f holds, or the interval is infinite and can be decomposed into an infinite number of finite 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
Efin A(σ)
=
σ|σ|(A)
if σ is finite
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
iff
ĥ(Ee1(σ),, Een(σ))
M¬f(σ) = tt
iff
not (Mf(σ) = tt)
Mf1 f2(σ) = tt
iff
(Mf1(σ) = tt) and (Mf2(σ) = tt)
Mskip(σ) = tt
iff
|σ| = 1
Mv f(σ) = tt
iff
(for all σ s.t. σ vσ, Mf(σ) = tt)
Mf1 ; f2(σ) = tt
iff
(exists k, s.t. Mf1(σ0σk) = tt and Mf2(σkσ|σ|) = tt)
or (σ is infinite and Mf1(σ) = tt)
Mf(σ) = 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 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 infinite number of li s.t. l0 = 0 and
  for all 0 i,li li+1 and Mf(σliσli+1) = tt)







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