Exemple

Goal "VARS a b                                     \
\    {true}                                        \
\    a := 0; b := X;                               \
\    WHILE Y <= b INV {X = a*Y + b & 0 <= b} DO    \
\      b := b-Y;                                   \
\      a := a+1                                    \
\    OD                                            \
\    {X = a*Y + b & 0 <= b & b < Y}                ";

Cette commande va initier la preuve du programme de calcul du quotient et du reste de la division entière de 2 nombres (X et Y). Les variables sont en minuscules, les constantes en majuscules. A noter que l'on doit indiquer les variables (ici a et b) après le mot VARS, et l'invariant de l'itération après le mot INV. Attention à respecter la syntaxe du langage impératif dont les construtions syntaxiques sont :

• SKIP                      (instruction vide)
• _ := _                    (affectation)
• _ ; _                     (séquence)
• IF _ THEN _ ELSE _ FI     (conditionnelle)
• WHILE _ INV {_} DO _ OD    (itération)
  

On prouve le théorème précédent en tapant:

by(hoare_tac Asm_full_simp_tac 1);
by(Auto_tac);

où les paramètres de la tactique hoare_tac ne sont pas utiles à connaître pour ce TP (on utilisera toujours ces mêmes paramètres).