Table des matières

Sémantique

Enseignant Site/Liens Cours TD TP ECTS
Cours : E. Violard
TD : N. Magaud
à voir. peut être des TD/TP via racine de N. Magaud 18 18
Objectifs
Acquérir les bases théoriques des techniques de spécification et preuve de programme.
Contenu
Fondements de la programmation Preuve de programmes.
Correction partielle et terminaison.
Préconditions, postconditions, invariants, variants.
Logique de Hoare.
Weakest préconditions de Dijkstra.
Application à la construction rationnelle de programmes.
Spécification algébrique.
Signatures hétérogènes, variables et termes.
Logique équationnelle, preuves déductives et inductives.
Préconditions et équations conditionnelles.
Eléments de sémantique dénotationelle : algèbre multisorte, évaluation, junks, confusion, initialité.
Initiation à un langage de spécification algébrique.
Application aux structures de données usuelles.
Prérequis
Logique et programmation logique, connaissance d'un langage impératif.
Références
BLACKHOUSER R., Program Construction and Verification, Prentice-Hall, 1986.
BERGSTRA J.A. & al., Algebraic Specifications, Addison-Wesley, 1988.
GOGUEN J.A. & al., Applications of Algebraic Specifications using OBJ, CUP, 1992.
Contrôle des Connaissances
Contrôle continu : coeff. 1/3
Examen écrit : coeff. 2/3 (durée : 2h)

Notes (par dates)

TD

 
m1ilc/semantics.txt · Dernière modification: 2010/05/24 10:19 par suitable
 
Sauf mention contraire, le contenu de ce wiki est placé sous la licence suivante :CC Attribution-Noncommercial-Share Alike 3.0 Unported
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki