La logique des algorithmes

Logique de Hoare au brevet des collèges
jeudi 15 avril 2010
par  Alain BUSSER

Des démonstrations sur des programmes de calcul sont souvent demandées au brevet des collèges. Par exemple

  • « Vérifier qu’en choisissant 2 au départ avec le programme A, on obtient 9 » (la vérification est bien une rédaction de preuve) ;
  • Montrer qu’une fonction est affine (sujet Polynésie 2016 ci-dessous) ;
  • Montrer que deux programmes de calcul A et B sont équivalents, c’est-à-dire que pour tout x fourni en entrée, A(x)=B(x).

Or ces preuves ne peuvent être correctes que si la logique utilisée tient compte du fait que la valeur de vérité de propositions portant sur les variables, varie elle-même au cours du temps (au cours de l’exécution du programme). C’est le cas de la logique de Hoare présentée ici.

Il peut sembler peu raisonnable d’aborder cette logique en collège voire au lycée, mais est-il raisonnable d’exiger des preuves de ce genre au collège ? N’y a-t-il pas un risque à présenter comme preuves, des productions qui n’en sont pas vraiment, même si elles sont conformes aux attendus de l’énoncé, et à une pratique régulière en classe ? D’ailleurs comment appeler ces « pseudo-preuves » attendues au brevet, sinon « vérifications » comme on le voit dans les sujets, ou « expliquer si elle est vraie ou fausse » (sujet Polynésie) ?

Hoare

Charles Antony Richard Hoare n’est pas réellement le premier à chercher à démontrer qu’un algorithme fait ce pour quoi il a été créé, mais la logique qu’il a formalisée il y a plus de 40 ans continue à servir non seulement à justifier des algorithmes mais aussi à en créer.

L’utilité de cette logique est triple :

  1. Un programme étant donné, démontrer qu’il implémente bien l’algorithme représenté ;
  2. Un programme étant donné, deviner quel algorithme il implémente ;
  3. Un algorithme étant donné, construire un programme correct.

Chacune de ces tâches est susceptible d’être elle-même informatisée, ce qui donne lieu à des logiciels analysant ou construisant des algorithmes. Un exemple dans la langue de Goethe.

Les exemples ci-dessous sont extraits du brevet des collèges 2016 : Polynésie et Métropole-Réunion-Antilles-Guyane.

Sujet Métropole

On considère les deux programmes de calcul ci-dessous.

Programme A Programme B
1. Choisir un nombre.
2. Multiplier par −2.
3. Ajouter 13.
1. Choisir un nombre.
2. Soustraire 7.
3. Multiplier par 3.

1. Vérifier qu’en choisissant 2 au départ avec le programme A, on obtient 9.
2. Quel nombre faut-il choisir au départ avec le programme B pour obtenir 9 ?
3. Peut-on trouver un nombre pour lequel les deux programmes de calcul donnent le même résultat ?

Pour essayer ces deux programmes sur un même nombre, on peut actionner le curseur ci-dessous (un clic droit ou un toucher long permet d’ouvrir la page dans un autre onglet du navigateur) :

HTML - 29.7 ko
sujet DNB 2016

Comme le logiciel Sofus est spécialisé dans l’étude de programmes de calcul, c’est ce logiciel qui sera utilisé ici. Il est tout-à-fait conforme au programme du collège puisqu’il utilise la programmation par blocs.

Programme A

Le programme A, dans Sofus, donne quelque chose comme ceci :

En l’exécutant, on a bien le nombre 9 qui s’affiche en bas de la fenêtre de sortie, mais comment prouver qu’on obtient 9 ? Pour cela, il faut donner les valeurs successives du nombre (qui est une variable), chacune prouvant la suivante.

Débogage

Quand on corrige des bogues, on ajoute des affichages après chaque instruction, ce qui en Sofus peut se faire ainsi :

Ces ajouts de texte dans la fenêtre de sortie produisent le texte suivant :

