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) :

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 :

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.

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

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

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()

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 :

Avec Sofus 2.0

Depuis la version 2.0, Sofus est doté de quelques possibilités de calcul formel, lesquelles permettent de faire l’exercice plus rapidement :

Simplification du programme de calcul A :

Simplification du programme de calcul B :

Résolution de l’équation A(x)=B(x) :

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é :

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 :

Avec Sofus 2.0

On peut maintenant remplacer les nombres par des noms de variables :

1. Pour que 2x+1 se termine par un 7 il faut et il suffit que 2x se termine par un 6, et pour cela il faut et il suffit que x se termine, soit par un 3, soit par un 8. Ce qui répond à la première question.
2. En développant la somme x+x+1 du nombre x et de son successeur, on trouve aussi 2x+1, ce qui répond à la seconde question.

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 (!).

This work is in the Public Domain.

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 :

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 dessin ci-dessus dessinent la même figure :

Sauriez-vous le prouver ?