Abstract FR:

Dans les formalismes actuels de specifications algebriques, les proprietes des fonctions sont la plupart du temps decrites de facon recursive, ce qui conduit souvent a des specifications lourdes et peu claires. L'usage d'iterateurs peut simplifier les specifications en augmentant leur clarte et leur concision. Le propos de cette these est d'ajouter un outil d'iteration dans les specifications algebriques dont la definition soit la plus implicite possible, tout en restant dans un cadre de premier ordre. Dans la mesure ou une specification admet souvent une large classe de modeles, un iterateur doit etre coherent avec tous les modeles et ne peut donc pas etre defini en tenant compte des choix d'implementation (comme dans les langages de programmation). C'est pourquoi il est necessaire de definir une semantique propre aux iterateurs. Nous definissons le formalisme des sequence-specifications avec predicats: il constitue un nouveau formalisme dedie a la manipulation de listes de longueur non fixee. Ce formalisme etend le pouvoir d'expression des specifications algebriques et fournit un cadre tres general de specifications comportant des aspects non-deterministes, et polymorphes. Ce formalisme verifie des resultats d'initialite, de structuration, et l'existence d'un calcul correct et complet. Nous definissons le formalisme des specifications avec iterateurs a partir des sequence-specifications et nous donnons une semantique propre aux iterateurs. Nous prouvons qu'il existe une traduction des specifications avec iterateurs en sequence-specifications avec predicats qui conserve la semantique