NFP120

Spécification logique et validation des programmes séquentiels


6 crédits Pierre COURTIEU EPN05 - Informatique Unité d'enseignement de type cours

Publié Du 01-09-2007 au 31-08-9999

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

Compétences

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

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)

Thésaurus du Cnam :

  • Langage de programmation
  • Sémantique des programmes
  • Logiciel sur
  • Vérification
  • Preuve de logiciel

Thésaurus Formacode :

  • Aucune indexation

Secrétariat

Libellé
EPN05 - Informatique
Nom du contact
Safia Sider
Adresses email
safia.sider@lecnam.net
Numéros de téléphone
01 40 27 26 81
Adresse postale
2 rue Conté 33.1.13A
Paris 75003