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

Public Concerné

Le cours présente progressivement toutes les connaissances requises.

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.

Capacité et compétences acquises

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

Organisation

6Crédits

Contenu de la formation

Programmation et logique
- Proplog et le calcul propositionnel
- Datalog et bases de données relationnelles et déductives
- Prolog et le calcul des prédicats du 1er ordre
Validation des programmes
- calcul des séquents et tableaux sémantiques
- preuves de Hoare et de Dijkstra
Application aux programmes Java
- assertions java
- validation de programmes Java : ESC

Accès à PLEIAD

ACTUS-PRESSE

CNAM et entreprises

Préinscription en ligne

Documents à télécharger

l’alternance en vidéos