Séance 1

• Sémantique opérationnelle naïve NikOpNaive.thy
• Sémantique opérationnelle à grands pas NikBigStep.thy

Voir la page Niklaus.SemOpBigStep pour les propriétés de cette sémantique, ainsi que pour la version à petits pas.

Séance 2

• Corrigé de l'exercice du tutoriel TutoExosCorrige.thy
• Sémantique dénotationnelle naïve NikDenNaive.thy
• Définitions récursives :
  • Fonctionnelles et points fixes

Séance 3

• Plus faible précondition, consistance et complétude de la sémantique axiomatique NikAxWeakestPrecondition.thy
• Correction de l'algorithme d'Euclide pour le PGCD NiklausGCD.thy
• Exemple de fichier Why3 pour prouver cet algorithme codé en C gcd.c