Spécification logique et validation des programmes séquentiels

Public concerné et conditions d'accès

Le cours présente progressivement toutes les connaissances requises.

Finalités 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és et compétences visées :
Maitrise de techniques formelles de spécification et de validation de programmes.

Organisation

Nombre de crédits enseignements ECTS
6 ECTS

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, invariants de boucles
  • Application aux programmes Java (assertions, outils de validation)
Téléchargez la fiche de la formation: