NFP120 - Spécification logique et validation des programmes séquentiels   [ 6  crédits ]

Public Concerné
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.

Finalité de l'unité d'enseignement

Objectifs pédagogiques
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é.
Capacité et compétences acquises
Maitrise de techniques formelles de spécification et de validation de programmes.
Organisation
6 Crédits 
Contenu de la formation
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)

Trouvez votre formation

Trouvez une Unité d'Enseignement

Please install the Flash Plugin


Accés à PLEIAD

     
Formations en alternance Formation continue Cours du soir Formation à distance, e-learning Formations courtes DIF CIF Congé individuel de formation CIF CDI, CIF CDD, CIF HTT Contrat de professionnalisation Centre de bilan de compétences Compte Personnel de Formation CPF