Skip Navigation
York U: Redefine the PossibleHOME | Current Students | Faculty & Staff | Research | International
Search »FacultiesLibrariesCampus MapsYork U OrganizationDirectorySite Index
Future Students, Alumni & Visitors
2006 Technical Reports

Automated Model-based Verification of Object-Oriented Code

Jonathan Ostroff, Chen-wei Wang, Eric Kerfoot and Faraz Ahmadi Torshizi

Technical Report CSE-2006-05

York University

May 24, 2006


ESpec is a suite of tools that facilitates the testing and verification of Eiffel programs in an integrated environment. The suite includes testing tools and Fit tables (for customer requirements) that report contract failures. This paper describes ES-Verify (part of ESpec) for automatically verifying a significant subset of Eiffel constructs written with a value semantics. The tool includes a mathematical model library (sequences, sets, bags and maps) for writing high level specifications, and a translator that converts the Eiffel code into the language used by the Perfect Developer (PD) theorem prover. Preliminary experience indicates that the vast majority of verification conditions are quickly and automatically discharged, including loop variants and invariants. ES-Verify is the first automated Eiffel verification tool (to our knowledge) and allows the developer to use the clean syntax and object-oriented structures of Eiffel, together with its mature industrial strength design by contact mechanism.

Download paper in PDF format.

The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.