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

Trouvez votre formation

Trouvez une Unité d'Enseignement

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