Maintenant nombre = 2
Maintenant nombre = -4
Maintenant nombre = 9

La logique de Hoare consiste juste à remplacer les vérifications par affichage, par des propositions qui sont vraies au moment où on les cite :

Après chaque instruction, une affirmation concernant le nombre choisi au départ, devient vraie ; ces propositions sont coloriées en vert par Blockly :

La copie d’écran ci-dessus constitue une preuve dans la logique de Hoare ; on constate que chaque instruction (en mauve) est prise en sandwich entre deux propositions (en vert) avec la convention suivante : Si la proposition du dessus est vraie juste avant l’exécution de l’instruction, alors celle du dessous est vraie juste après l’exécution de l’instruction.. On va se servir de cette logique pour prouver que A est affine.

Version Xcas

Pour travailler sur A vu comme fonction de nombre, on utilise cette forme légèrement modifiée du programme :

En cliquant sur le bouton « exporter Xcas » de Sofus, on obtient alors ce texte dans la zone de sortie :

function A(nombre) {
  nombre := nombre * -2;
  nombre := nombre + 13;
  return nombre;
}:;

En copiant-collant ce code vers le logiciel Xcas, on peut faire la séance Xcas suivante, où non seulement Xcas prouve que A(2)=9 mais aussi que A est affine :

Pour démontrer que A(x)=-2x+13, on va utiliser la logique de Hoare, et celle-ci s’utilise par chaînage arrière : On part du but à démontrer et on remonte le script, instruction par instruction :

On veut prouver qu’à la fin de l’exécution du script, le nombre est devenu -2x+13 (x étant la valeur initiale du nombre). On écrit donc nombre=-2x+13 tout en bas. Ensuite, on remonte le script, à chaque fois en remplaçant chaque occurence de nombre par ce que produit l’instruction sur nombre :

  • augmenter nombre de 13 a pour effet de remplacer nombre par nombre+13 : La proposition nombre=-2x+13 est donc remplacée par nombre+13=-2x+13 pusque seul le premier membre était nombre et on a effectué sur ce membre la substitution citée ;
  • multiplier nombre par -2 mène alors à la substitution de nombre par -2×nombre, qui mène à la deuxième proposition en partant du haut ;
  • fixer nombre à x mène à la substitution de nombre par x, laquelle aboutit alors à la tautologie -2x+13=-2x+13 tout en haut.

On peut maintenant lire la preuve de haut en bas :

  • -2x+13 est toujours égal à -2x+13 ; a fortiori avant l’exécution du script ;
  • Après la première instruction (qui est une affectation), nombre=x ce qui donne -2×nombre+13=-2x+13 (qui n’était pas vraie avant l’affectation, mais est vraie à ce stade) ;
  • Après la seconde (et avant-dernière) instruction, nombre a été multiplié par -2 et on peut laisser tomber le -2× qui est devant : C’est maintenant nombre+13 qui est égal à 2x+13 (ce qui n’était pas le cas, ni avant l’exécution de cette instruction, ni ne sera le cas après comme on le verra : Cette égalité est vraie de façon éphémère) ;
  • Enfin, après ajout de 13, ce n’est plus nombre+13 mais nombre lui-même qui est égal à -2x+13.

Ceci prouve qu’à la fin du script (et à ce moment seulement), la variable nombre est égale à -2x+13. Et cette preuve fournit à son tour la preuve que A est affine.

Programme B

Voici le programme B, programmé en Sofus :

Cette fois-ci, il s’agit non de prouver mais de trouver. Avec l’export Xcas par exemple, on peut utiliser solve pour chercher l’antécédent de 9 par B. Mais la résolution de l’équation passe d’abord par l’écriture de l’équation, et celle-ci nécessite encore une fois de prouver que B, vu comme fonction de x, est affine et égale à 3(x-7)=3x-21. Là encore, la logique de Hoare vient à la rescousse, une fois qu’on sait ce qu’on doit prouver :

La preuve par Coq

