Identifying pre-conditions with the Z/EVES theorem prover

Author

Ledru, Yves

Author_Institution

Lab. Logiciels Syst. Reseaux, IMAG, St. Martin-d´´Heres, France

fYear

1998

fDate

13-16 Oct 1998

Firstpage

32

Lastpage

41

Abstract

Starting from a graphical data model (a subset of the OMT object model), a skeleton of formal specification can be generated and completed to express several constraints and provide a precise formal data description. Then standard operations to modify instances of this data model can be systematically specified. Since these operations may invalidate the constraints, it is interesting to identify their pre-conditions. In this paper, the Z-EVES theorem prover is used to calculate and try to simplify the pre-conditions of these operations. Then the developer may identify a set of conditions and use the prover to verify that they logically imply the pre-condition

Keywords

computer aided software engineering; data description; data models; formal specification; object-oriented methods; theorem proving; OMT object model; Z-EVES theorem prover; constraints; data model instance modification operations; formal data description; formal specification skeleton; graphical data model; logical implication; preconditions identification; Automation; Electrical capacitance tomography; Encapsulation; Formal specifications; Natural languages; Read only memory; Skeleton; Testing; Unified modeling language;

fLanguage

English

Publisher

ieee

Conference_Titel

Automated Software Engineering, 1998. Proceedings. 13th IEEE International Conference on

Conference_Location

Honolulu, HI

Print_ISBN

0-8186-8750-9

Type

conf

DOI

10.1109/ASE.1998.732566

Filename

732566