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