Description du livre
Les spécifications formelles sont un outil important pour la construction, la vérification et l'analyse des systèmes, car sans elles, il n'est guère possible d'expliquer si un système a fonctionné correctement ou a montré un comportement attendu. Ce livre propose l'utilisation des théorèmes de représentation comme moyen de développer une compréhension de tous les modèles d'une spécification afin d'exclure d'éventuels modèles involontaires, démontrant la méthodologie générale avec des théorèmes de représentation pour des applications dans le raisonnement spatial qualitatif, le traitement des flux de données et la révision des croyances.
Pour le raisonnement spatial qualitatif, il développe un modèle de relation spatiale qui capture le contexte de mise à l'échelle avec des partitions hiérarchiques d'un domaine spatial et caractérise axiomatiquement les relations résultantes. Il montre également que diverses propriétés importantes du traitement des flux, telles que la détermination du préfixe ou diverses propriétés de factorisation peuvent être axiomatisées, et que les axiomes sont remplis par des classes naturelles de fonctions de flux. Le troisième exemple est celui de la révision des croyances, qui concerne la révision des bases de connaissances dans le cadre de nouvelles informations potentiellement incompatibles. Dans ce contexte, l'ouvrage examine une sous-catégorie d'opérateurs de révision, à savoir la classe des opérateurs de réinterprétation, et les caractérise de manière axiomatique. Une propriété caractéristique des opérateurs de réinterprétation est celle de dissoudre les incohérences potentielles en réinterprétant les symboles de la base de connaissances.
Destiné aux chercheurs en informatique théorique ou dans l'un des domaines d'application susmentionnés, l'ouvrage présente des résultats qui démontrent l'utilisation des théorèmes de représentation pour la conception et l'évaluation de spécifications formelles, et fournit la base des futurs kits de développement d'applications qui aideront les concepteurs d'applications à construire automatiquement des représentations.