ITL
© 1996-2015







26 Exercises First Order ITL

Exercise 8 Give the semantics of the following formulae:

true
false
f1 ∨ f2
f1 ⊃ f2
f1 ≡o f2
∃v  f
iff0 then f1 else f2

Exercise 9 Give the formal semantics of                      *
(skip ∧ Account = 50 )

Exercise 10 Give the informal semantics (picture) of following formulae:

A =  0 ∧ skip ∧ A := A + 1
len (6)
A =  0 ∧ len(2) ∧ A ← A + 1
len (4) ∧ A =  3 ∧ A gets A + 1
len (3) ∧ A =  2 ∧ stable A

Exercise 11 Given informal specification

  • the system’s behaviour consists of only two states,
  • in the initial state the variable Account is equal to 50 and
  • in the next state it is increased by 100 .

Give the corresponding ITL formula.

Exercise 12 Given the following “formal specification”

Spec =  {σ : σ =  σ0...σn and
             σ0 (Cash  ) = initialand
             σi+1(Cash ) = σi(Cash ) + 50
             for0 ≤ i < n
}

Give the corresponding ITL formula.