Fondations logiques des langages orientés objet et basés sur les cadres

Nous proposons un nouveau formalisme, appelé Logique de Cadre (abrégé, F-logique), qui rend compte de manière claire et déclarative de la plupart des aspects structurels des langages orientés objet et basés sur les cadres. Ces caractéristiques incluent l'identité des objets, les objets complexes, l'héritage, les types polymorphes, les méthodes de requête, l'encapsulation, et d'autres. En un sens, la F-logique se trouve dans la même relation avec le paradigme orienté objet que le calcul des prédicats classique avec la programmation relationnelle. La F-logique a une sémantique théorique des modèles et une théorie de preuve basée sur la résolution qui est solide et complète. Un petit nombre de concepts fondamentaux issus de la programmation orientée objet ont une représentation directe dans la F-logique ; d'autres aspects secondaires de ce paradigme sont également faciles à modéliser. L'article aborde également les questions sémantiques relatives à la programmation avec un langage orienté objet déductif basé sur un sous-ensemble de la F-logique.