Cours numero 3: Sémantique opérationnelle et preuves de programmes

On a vu dans ce cours une sémantique opérationnnelle de Ocaml  qui montre que le
langage suit une stratégie d'appel par valeur.

On a ensuite montré comment raisonner par  induction bien fondée pour prouver la
terminaison de  programmes  et  des proprietés  de   programems par raisonnement
équationnel. On a appliqué tout cela sur l'exemple de l'associativité de append,
et la correction complète d'un programme qui implante le tri par insertion.

On a vu briévement ensuite les problèmes d'efficacité en temps et en espace.