Exemple

Faisons une preuve de l'exemple du PGCD en utilisant ces règles. Pour cela on va présenter l'algorithme en mettant en commentaire les pré et post-conditions. On vérifie ensuite que les pré et post-conditions en commentaires peuvent être prouvées en utilisant les règles.

 		 $P:\{ a,b \in \mathcal{N} \}$

m:=a;

n:=b;

while  m != n do

if m > n then m := m - n fi

if m < n then n := n - m fi

od

$T:\{ m=pgcd(a,b) \wedge a,b \in \mathcal{N}\}$

En fait, le texte commenté ci-dessous permet de suivre la preuve. Dans cette présentation, le lecteur a toutes les informations qui lui permettent de reconstituer la preuve.

 		 $P:\{ a,b \in \mathcal{N} \}$

m:=a;

n:=b;

$Q:\{ m=a \wedge m=b \wedge a,b,m,n \in\mathcal{N}\}$

$Inv:\{ pgcd(a,b)=pgcd(m,n)\wedge a,b,m,n \in\mathcal{N} \}$

while  m != n do

if m > n then m := m - n fi

if m < n then n := n - m fi

od

$R:\{ pgcd(a,b)=pgcd(m,n)\wedge m=n \wedge a,b,m,n \in\mathcal{N} \}$

$T:\{ m=pgcd(a,b) \wedge a,b \in \mathcal{N}\}$

Prouvons d'abord:

 $P=\{ a,b \in \mathcal{N} \}$(A)

m:=a;

n:=b;

$Q:\{ m=a \wedge m=b \wedge a,b,m,n \in\mathcal{N}\}$

Preuve: Il suffit d'appliquer l'axiome de l'affectation:

		$Q[m \leftarrow a,n\leftarrow b]$

$=\{ m=a \wedge m=b \wedge a,b,m,n \in\mathcal{N}\}[m \leftarrow a,n\leftarrow b]$

$=\{ a=a \wedge b=b \wedge a,b,b,a \in\mathcal{N}\}$

$\Leftrightarrow\{ a,b \in\mathcal{N}\}$

$\Leftrightarrow P$

Prouvons maintenant:

 $Inv:\{ pgcd(a,b)=pgcd(m,n)\wedge a,b,m,n \in\mathcal{N} \wedgem\neq n \}$(I)

if m > n then m := m - n fi

if m < n then n := n - m fi

$Inv:\{ pgcd(a,b)=pgcd(m,n)\wedge a,b,m,n \in\mathcal{N} \}$

Preuve: On a (axiome de l'affectation):

		$P:\{ pgcd(a,b)=pgcd(m,n-m)\wedge a,b,m,n-m \in\mathcal{N} \}$

n := n - m

$Inv:\{ pgcd(a,b)=pgcd(m,n)\wedge a,b,m,n \in\mathcal{N} \}$


et

$P \wedge m<n \Rightarrow Inv$(théorème)


Et donc (if):

$Inv:\{ pgcd(a,b)=pgcd(m,n)\wedge a,b,m,n \in\mathcal{N} \}$

if m < n then n := n - m fi

$Inv:\{ pgcd(a,b)=pgcd(m,n)\wedge a,b,m,n \in\mathcal{N} \}$


De même on montre que: 

$Inv:\{ pgcd(a,b)=pgcd(m,n)\wedge a,b,m,n \in\mathcal{N} \}$

if m > n then m := m - n fi

$Inv:\{ pgcd(a,b)=pgcd(m,n)\wedge a,b,m,n \in\mathcal{N} \}$

On en déduit (en utilisant la règle de composition) (W)

En utilisant la règle du WHILE à (W) on a:

$\{Inv \}$(B)

while  m != n do

if m > n then m := m - n fi

if m < n then n := n - m fi

od

$\{Inv \wedge m=n\}$

Prouvons enfin:

 		 $P:\{ a,b \in \mathcal{N} \}$

m:=a;

n:=b;

while  m != n do

if m > n then m := m - n fi

if m < n then n := n - m fi

od

$T:\{ m=pgcd(a,b) \wedge a,b \in \mathcal{N}\}$

Preuve: Comme

		$\{Inv \wedge m=n\}\Rightarrow T$(C)


On déduit que (Règle de déduction appliquée à (B) et (C):

$Inv$(D)

while  m != n do

if m > n then m := m - n fi

if m < n then n := n - m fi

$T$


De même de:

$Q\Rightarrow Inv$(E)


On déduit que (Règle de déduction appliquée à (D) et (E):

$Q$(F)

while  m != n do

if m > n then m := m - n fi

if m < n then n := n - m fi

od

$T:\{ m=pgcd(a,b) \wedge a,b \in \mathcal{N}\}$


Enfin, par la règle de composition appliquée à (E) et (A):

$P$

m:=a;

n:=b;

while  m != n do

if m > n then m := m - n fi

if m < n then n := n - m fi

od

$T$