Formal specification and analysis of industrial systems
V. Bos, Jjt Jeroen Kleijn · TU/e Research Portal · 2002
ion: Suppose 〈 p, σ 〉 p d −→〈 pd, σd 〉 and 〈 p, σ 〉 p d ′ −−→〈 pd′, σd′ 〉, where p ≡ π(x) and d′ < d. Using Rule 44 we obtain 〈x, σ 〉 p d −→ 〈xd, σd 〉 and we can conclude that pd ≡ τA(xd). Also, 〈x, σ 〉 p d ′ −−→ 〈xd′ , σd′ 〉 and we can conclude that pd′ ≡ τA(xd′). Induction on x gives us 1. 〈xd′ , σd′ 〉 p d−d ′ −−−→ 〈xd, σd 〉, 2. ∀xd′,a, σd′,a, a : 〈xd′ , σd′ 〉 a −→〈xd′,a, σd′,a 〉 ⇒ ∃xa, σa, xd,a, σd,a : 〈x, σ 〉 a −→ 〈xa, σa 〉 ∧ 〈xd, σd 〉 a −→ 〈 xd,a, σd,a 〉, 3. 〈xd′ , σd′ 〉6 ↓. Lemma 4.53 is easily proved since we already derived that pd ≡ τA(xd) and pd′ ≡ τA(xd′). Rule 40 and result 1 of the induction on x give 〈 pd′, σd′ 〉 p d−d ′ −−−→ 〈 pd, σd 〉. To prove Lemma 4.55, we assume 〈 pd′ , σd′ 〉 a −→ 〈 pd′,a, σd′,a 〉 for some pd′,a, σd′,a, and a. Since pd′ ≡ τA(xd′), we find using Rule 42 or 43 and result 2 of the induction on x that pd′,a ≡ τA(xd′,a). We can distinguish two cases: a 6≡ τ or a ≡ τ . Suppose a 6≡ τ , then we know by result 2 of the induction on x that there are xa, σa, xd,a, and σd,a such that 〈x, σ 〉 a −→〈 xa, σa 〉, 〈xd, σd 〉 a −→ 〈xd,a, σd,a 〉, and a 6∈ A. Using Rule 42 we obtain 〈 τA(x), σ 〉 a −→ 〈 τA(xa), σa 〉 and 〈 τA(xd), σd 〉 a −→ 〈 τA(xd,a), σd,a 〉. So, we have 〈 p, σ 〉 a −→ 〈 pa, σa 〉 and 〈 pd, σd 〉 a −→ 〈 pd,a, σd,a 〉 with pa ≡ τA(xa) and pd,a ≡ τA(xd,a). In case a ≡ τ , we know by result 2 of the induction on x that there are xa′ and xd,a′ , such that 〈x, σ 〉 a ′ −−→ 〈xa′ , σa′ 〉, 〈xd, σd 〉 a ′ −−→ 〈xd,a′ , σd,a′ 〉, and a′ ∈ A. Using Rule 43 we obtain 〈 τA(x), σ 〉 τ −→ 〈 τA(xτ ), στ 〉 and 〈 τA(xd), σd 〉 τ −→ 〈 τA(xd,τ ), σd,τ 〉. So, we have 〈 p, σ 〉 a −→〈 pa, σa 〉 and 〈 pd, σd 〉 a −→〈 pd,a, σd,a 〉 with pa ≡ τA(xa), pd,a ≡ τA(xd,a), and a ≡ τ . To prove Lemma 4.56 we use result 3 of the induction on x, which tells us that 〈xd′ , σd′ 〉6 ↓. Since pd′ ≡ τA(xd′), Rule 41 does not apply to pd′ and we obtain 〈 pd′ , σd′ 〉6 ↓. 132 The specification language χσ 4 4.18 Process specifications in χσ In this section, we describe how process specifications can be written in χσ. It is important to know that the process specification mechanism of χσ is based on syntactic replacement. So, formal parameters are replaced by actual parameters. Furthermore, it is assumed that instantiation is finite and therefore, recursive process specifications are not allowed. However, infinite behaviour can be specified by the repetition operator as discussed in Section 4.9. In χσ, process specifications are equations. The general form is P (x1, . . . , xn) = p, where P is an identifier, x1, . . . , xn are programming variables, and p is a χσ process possibly containing the programming variables x1, . . . , xn. An example is presented in Chapter 8.