===== Sémantique =====


^ Enseignant ^ Site/Liens ^ Cours ^ TD ^ TP ^ ECTS ^
| Cours : E. Violard\\ TD : N. Magaud | à voir. peut être des TD/TP via [[http://dpt-info.u-strasbg.fr/~magaud/| racine de N. Magaud]] | 18 | 18 |  |  |
^ Objectifs ^^^^^^
| Acquérir les bases théoriques des techniques de spécification et preuve de programme. ||||||
^ Contenu ^^^^^^
| [[semantics_1|]]  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) ====

  * [[m1ilc:semantics_1|]] -- 28/01/2010 & 4/2/2010
  * [[m1ilc:semantics_2|]] -- 4/02/2010
  * [[m1ilc:semantics_3|]] -- 18/02/2010
  * [[m1ilc:semantics_4|]] -- 25/02/2010
  * [[m1ilc:semantics_5|]] -- 4/03/2010
  * [[m1ilc:semantics_6|]] -- 11/03/2010
  * [[m1ilc:semantics_7|]] -- 18/03/2010
  * [[m1ilc:semantics_8|]] -- 25/03/2010
  * [[m1ilc:semantics_9|]] -- 1/04/2010
  * [[m1ilc:semantics_a|]] -- 15/04/2010
  * [[m1ilc:semantics_b|]] -- 22/04/2010
  * [[m1ilc:semantics_c|]] -- 29/04/2010

==== TD ====

  * [[m1ilc:semantics_td_1|]] -- 5/2/2010
  * [[m1ilc:semantics_td_2|]] -- 19-26/2/2010
  * [[m1ilc:semantics_td_2a|]] -- 5/3/2010