Preuve De Propriété De Précédence

Preuve De Propriété De Précédence

Définition formelle de Prec(P1,P2) Afin de définir la sémantique formelle du pattern de précédence Prec(P1,P2), introduisons les notations suivantes : 1. Soit Σ l’ensemble des états du système M, op(σ) désigne les états atteignables à partir de l’état σ après exécution de l’opération op. L’expression σ |= P signifie que l’état σ vérifie le prédicat P. 2.

Soit Chs l’ensemble des chemins possibles, à partir de l’état initial σ0, en exécutant les différentes opérations Ops du système : Chs ={(σ0,σ1,…) | ∀i.(i ≥ 1 ⇒ ∃op.(op ∈ Ops∧σi ∈ op(σi−1)))} 3. Étant donnés un chemin ch = (σ0,σ1,…,σi,…) et un rang i (0 ≤ i), ch[i] représente l’état σi du chemin ch

Preuve du cas général Prec(P1, P2)

Rappelons que notre objectif est de prouver le pattern de précédence Prec(P1,P2). Remarquons que l’obligation de preuve du théorème (1) n’est pas applicable pour la preuve d’une telle propriété. En effet, la propriété Prec(P1,P2) peut être vérifiée alors que l’état précédant celui vérifiant le prédicat P2 ne satisfait pas P1 comme le montre la figure 5.2.

Cette figure montre des états non successifs vérifiant les prédicats P1 et P2 alors que les États intermédiaires ne satisfont pas P1. De plus, plusieurs chemins peuvent mener d’un état vérifiant P1 à un état qui satisfait P2. Comme le montre la figure 5.2, la propriété Prec(P1, P2) peut être décomposée en l’ensemble des propriétés suivantes : {Prec(P1, Ri)i∈1..n, PrécI( i∈1..n Ri, P2)} avec les prédicats Ri modélisant les états précédant immédiatement ceux vérifiant P2. Ainsi, le théorème 1 est appliqué sur la propriété Préc( i∈1..n Ri, P2) et le processus de décomposition est répété sur les propriétés Prec(P1, Ri)i∈1..n jusqu’à l’obtention de tous les états intermédiaires entre P1 et P2 ou la preuve que la propriété est fausse.