thesis

Preuve de formules conditionnelles dans des spécifications algébriques conditionnelles

Defense date:

Jan. 1, 1986

Edit

Institution:

Paris 11

Disciplines:

Computer sciences

Authors:

Directors:

Abstract EN:

In this thesis, different proof methods in algebraic specifications are outlined. One of them (the induction-narrowing method) is extended to prove conditional formulas in conditional specifications. This method can only be applied on specifications satisfying the property of sufficient completness with respect to the constructors. This property is studied for conditional specifications.

Abstract FR:

Dans cette thèse, différentes méthodes de preuve automatique de théorèmes, définies dans le contexte des spécifications algébriques, sont résumées. Il est montré comment étendre une de ces méthodes, (la méthode par récurrence-surréduction) à la preuve de formules conditionnelles dans des spécifications algébriques conditionnelles. Cette méthode s'applique uniquement sur des spécifications satisfaisant la propriété de complétude suffisante par rapport aux constructeurs. Cette propriété est donc étudiée pour le cas des spécifications conditionnelles.