Transformations automatiques de spécifications sémantiques, applications : un vérificateur de types incrémental / par Laurent Hascoët

Bibliogr. p. 174-175

Thèse de doctorat informatique 1987 Nice

Pour le problème de la vérification de types incrémentale, nous commençons par exposer et justifier certaines contraintes sur le vérificateur de types à traiter. Lorsque ces contraintes sont vérifiées, nous fournissons un système en grande partie automatique qui génère un vérificateur de types incrémental à partir d'un vérificateur de types ordinaire. La méthode employée consiste d'une part à transformer une vérification de types comportant plusieurs passes, montantes et descendantes, sur l'arbre, pour obtenir un mécanisme en une seule passe montante. D'autre part, nous introduisons une notion de «delta», par laquelle on s'efforce de ne détecter que les erreurs de type qui sont apparues depuis la dernière vérification