Skip to main content
SpringerLink
Log in

VAlloy — Virtual Functions Meet a Relational Language

  • Conference paper
  • First Online:
FME 2002:Formal Methods—Getting IT Right (FME 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2391))

Included in the following conference series:

Abstract

We propose VAlloy, a veneer onto the first order, relational language Alloy. Alloy is suitable for modeling structural properties of object-oriented software. However, Alloy lacks support for dynamic dispatch, i.e., function invocation based on actual parameter types. VAlloy introduces virtual functions in Alloy, which enables intuitive modeling of inheritance. Models in VAlloy are automatically translated into Alloy and can be automatically checked using the existing Alloy Analyzer. We illustrate the use of VAlloy by modeling object equality, such as in Java. We also give specifications for a part of the Java Collections Framework.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J. Crawford, M. Ginsberg, E. Luks, and A. Roy. Symmetry-breaking predicates for search problems. In Proc. Fifth International Conference on Principles of Knowledge Representation and Reasoning, 1996.

    Google Scholar 

  2. Mukesh Dalal and Dipayan Gangopahyay. OOLP: A translation approach to object-oriented logic programming. In Proc. First International Conference on Deductive and Object-Oriented Databases (DOOD-89), pages 555–568, Kyoto, Japan, December 1989.

    Google Scholar 

  3. Michael D. Ernst. Dynamically Discovering Likely Program Invariants. PhD thesis, University of Washington Department of Computer Science and Engineering, Seattle, Washington, August 2000.

    Google Scholar 

  4. Marieke Huisman, Bart Jacobs, and Joachim van den Berg. A case study in class library verification: Java’s Vector class. Software Tools for Technology Transfer, 2001.

    Google Scholar 

  5. Daniel Jackson. Micromodels of software: Modelling and analysis with Alloy, 2001. Available online: http://sdg.lcs.mit.edu/alloy/book.pdf.

  6. Daniel Jackson. Alloy: A lightweight object modeling notation. ACM Transactions on Software Engineering and Methodology, 2002. (to appear).

    Google Scholar 

  7. Daniel Jackson and Alan Fekete. Lightweight analysis of object interactions. In Proc. Fourth International Symposium on Theoretical Aspects of Computer Software, Sendai, Japan, October 2001.

    Google Scholar 

  8. Daniel Jackson, Ian Schechter, and Ilya Shlyakhter. ALCOA: The Alloy constraint analyzer. In Proc. 22nd International Conference on Software Engineering (ICSE), Limerick, Ireland, June 2000.

    Google Scholar 

  9. Daniel Jackson, Ilya Shlyakhter, and Manu Sridharan. A micromodularity mechanism. In Proc. 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), Vienna, Austria, September 2001.

    Google Scholar 

  10. Daniel Jackson and Mandana Vaziri. Finding bugs with a constraint solver. In Proc. International Symposium on Software Testing and Analysis (ISSTA), Portland, OR, August 2000.

    Google Scholar 

  11. Idit Keidar, Roger Khazan, Nancy Lynch, and Alex Shvartsman. An inheritance-based technique for building simulation proofs incrementally. In Proc. 22nd International Conference on Software Engineering (ICSE), pages 478–487, Limerick, Ireland, June 2000.

    Google Scholar 

  12. Sarfraz Khurshid, Darko Marinov, and Daniel Jackson. An analyzable annotation language. In Proc. ACM SIGPLAN 2002 Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA), Seattle, WA, Nov 2002.

    Google Scholar 

  13. Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report TR 98-06i, Department of Computer Science, Iowa State University, June 1998. (last revision: Aug 2001).

    Google Scholar 

  14. Barbara Liskov. Program Development in Java: Abstraction, Specification, and Object-Oriented Design. Addison-Wesley, 2000.

    Google Scholar 

  15. Nancy Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, 1996.

    Google Scholar 

  16. Darko Marinov and Sarfraz Khurshid. TestEra: A novel framework for automated testing of Java programs. In Proc. 16th IEEE International Conference on Automated Software Engineering (ASE), San Diego, CA, November 2001.

    Google Scholar 

  17. Chris Moss. Prolog++ The Power of Object-Oriented and Logic Programming. Addison-Wesley, 1994.

    Google Scholar 

  18. Mark Roulo. How to avoid traps and correctly override methods from java.lang.Object. http://www.javaworld.com/javaworld/jw-01-1999/jw-01-object.html.

  19. Ilya Shlyakhter. Generating effective symmetry-breaking predicates for search problems. In Proc. Workshop on Theory and Applications of Satisfiability Testing, June 2001.

    Google Scholar 

  20. G. Smith. The Object-Z Specification Language. Kluwer Academic Publishers, 2000.

    Google Scholar 

  21. J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, second edition, 1992.

    Google Scholar 

  22. Sun Microsystems. Java 2 Platform, Standard Edition, v1.3.1 API Specification. http://java.sun.com/j2se/1.3/docs/api/.

  23. Joachim van den Berg and Bart Jacobs. The LOOP compiler for Java and JML. In Proc. Tools and Algorithms for the Construction and Analysis of Software (TACAS), (Springer LNCS 2031, 2001), pages 299–312, Genoa, Italy, April 2001.

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. MIT Laboratory for Computer Science, 200 Technology Square, Cambridge, MA, 02139, USA

    Darko Marinov & Sarfraz Khurshid

Authors
  1. Darko Marinov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sarfraz Khurshid
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Information Technology, Uppsala University, P.O. Box 337, 751 05, Uppsala, Sweden

    Lars-Henrik Eriksson

  2. Software Verification Research Centre, The University of Queensland, Queensland, 4072, Australia

    Peter Alexander Lindsay

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Marinov, D., Khurshid, S. (2002). VAlloy — Virtual Functions Meet a Relational Language. In: Eriksson, LH., Lindsay, P.A. (eds) FME 2002:Formal Methods—Getting IT Right. FME 2002. Lecture Notes in Computer Science, vol 2391. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45614-7_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-45614-7_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43928-8

  • Online ISBN: 978-3-540-45614-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation