Convertir les programmes impératifs en formules

Cette séance de cours couvre le processus de conversion des programmes impératifs en formules, en se concentrant sur la génération de conditions de vérification, la construction de formules et l'expression des affectations et des structures de flux de contrôle en tant que relations. Il explique comment représenter l'exactitude du programme en tant que condition de vérification et comment l'implémenter en tant qu'algorithme, en utilisant des exemples dans Stainless. La séance de cours traite également de la traduction d'énoncés impératifs, de choix non déterministes et d'hypothèses en formules. En outre, il explore les concepts de ravages, de programmes sans boucle et de chemins de programme, fournissant des informations sur la construction de formules de taille polynomiale pour décrire les comportements des programmes.