Identifying Pre-Conditions with the Z/EVES Theorem Prover

9 years 6 months ago
Identifying Pre-Conditions with the Z/EVES Theorem Prover
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 preconditions. In this paper, the Z-EVES theorem prover is used to calculate and try to simplify the preconditions 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. Y. Ledru. Identifying pre-conditions with the Z/EVES theorem prover. In Proceedings of the 13th International Conference on Automated Software Engineering. pp. 32-41, IEEE Computer Society Press, Honolulu, 1998. This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights the...
Yves Ledru
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 1998
Where KBSE
Authors Yves Ledru
Comments (0)