Cette séance de cours couvre la logique Hoare, qui permet d'insérer des annotations dans le code pour simplifier les preuves sur le comportement du programme. Les sujets abordés comprennent les relations informatiques, les ravages, les choix non déterministes, le commandement et la traduction des programmes en relations.