- Un exemple allant de la spec à l'IMPLEMENTATION (l'opération maximum d'un tableau)
- avec la construction de la boucle WHILE DO INVARIANT VARIANT END
- avec utilisation de la substitution "devient tel que" ( x : P)
- un complément aux clauses d'une machine avec le PROMOTES et l'EXTENDS pour l'INCLUDES (illustration par des dessins, cas Coffres bancaires)
- Enseignement, j'ai cité France culture de dimanche matin, écouté alors que je mettais au point le sujet du ds en latex.
Aucun commentaire:
Enregistrer un commentaire