Preuve de programme

I. Bases logiques

A. Calcul des prédicats (du premier ordre)

Les formules de la logique du premier ordre sont des formules logiques dans lesquelles on peut trouver :

• des variables
• des connecteurs logiques
• des prédicats sur les variables (fonctions à valeur booléenne)
• des fonctions sur les variables
• des quantificateurs (universel et existentiel)

Exemple :

∀ x, ∀ y ∃ z.( x ∈ ℤ ∧ y ∈ ℤ ∧ z ∈ ℤ → (z ≥ 0 ∧ (x = y + z ∨ y = x + z)))
      

B. Un peu de vocabulaire

Une variable quantifiée (existentiellement ou universellement) est appelée variable liée.

Une variable non quantifiée est appelée variable libre.

Une formule close est une formule dont toutes les variables sont liées.

Un modèle M d'un langage du premier ordre est une structure (elements, fonctions, prédicats) dans lequel on donne un sens aux symboles du langage.

Une formule F est satisfaisable s'il existe un modèle M dans lequel F est vraie. On note alors M ⊧ F.

Une formule F est valide si et seulement si elle est vraie dans tout modèle du langage. On note cela ⊧ F.

Le calcul des prédicat est semi-décidable : il est possible d'énumérer tous les théorèmes, mais il n'existe pas d'algorithme capable de prouver à coup sûr n'importe quel théorème.

Sans les fonctions, le calcul des prédicats est complet : tout théorème est démontrable (théorème de complétude de Gödel). Cependant, si on rajoute les fonctions sur l'arithmétique, on obtient un système incomplet : il existe des théorèmes non démontrables (théorème d'incomplétude de Gödel).

C. Skolémisation

La skolémisation est un processus qui consiste à transformer une formule du calcul du prédicat de façon à :

• Supprimer tout quantificateur existentiel en remplaçant la variable quantifiée par une fonction des variables quantifiées universellement qui la précèdent ;
• Ramener tous les quantificateurs universels en tête de formule
• (Omettre les quantificateurs universels)

Exemple pour la formule précédente :

  ∀ x, ∀ y ( x ∈ ℤ ∧ y ∈ ℤ ∧ z(x,y) ∈ ℤ → (z ≥ 0 ∧ (x = y + z ∨ y = x + z)))

Transformable éventulement en :

  ( x ∈ ℤ ∧ y ∈ ℤ ∧ z(x,y) ∈ ℤ → (z ≥ 0 ∧ (x = y + z ∨ y = x + z)))

D. Triplet de Hoare

un Triplet de Hoare se note {Pré} Inst {Post}, avec :

• Pré : un prédicat (pré-condition)
• Inst : une instruction
• Post : un prédicat (post-condition)

Il permet de spécifier que si la propriété Pré est vraie avant l'exécution de l'instruction Inst, alors la propriété Post est vraie à la fin de l'exécution de l'instruction Inst. Les triples de Hoare permettent de :

• Donner la sémantique d'un langage
• Faire des preuves de programme

Exemples :

{x = n} (x = x+1) {x = n+1}
          

{x = n} (if b then x = n + 1 else x = n -1) {(b → x = n+1) ∧ (¬b → x = n - 1)}
          

Les notions de pré-condition et post-condition sont étendues aux fonctions/méthodes ainsi :

• Une précondition d'une fonction est un prédicat qui doit être vérifié lorsque la fonction est appelée ;
• Une postcondition d'une fonction est un prédicat qui doit être vérifié à la fin de l'exécution de la fonction.

Remarque : les préconditions et postconditions sont en fait des formules de la logique des prédicats skolémisées.

E. Substitution

Appliquer une substitution est une opération qui consiste à remplacer une ou plusieurs variables libres dans un prédicat par une valeur. On note en général une substitution {val1/var1, val2/var2, ...}.

Exemple :

{4/x, 5/y}(x + 1 = y) ≡ (4 + 1 = 5)

Mais on peut également noter une substitution [var1 := val1 || var2 := val2 ...].

Exemple :

[x := 4 || y := 5](x + 1 = y) ≡ (4 + 1 = 5)

En effet, une affectation n'est ni plus ni moins qu'une substitution...

Ainsi, à partir d'une précondition d'une fonction, on peut, instruction après instruction, établir la nouvelle propriété établie par l'instruction, et ainsi, vérifier si la fonction établit bien sa post condition.

Exemple :

f(x):
  PRE:
    x ≥ 0
  CORPS:
    x = x + 1; PROP : x ≥ 1
    x = 2 * x; PROP : x ≥ 2
    x = x - 1
  POST:
    x ≥ 1
  

Preuve de PROP 1 :
    x ≥ 0 → [x := x+1](x ≥ 1)
    x ≥ 0 → (x+1 ≥ 1)

Preuve de PROP 2 :
    x ≥ 1 → [x := 2x](x ≥ 2)
    x ≥ 1 → (2x ≥ 2)

