Assertions And Correctness Formulae

Assertions and correctness formulae: Let R be a special variable referring to the timed occurrence function which denotes the observable behaviour of a real-time system. Let MVAR be a set of logical variables with typical element M ranging over timed occurrence functions. The boolean primitive O@texp will be considered as an abbreviation of O 2 R(texp). In addition, the boolean primitiveO@M texp will be used as an abbreviation of O 2 M(texp) and similarlywe shall use P during M I  8t 2 I
P@Mt, and P inM I  9t 2 I
P@M t. Since R refers to all observables, the unrestricted occurrence of R in assertions leads to problems when trying to apply the parallel composition rule.

Definition (Event projection) If E is a set of observable events and r is a mapping, the restriction ρ↓ E of r to E at time τ is

Define obs(R ↓ E) = E.
Definition  (Interval projection) For an interval ⊆  TIME and a mapping ρ, ρ ↓ I is the restriction of ρ with respect to I and is defined as

Let x0 denote the initial state value of a variable x and let now now0 denote the starting time. Then instead of

we may write, using now0 to refer to the starting time

Let var(φ) denote the program variables in j and var₀(φ) the variables x ⊆ VAR such that x₀ appears in φ. An assertion will be interpretedwith respect to a 4-tuple (σ₀;σ;ρ; γ). The state σ₀ gives now0 and the terms x0 their value; the state σ, the mapping σ and the environment γ are as defined. The most important cases are:

Furthermore,

These additions lead to a slightly different definition of the validity of a correctness formula.

Definition  (Valid correctness formula) If X ⊆ VAR* is the list of all variables x ⊆ var(A) and X0 is the corresponding list of terms x0, the correctness formula is valid, iff for all γ and σ₀ and any σ and ρ with

If var₀(C) = ø then this reduces to the original definition.