kirancodes.me
To Proof Maintenance & Beyond!
ASE 1998

Identifying Pre-Conditions with the Z/EVES Theorem Prover

Yves Ledru

DOI 10.1109/ase.1998.732566dblp

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.

BibTeX
@inproceedings{Ledru:ASE98,
  author    = {Yves Ledru},
  title     = {Identifying {Pre-Conditions} with the {Z/EVES} Theorem Prover},
  booktitle = {ASE},
  pages     = {32-},
  publisher = {{IEEE} Computer Society},
  year      = {1998},
}

Related papers