Cours 1 : Introduction générale (2h).

I - Intro

II - Frama-C

III - Contrats de fonctions (ACSL - 1)

IV - Weakest Precondition -- ou comment prouver les contrats (fonctionnement WP).

Cours 2 : Logique de Floyd-Hoare.

I - Rappels - débrief TP.

II - Principe de la logique de Floyd-Hoare.

Cours 3: Calcul de la plus faible précondition et boucles.

I - Weakest précondition (sans boucle).

II - Les boucles.

Cours 4: Correction totale

I - Résumé de l’épisode précédent (boucles):

II - Correction totale.