Séance de cours
Cette séance de cours de l'instructeur couvre le processus de conversion des programmes impératifs en formules, en se concentrant sur la génération de conditions de vérification. Il explique comment exprimer l'exactitude du programme en tant que condition de vérification et l'implémenter en tant qu'algorithme. La séance de cours se penche également sur la représentation des fragments de programme et des spécifications sous forme de formules, introduisant des énoncés impératifs, du non-déterminisme et des programmes sans boucle. Il détaille la construction de formules décrivant les relations entre les états initial et final de l'exécution du programme, y compris les affectations, les instructions if-else et les points-virgules de commande. Des exemples et des formules de calcul sont fournis pour illustrer les concepts.