Spécification Logique et Validation des Programmes Séquentiels

Objectifs :
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
Description des heures d'enseignements

Cours : 60: heures

Modalités de validation :
devoir hebdomadaire noté examen final
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