Pour prouver que B est affine, on peut utiliser les possibilités de calcul formel que permet Coq, en l’occurence en utilisant le fait que R est un anneau (« ring ») :

Require Import Reals.
Open Scope R_scope.
Definition A (x:R): R := -2*x+13.
Definition B (x: R): R := let y:=x-7 in 3*y.
Lemma Run: forall x:R, B(x)=3*x-21.
Proof.
    intros.
    unfold B.
    ring.
Qed.

Mais dans le cas présent Coq n’a fait qu’un développement par distributivité et un logiciel de calcul formel permettrait de trouver 3x-21 par développement, alors qiue Coq ne permet que de prouver que l’expression développée est 3x-21.

De même, why3 permet de « prouver » que pour tout x réel, B(x)=3x-21, avec ce script :

module Brevet
  use import real.Real
  use import ref.Ref
let fB (x:real) : real
    ensures { result=3.0*x-21.0 }
  = let y = ref x in
    y := !y-7.0;
    y := !y * 3.0;
    !y
end

En effet si on clique sur la roue dentée, on apprend assez rapidement que « VC for fB » apparaît en vert pour indiquer que la condition « require » est vraie. De cette forme de programmation par contrat peut d’ailleurs venir une idée de corrigé par Python. L’exercice est d’écrire le programme de calcul en Python ; avec une production attendue de ce genre :

def B(x):
        y = x
        y -= 7
        y *= 3
        return y

Si la fonction s’appelle bien B, l’interro sera faite avec

from random import *
def interro():
        note = 0
        for n in range(20):
                x = randrange(100)
                try:
                        assert(B(n)==3*n-21)
                        note += 1
                except:
                        return note
        return note
               
       
print interro()

Une note sur 20 est donnée, et vaut 20 si la fonction coïncide avec B sur 20 nombres choisis au hasard.

Avec mathem@ALGO

En allant sur mathem@ALGO on peut programmer en Sofus dans l’onglet « Xcas/Blockly », section « tableur ». Le nom de la variable a été choisi pour permettre une communication automatique avec le tableur (histoire d’afficher l’historique du programme) :

Pour prouver quelque chose par le calcul littéral, il suffit de remplacer le nombre choisi par un nom de variable, par exemple x :

Le problème est que le résultat n’est pas réduit :

Mais on est dans Xcas, il suffit donc de demander, dans la cellule suivant du tableur, un développement (« expand ») :

Preuve convaincante et facile à obtenir, bravo mathem@ALGO !

La suite de l’exercice se fait par l’algèbre, en résolvant des équations ; là, Hoare n’y peut rien.

Avec ekoarun

Une fois prouvé que A(x)=-2x+13 et B(x)=3x-21, on peut répondre à la dernière question en résolvant l’équation -2x+13=3x-21. Par exemple avec ekoarun. Une fois l’équation entrée au clavier virtuel d’ekoarun, on obtient ceci :

Ensuite on glisse le terme « 3x » à gauche, et le terme « +13 » à droite, ce qui change leur signe :

Ensuite on simplifie les deux membres (en les sélectionnant puis en cliquant sur Σ)

Ensuite, pour finir d’isoler x, on sélectionne le premier membre, et on choisit la bonne option dans le menu qui s’ouvre alors :

Mais oui, la bonne option c’est « ×(-1/5) » :

Une fois simplifiée, l’équation peut être considérée comme résolue :

Sujet Polynésie

Voici le sujet :

Voici un programme de calcul :

•Choisir un nombre entier positif
•Ajouter 1
•Calculer le carré du résultat obtenu
•Enlever le carré du nombre de départ.

1. On applique ce programme de calcul au nombre 3. Montrer qu’on obtient 7.
2.Voici deux affirmations :
Affirmation n°1 : « Le chiffre des unités du résultat obtenu est 7 ».
Affirmation n°2 : « Chaque résultat peut s’obtenir en ajoutant le nombre entier de départ et le nombre entier qui le suit ».
a.Vérifier que ces deux affirmations sont vraies pour les nombres 8 et 13.
b.Pour chacune de ces deux affirmations, expliquer si elle est vraie ou fausse quel que soit le nombre choisi au départ

