Département d'Informatique

Maîtrise d'Informatique 2001/2002

Spécifications formelles, preuves

& construction de programmes

Travaux dirigés

Mardi 11 décembre

Théorèmes d'une spécification algébrique:
logique équationnelle et inductive

Où l'on cherche à montrer que notre spécification algébrique est suffisante pour décrire le type de données que l'on voulait spécifier, en faisant la preuve de certaines propriétés caractéristiques des opérations.
Dans la suite, on utilise la notation CafeOBJ pour écrire axiomes et théorèmes.

1 Logique équationnelle

Les démonstrations de théorèmes s'appuient uniquement sur les axiomes et les règles de remplacement d'égaux à égaux:

réflexivité
symétrie
transitivité
substitution
congruence

On considère les axiomes suivants pour spécifier les entiers naturels en supposant que les constructeurs 0 et s (successeur), l'opérateur + (addition) sont déclarés avec le bon profil dans la signature:
```
axioms {
  vars N M : Nat
   
  eq N + 0 = N .           -- axiome (1)
  eq N + s(M) = s(N + M) . -- axiome (2)
  }
```
Démontrer (en utilisant la logique équationnelle) que:
s(s(0)) + s(s(s(0))) == s(s(s(s(0)))) + s(0)
Comment CafeOBJ procède-t-il pour démontrer ce théorème ?
Peut-on démontrer le théorème suivant avec la seule logique équationnelle ?
```
  N + M == M + N
```

2 Logique inductive

La logique inductive est la logique équationnelle auquelle est ajoutée la règle d'induction qui autorise le raisonnement par récurrence.

Poursuivre l'exercice 1 pour prouver l'associativité de l'addition c'est-à-dire :
```
  vars L M N : Nat .
   
  L + (M + N) == (L + M) + N 
```
Démontrer la commutativité c'est-à-dire :
```
   
  N + M == M + N 
```
Dans le membre gauche des axiomes (1) et (2), les constructeurs s'appliquent sur le deuxième opérande de l'addition. Avant de montrer la commutativité, on pourra montrer par induction, deux lemmes similaires à ces axiomes, mais avec les constructeurs placés sur le premier opérande.
On ajoute maintenant au module en 1.(a), la multiplication et les axiomes suivants:
```
  eq N * 0 = 0 .              -- axiome (3)
  eq N * s(M) = (N * M) + N . -- axiome (4) 
```
On suppose avoir démontré la commutativité de la multiplication
(en utilisant la même démarche que pour l'addition).
En ajoutant un opérateur sum (pour la somme des n premiers entiers), démontrer un théorème inductif qui signifie:

∀ n ∈ IN .

n

&Sygma;

i=1
i =

n(n+1)

2

(on évitera la division par 2 en exprimant ce théorème différemment).

This document was translated from L^AT_EX by H^EV^EA.