NFP120 : Spécification logique et validation des programmes séquentiels (6 ECTS)

Pré-requis

Le cours présente progressivement toutes les connaissances requises, néanmoins il est souhaitable d'avoir des notions de logique (propositionnelle, des prédicats). L'UE NFP108 est par exemple une très bonne introduction.

Objectifs

Donner les principes fondamentaux d'une programmation et d'une documentation rigoureuse.
Montrer comment la documentation formelle permet la validation des logiciels.
Remarque: Ce cours comportait précédemment une longue introduction à Prolog, cet aspect du cours a été retiré.

Contenu

Programmation et logique
 

• sémantique des formules logique
• méthode de déduction logique: tableaux sémantiques
• sémantique des programmes
• méthode de déduction sur les programme: preuves de Hoare, invariants de boucles
• Application aux programmes Java ou C (assertions, outils de validation)

Modalités de validation

Une évaluation en contrôle continu est conseillée (TP, QCMs...). Un examen final sur table est obligatoire, avec un coefficient minimal de 50% de la note finale.

Compétences visées

Maitrise de techniques formelles de spécification et de validation de programmes.

Formations

Cette unité d'enseignement est dispensée dans les formations suivantes :

• Titre RNCP Niveau 6 Concepteur intégrateur d'infrastructures informatiques (systèmes et réseaux, applicatives, ou de sécurité) parcours Cybersécurité (CRN0803A)
• Titre RNCP Niveau 6 Concepteur intégrateur d'infrastructures informatiques (systèmes et réseaux, applicatives, ou de sécurité) parcours Systèmes d'information (CRN0802A)
• Titre RNCP Niveau 6 Concepteur intégrateur d'infrastructures informatiques (systèmes et réseaux, applicatives, ou de sécurité) parcours Systèmes et réseaux (CRN0801A)

Cette unité d'enseignement n'est dispensée dans aucun centre pour le moment.
N'hésitez pas à revenir consulter cette page régulièrement.