On peut le manipuler en ligne avec un curseur ne prenant que des valeurs entières puisque c’est ce qui est suggéré dans l’énoncé :

HTML - 31.8 ko
sujet DNB Polynésie 2016

Pour le programmer en Sofus, on a besoin d’une autre variable, copie, pour stocker le nombre de départ jusqu’à la fin, où on a besoin de la copie parce que l’original a été modifié entre-temps :

Prouver qu’on a 7

Les affichages sont donc plus nombreux qu’avant :

Ce script avec affichages donne ces affichages :

nombre = 3
copie = 3
nombre = 4
nombre = 16
copie = 9
nombre = 7

Et la méthode d’Hoare donne ceci :

Pour vérifier d’un coup les deux affirmations, on peut là aussi commencer par prouver que le programme de calcul est affine, et que si le nombre choisi au départ est noté x, on a 2x+1 à l’arrivée. Avec la logique de Hoare, cela donne cette preuve :

Alors on finit vite l’exercice :

  • Avec x=10 on a 2×10+1=21 qui finit par 1 et pas par 7 ; l’affirmation 1 est donc fausse (démonstration par contre-exemple) ;
  • x+(x+1) est effectivement égal à 2x+1, pour tout x entier naturel.

Avec Xcas

Une fois qu’on sait gérer la variable supplémentaire copie, on peut tout mettre dans un bloc :

L’export vers Xcas donne ce code :

function Tahiti(nombre) {
   local copie;
  copie := nombre;
  nombre := nombre + 1;
  nombre := pow(nombre,2);
  copie := pow(copie,2);
  nombre := nombre - copie;
  return nombre;
}:;

Une fois copié-collé ce code dans Xcas, on peut rapidement avoir cette séance qui prouve l’affirmation 2 :

Remarque : Avec le bloc qui a été créé ci-dessus, il est assez facile d’infirmer l’affirmation 1 :

Ceci dit, pour faire ce petit script, il faut savoir

  • Comment programmer une boucle avec indice (ici, n) ;
  • Quel est le lien entre le dernier chiffre et la division euclidienne par 10...

Avec Coq et Alt-Ergo

Puisque la variable x est un entier naturel, on pense à quelque chose comme ceci :

Definition f1 (x:nat): nat := let y:=x+1 in y*y-x*x.
Definition f2 (x: nat): nat := x+x+1.
Compute f1 3.
Compute f1 8.
Compute f1 13.

Mais à moins de se lancer dans la grande aventure d’une démonstration par récurrence (au brevet des collèges c’est peut-être légèrement prématuré !), on ne voit pas comment démontrer l’égalité entre les fonctions f1 (le programme de l’énoncé) et f2 (la somme de l’entier et de son successeur). On en revient là encore au calcul formel, avec la tactique ring de Coq, et pour celle-là, il faut travailler dans un anneau unitaire comme Z ou R. Dans le premier cas, on charge Z pour faire la démonstration :

Require Import ZArith.
Open Scope Z_scope.
Definition f1 (x:Z): Z := let y:=x+1 in y*y-x*x.
Definition f2 (x: Z): Z := x+x+1.
Theorem tahiti: forall (x: Z), f1(x) = f2(x).
Proof.
    intros.
    unfold f1, f2.
    ring.
Qed.

Quand on démarre la démonstration on a

1 subgoals
______________________________________(1/1)
forall x : Z, f1 x = f2 x

Après les introductions :

1 subgoals
x : Z
______________________________________(1/1)
f1 x = f2 x

On fait l’hypothèse que x est entier et on a pour but de montrer que f1(x)=f2(x). Unfold développe les expressions f1 et f2 :

1 subgoals
x : Z
______________________________________(1/1)
(x + 1) * (x + 1) - x * x = x + x + 1

