Couvre la logique de Hoare, la post-condition la plus forte et la condition préalable la plus faible pour simplifier les preuves dans la programmation impérative.
Se concentre sur l'utilisation d'Inox pour la vérification des programmes, en démontrant le processus de vérification des programmes et en assurant l'exactitude.
Introduit Stainless, un outil open-source pour vérifier les programmes Scala, couvrant le langage, la modélisation, les conseils de vérification et les travaux intérieurs.
Explore les limites impératives de la programmation, les théories sans mutation, les principes de programmation fonctionnelle et l'histoire des langages fonctionnels.
Couvre les concepts de base de la programmation orientée objet en Java, mettant l'accent sur l'encapsulation, l'abstraction et l'importance d'organiser des programmes complexes.
Couvre la simulation d'événements discrets à l'aide de circuits numériques, de composants de base, de composants complexes et de la mise en œuvre de la simulation.
Couvre les concepts et la mise en œuvre de la programmation fonctionnelle dans Scala, mettant l'accent sur les fonctions, les données immuables et l'abstraction des données.
Explore la conversion de programmes impératifs en formules de vérification, couvrant les affectations, les instructions if-else et les points-virgules de commande.
Couvre la modélisation des instructions de contrôle avec des fonctions dans Scala, y compris les boucles while, les boucles de répétition et la traduction for-loops.
Décrit la logistique du cours et les objectifs de la programmation orientée objet, en mettant l'accent sur la gestion des erreurs et l'intégration de sessions pratiques avec l'apprentissage théorique.
Explore la mutation sûre dans Scala, en mettant l'accent sur la gestion de l'état mutable et son importance dans les interactions, la modélisation et l'efficacité de mise en œuvre.