# 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_{0}(φ) the variables x ⊆ VAR such that x_{0} appears in φ. An assertion will be interpretedwith respect to a 4-tuple (σ_{0};σ;ρ; γ). The state σ_{0} 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 σ_{0} and any σ and ρ with

If var_{0}(C) = ø then this reduces to the original definition.