La tactique ring peut montrer cette égalité, par le calcul formel.

Avec l’outil de preuve en ligne Alt-Ergo le script suivant permet de démontrer l’égalité entre les deux fonctions :

goal tahiti :
  forall x,y:int.
  y=x+1  ->
  y*y-x*x=x+x+1

En fait, l’outil de preuve de l’avenir est probablement why3 ; on lui soumet ce fichier :

theory Tahiti "Brevet des collèges"
  use import int.Int
 
  function f1 (x:int): int=let y=x+1 in y*y-x*x
  function f2 (x:int): int=x+x+1
  lemma Affine: forall x:int. f1 x = f2 x
end

puis on clique sur la roue dentée ; le bouton coché signifie que le lemme affine est prouvé :

Mais malgré ce que son nom laisse penser, why ne fait que valider le théorème, sans expliquer pourquoi il est vrai (c’est-à-dire sans donner la démonstration).

Avec mathem@ALGO

En allant sur mathem@ALGO, puis en cliquant successivement sur « Blockly/Xcas » et sur « tableur Xcas », on peut reprogrammer avec Sofus, mais cette fois-ci en mettant la copie dans la colonne B et en utilisant une variable anonyme comme x comme valeur initiale :

Les étapes du calcul sont maintenant détaillées, sous forme littérale, dans le tableur :

Pour achever la preuve, il suffit de demander à Xcas de simplifier le résultat, par exemple dans B4 :

La logique de Hoare ne se limite pas à examiner des programmes de calcul sans tests ni boucles. Des extensions sont proposés dans le pdf suivant, programmé en JavaScript et concernant plutôt le lycée :

La version Lycée

L’objet de l’article ci-dessous est une liste d’exemples illustrant comment la logique de Hoare fonctionne, en l’ocurrence sur des exemples de la classe de Seconde. Les exemples sont rédigés en JavaScript, avec un code de couleurs qui devrait, pour les lecteurs non daltoniens, faciliter la lecture. Pour autant le sujet n’est pas vraiment facile...

Il est à remarquer que la logique de Hoare achoppe sur des sujets tels que la récursivité et le calcul parallèle, qui par un étrange hasard, sont hors du programme du lycée...

Le pdf ci-dessous est placé sous license « creative commons » : Vous avez le droit de le lire (youpi !) et de le diffuser ; vous avez même le droit de le modifier (c’est d’ailleurs le but du choix de cette license). La seule chose dont vous n’avez pas le droit, c’est de prétendre en être l’auteur (!).

Creative Commons License
This work is in the Public Domain.

PDF - 113.6 ko
L’article au format pdf

Nouveau : présentation à l’IREM le 12 avril 2017

Au séminaire de l’IREM le 12 avril 2017, a été présenté le sujet, avec le diaporama suivant :

PDF - 1.1 Mo

Voici le plan :

  1. Exemple du sujet du brevet (Polynésie 2016 traité ci-dessus)
  2. Corrigé de la question l’image de 3 est 7, en rédigeant des propositions là où elles sont vraies ; transition vers la logique de Hoare
  3. remarques épistémologiques : Avant Hoare il y a eu Floyd, et même avant lui, Turing
  4. exemples liés au domaine des transports, où apparaît la nécessité de prouver (avec Coq) le logiciel qui gère la fusée ou le train
  5. preuve par Coq de l’égalité des deux fonctions (récurrence avortée, puis théorie des anneaux ; extensions de l’exercice à partir de la preuve issue de la théorie des anneaux)
  6. obtention automatique de la théorie de Coq (à compléter) par why3 ; variante acec Alt-Ergo qui est un prouveur automatique (opacité de la preuve et impossibilité de prouver tout, d’après le théorème de Church)
  7. La nécessité de passer par le calcul formel (théorie des anneaux) incite alors à traiter l’exercice du brevet uniquement par le calcul formel : Présentation de l’extraordinaire outil mathem@ALGO qui permet de passer automatiquement de la programmation visuelle au tableur de calcul formel.
  8. En guise de conclusion, un exemple de programme de tortue, sur lequel on pose des questions similaires à celles portant sur les programmes de calcul :

