Le cinquième cours

portera sur :

• la clause REFINES et la machine REFINEMENT
  

• quelques raffinages (vous les trouverez dans le poly)
  

• la boucle, INVARIANT et VARIANT de boucle
  
• le théorème à prouver pour la boucle
  

On sera alors en pleine programmation.

Il nous restera les machines IMPLEMENTATION
celles que l'Atelier B transforme automatiquement en programmes en langage C ou en ADA ou en ...