COURS // INF3143 Modélisation et spécification formelles de logiciels
Description du cours
- Cycle : 1
- Type de cours : Magistral
- Nombre de crédits : 3
- Discipline : Informatique
Description
Le cours vise à initier les étudiants aux méthodes formelles de spécification et à leur rôle dans le cycle de développement des logiciels. Entres autres, il vise à familiariser les étudiants avec le mode descriptif de spécifications plutôt qu'avec le mode opérationnel (algorithme) auquel ils sont habitués. Il vise aussi à familiariser les étudiants avec les notions d'assertions, de contraintes et de contrats avec leur utilisation pour le développement de logiciels.
Rôle des spécifications et méthodes formelles.
Introduction à certaines notions formelles pour décrire des systèmes et composantes logiciels : diagrammes de classes et contraintes, automates et systèmes de transitions, contrats.
Approfondissement d'une approche basée sur les contraintes et contrats; logique : propositions et prédicats, quantificateurs, modélisation conceptuelle et description de propriétés; types abstraits : ensemble et multi-ensembles, séquences, spécifications comportementales, modélisation de composants divers (fonctions, types muables, types immuables), invariants, pré/post conditions.
Utilisation des assertions et contrats à l'étape de construction de logiciels : test unitaires, vérification dynamique de contrats.
Préalables académiques
[INF1130 Mathématiques pour informaticien] ou [MAT1060 Mathématiques algorithmiques] ; [INF2120 Programmation II]
