Abstraction de données : modules et spécifications dans Coq

Cette séance de cours couvre le concept d'abstraction de données en programmation, en se concentrant sur l'utilisation de modules et de types de modules dans l'assistant de preuve Coq. Il commence par une introduction à la structure des modules, en particulier le type de module QUEUE, qui comprend des paramètres pour les types de données et les opérations telles que la file d'attente et la file d'attente. L'instructeur discute des spécifications axiomatiques, fournissant des axiomes qui définissent le comportement de ces opérations, telles que la mise en file d'attente vide et la relation entre les opérations de mise en file d'attente et de mise en file d'attente. La séance de cours explore également la mise en œuvre de différentes structures de files d'attente, y compris ListQueue et TwoStacksQueue, et comment celles-ci peuvent être définies à l'aide du système de modules dans Coq. Tout au long de la séance de cours, l'instructeur souligne l'importance des spécifications formelles pour assurer l'exactitude des structures de données et de leurs opérations, illustrant ces concepts avec des exemples pratiques et des extraits de code Coq. La session se termine par une discussion sur les relations d'équivalence et leur application à l'abstraction de données, renforçant les fondements théoriques du matériel présenté.