An EVES data abstraction example

  • Mark Saaltink
  • Sentot Kromodimoeljo
  • Bill Pase
  • Dan Craigen
  • Irwin Meisels
Part of the Lecture Notes in Computer Science book series (LNCS, volume 670)


This paper provides an introduction to EVES. EVES is a formal methods tool consisting of a language based on set theory, called Verdi, and an automated deduction system, called NEVER. We provide a general introduction to EVES and demonstrate its capabilities using an example of data abstraction (table/list).


Proof Obligation Automate Deduction Current Element Abstract Data Type Abstraction Function 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    W.W. Bledsoe, P. Bruell: A man-machine theorem proving system. Artificial Intelligence 5(1):51–72, 1974.Google Scholar
  2. 2.
    R.S. Boyer, J.S. Moore: A Computational Logic. Academic Press, NY, 1979.Google Scholar
  3. 3.
    Dan Craigen: Reference Manual for the Language Verdi. ORA Canada Technical Report TR-91-5429-09a, September 1991.Google Scholar
  4. 4.
    C.A.R. Hoare: Proof of Correctness of Data Representations. Acta Informatica 1: 271–281, 1972.CrossRefGoogle Scholar
  5. 5.
    Sentot Kromodimoeljo, Bill Pase: Using the EVES Library Facility: A PICO Interpreter. ORA Canada Technical Report TR-90-5444-02, February, 1990.Google Scholar
  6. 6.
    Sentot Kromodimoeljo, Bill Pase: Final Report for the Investigation of Proof Techniques Within the EVES Verification Technology. ORA Canada Technical Report FR-92-5451-02, May 1992.Google Scholar
  7. 7.
    Sentot Kromodimoeljo, Bill Pase: Development of a Skeletal CSP Theory in EVES. ORA Canada Technical Report TR-92-5469-02, July 1992.Google Scholar
  8. 8.
    Sentot Kromodimoeljo, Bill Pase: Investigating the Role of EVES in System Engineering and Security Evaluation. ORA Canada Technical Report TR-92-5464-02, September 1992.Google Scholar
  9. 9.
    D.C. Luckham, et al.: Stanford Pascal verifier user manual. Technical Report STAN-CS-79-731, Stanford U. Computer Science Dept., March 1979.Google Scholar
  10. 10.
    Dave Parnas and W. Bartussek: Using Traces to Write Abstract Specifications for Software Modules. Information Systems Methodology, Proceedings of ICS, Lecture Notes in Computer Science (65), Springer-Verlag, 1978.Google Scholar
  11. 11.
    Dave Parnas, David Smith, Trevor Pearce: Making Formal Software Documentation More Practical: A Progress Report. Technical Report 88-236, Department of Computing and Information Science, Queen's University at Kingston, November, 1988.Google Scholar
  12. 12.
    Bill Pase, Sentot Kromodimoeljo: A User's Guide to a Skeletal CSP Theory in EVES. ORA Canada Technical Report TR-92-5469-03, July 1992.Google Scholar
  13. 13.
    Mark Saaltink: A Formal Description of Verdi. ORA Canada Technical Report TR-89-5429-10, October, 1989.Google Scholar
  14. 14.
    Mark Saaltink: Alternative Semantics for Verdi. ORA Canada Technical Report TR-90-5446-02, November, 1990.Google Scholar
  15. 15.
    Mark Saaltink: Z and EVES. ORA Canada Technical Report TR-91-5449-02. (An abridged version is in the Proceedings of the 6th annual Z Users Meeting, Springer Verlag.)Google Scholar
  16. 16.
    Mark Saaltink: The EVES Library. ORA Canada Technical Report TR-91-5449-03.Google Scholar
  17. 17.
    Mark Saaltink: The EVES Library Models. ORA Canada Technical Report TR-91-5449-04.Google Scholar
  18. 18.
    Mark Saaltink and Dan Craigen: Simple Type Theory in EVES. Proceedings of the 4th Workshop on Higher Order Logic, G. Birtwistle, editor. Springer Verlag, 1991.Google Scholar
  19. 19.
    J.M. Spivey: The Z Notation: A Reference Manual. Prentice Hall, 1987.Google Scholar
  20. 20.
    D.H. Thompson, R.W. Erickson (eds.): AFFIRM Reference Manual, USC Information Sciences Institute. Marina Dey Ray, CA, 1981.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Mark Saaltink
    • 1
  • Sentot Kromodimoeljo
    • 1
  • Bill Pase
    • 1
  • Dan Craigen
    • 1
  • Irwin Meisels
    • 1
  1. 1.ORA CanadaOttawaCanada

Personalised recommendations