Preuve de POST :
    x ≥ 2 → [x := x - 1](x ≥ 1)
    x ≥ 2 → (x-1 ≥ 1)

II. Invariant

A. Notion d'Invariant de boucle

Comment utiliser les mécanismes précédents avec une boucle ?

On introduit un invariant de boucle : prédicat vrai à chaque itération, mais tel que, conjugué à la condition de sortie de la boucle, il nous permette d'établir la post-condition.

Exemple :

def maximum(liste):
  max = liste[0]
  for i in range(0, len(liste)):
    if liste[i] > max:
      max = liste[i]
    #Invariant de boucle : max = maximum(liste[0:i])
  return max

B. Invariant de boucle et preuve

Principe de la preuve d'un invariant de boucle = preuve par récurrence :

• On prouve que l'invariant est vrai au départ

[INIT](INV)

• On prouve que si l'invariant est vrai à l'étape i, il est vrai à l'étape i+1 :

 INV → [CORPS_BOUCLE](INV)

L'invariant de boucle doit être là pour établir la post-condition. Il faudra donc que la formule suivante soit vraie :

PRE ∧ FIN_BOUCLE ∧ INV → POST

C. Invariant de classe

L'utilisation d'un objet d'une classe (avec encapsulation) peut être vue comme une suite d'appels des méthodes de l'objet, ce qui revient à comparer cela à une boucle sur un choix d'une méthode parmi toutes celles définies dans la classe. On peut donc associer un invariant à une classe. La preuve de cet invariant consistera à prouver que :

• À la création d'une instance de la classe, l'invariant est établi ;
• Chaque fois qu'une méthode de la classe est appelée, on peut considérer que l'invariant est vérifié, et il faut alors vérifier que cette méthode préserve l'invariant, c'est-à-dire qu'il est vrai à la fin de l'exécution de la méthode.

III. Preuve de correction partielle

Les principes vus précédemment permettent de vérifier que si on programme correct termine, alors il établit sa post-condition. C'est ce qu'on appelle la correction partielle.

Cela ne permet nullement de prouver que le programme se termine effectivement.

IV. Correction Totale

A. Définition

Pour qu'un programme soit réellement correct, il faut qu'il soit partiellement correct, et qu'il se termine. C'est ce qu'on appelle la correction totale.

B. Principe de preuve de terminaison

Pour prouver qu'une boucle termine, on va associer à la boucle un Variant.

C. Définitions

1. Variant

Un variant est une suite strictement décroissante définie sur une structure bien fondée.

2. Structure bien fondée

Une structure bien fondée est une structure (E, ≤) dans laquelle toute suite strictement décroissante possède une borne inférieure.

Exemple fréquemment utilisé de structure bien fondée : (ℕ, ≤).

d. Détail du processus de preuve

On vérifie qu'avant la première itération, le variant est bien défini (par exemple, est un naturel) :

PRE → V ∈ ℕ

On vérifie que la valeur du variant décroît et reste bien typée entre 2 itérations :

V = v ∧ INV → [CORPS_BOUCLE](V < v)

V. Applications

A. Préambule : écrire les pré-conditions, post-conditions et invariant en Python

Il est possible d'écrire ces différents prédicats dans un programme Python en utilisant les assertions. Cela n'a aucune valeur de preuve mais permet :

• de documenter le code
• d'avoir une exception claire à l'exécution si jamais une de ces propriétés venait à être violée.

Note sur les assertions en Python :

En Python, une assertion s'écrit sous l'une des formes suivantes :

• assert ExprBool, message
• assert ExprBool

lorsque l'instruction d'assertion est exécutée, l'expression à valeur booléenne ExprBool est évaluée. Si elle est vraie, le programme continue de s'exécuter. Sinon, le programme s'arrête avec une exception et l'éventuel message est affiché.

1. Écriture des préconditions

Clause assert au début des méthodes

2. Écriture des postconditions

Clause assert à la fin des méthodes

3. Écriture d'un invariant

• Écriture d'une méthode invariant() regroupant sous la forme d'une succession de "assert" toutes les propriétés d'invariance
• Appel de cette méthode à la fin du constructeur et à la fin de chaque méthode

B. Exemple

preuve01personne.py

C. Exercices

1. Preuves d'invariants de classe et de post-conditions

• Tenter de prouver la classe preuve02horloge.py. Proposer des corrections.
• sur la version corrigée de la classe Horloge, écrire la post-condition de la méthode incrémenter() et la prouver

2. Preuves sur les boucles

• Établir la preuve de correction partielle de la fonction maximum() définie dans le fichier preuve04boucleCorrectionPartielle.py
• Établir la preuve de terminaison de cette fonction de façon à établir la correction totale.

3. Travail personnel

Faire la preuve de correction totale pour la version non optimisée du tri à bulle donnée dans le fichier preuve06TriABulleNaif.py