Raffinement de modèles topologiques en B événementiel: Des droites aux 2-G-cartes

摘要

Les modeleurs géométriques permettent de construire des images de synthèse. Leur développement est devenu une entreprise des plus complexes où l'utilisation des méthodes formelles s'avère bénéfique. L'expérience nous a montré qu 'il est difficile de prouver formellement la correction des opérations réalisées par ces modeleurs en manipulant des données conformes aux modèles mathématiques implantés dans les modeleurs. Pour que la preuve devienne réalisable, il est nécessaire de manipuler des données abstraites. Reste ensuite à raffiner ces données. Nous illustrons cette démarche sur une version simplifiée d'une opération géométrique classique. Plus précisément, nous démontrons via le processus de raffinement du B événementiel que l'on peut transformer un ensemble de droites en un ensemble de 2-G-cartes, modèles topologiques couramment utilisés et implantés au sein des modeleurs.