Les deux programmes de calcul ci-dessus dessinent la même figure :

Sauriez-vous le prouver ?


Commentaires

Annonces

Prochains rendez-vous de l’IREM

Séminaire EDIM-IREM

- Mercredi 12 avril 2017, 14h-18h, campus du Tampon, amphi 120C
- Mercredi 3 mai 2017, 14h-18h, PTU, Saint-Denis, salle S23.6
- Mardi 13 juin 2017, 14h-18h, campus du Tampon
- Mercredi 14 juin 2017, 14h-18h, PTU, Saint-Denis, salle S23.6


Brèves

Décès de Raymond Smullyan

mercredi 15 mars

Le logicien Raymon Smullyan est décédé en février 2017, à l’âge respectable de 97 ans : Il avait eu Alonzo Church comme professeur ! Pour en savoir plus, voir cet article

Travailler à plusieurs

lundi 19 décembre 2016

Les enseignements d’exploration au lycée imposent aux enseignants de travailler ensemble. Chantal Tuffery-Rochdi a analysé dans sa thèse les pratiques des enseignants de MPS (méthodes et pratiques scientifiques). Elle répond aux questions des Cahiers pédagogiques.

Un document sur Eduscol

mardi 19 mai 2015

Un document clarifiant bien la façon dont les mêmes concepts vivent en mathématiques et dans les sciences « exactes » les utilisant, publié par Eduscol en octobre 2014. Citons-les :
« Le document proposé ci-dessous s’adresse aux professeurs de mathématiques, physique-chimie et sciences de l’ingénieur intervenant dans le segment [Bac-3 ; Bac+3]. Il vise à les informer des différences de présentation et d’interprétation qui sont faites de certains concepts mathématiques dans les autres disciplines. Ces éclaircissements peuvent contribuer à harmoniser et à clarifier l’utilisation de ces notions auprès des élèves. »

Histoire de la comptabilité

vendredi 28 décembre 2012

Sur ce site (en anglais) dédié à la comptabilité, on trouve des informations intéressantes sur l’histoire et les pratiques de ce domaine, qui peuvent être utiles aux professeurs enseignant des mathématiques financières (et aussi aux autres...).

La CGE et la réforme des lycées

lundi 16 janvier 2012

La Conférence des Grandes Écoles publie 19 préconisations pour la réforme du lycée.

Sur le Web : Les 19 préconisations

Pratique des mathématiques en série STD2A

lundi 16 janvier 2012

Le site de l’IGEN offre des recommandations et des ressources pour enseigner les mathématiques en série STD2A. Les thèmes abordés (couleurs et nuances de gris, arcs et architecture, jeux vidéos, photo et tableur, perspectives parallèles...) sont de nature à donner aussi des idées d’activités aux enseignants des autres séries !

En cheminant avec Kakeya

lundi 16 janvier 2012

Un livre (à télécharger) de Vincent Borelli et Jean-Luc Rullière qui présente le calcul intégral et la dérivation en s’appuyant sur la question de Kakeya. Pour les lycéens, les étudiants et tous les esprits curieux qui souhaitent voir les mathématiques sous un jour différent.

Sur le Web : Livre à télécharger

Bicentenaire Galois

lundi 12 septembre 2011

À l’occasion du bicentenaire de la naissance d’Évariste Galois (1811-2011), l’Institut Henri Poincaré et la Société mathématique de France organisent un ensemble de manifestations et proposent un site contenant diverses ressources documentaires susceptibles d’intéresser les enseignants.

Statistiques

Dernière mise à jour

jeudi 27 avril 2017

Publication

740 Articles
Aucun album photo
130 Brèves
11 Sites Web
126 Auteurs

Visites

50 aujourd'hui
1249 hier
1994849 depuis le début
10 visiteurs actuellement connectés