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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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.
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.
Michael D. Ernst. Dynamically Discovering Likely Program Invariants. PhD thesis, University of Washington Department of Computer Science and Engineering, Seattle, Washington, August 2000.
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.
Daniel Jackson. Micromodels of software: Modelling and analysis with Alloy, 2001. Available online: http://sdg.lcs.mit.edu/alloy/book.pdf.
Daniel Jackson. Alloy: A lightweight object modeling notation. ACM Transactions on Software Engineering and Methodology, 2002. (to appear).
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.
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.
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.
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.
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.
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.
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).
Barbara Liskov. Program Development in Java: Abstraction, Specification, and Object-Oriented Design. Addison-Wesley, 2000.
Nancy Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, 1996.
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.
Chris Moss. Prolog++ The Power of Object-Oriented and Logic Programming. Addison-Wesley, 1994.
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.
Ilya Shlyakhter. Generating effective symmetry-breaking predicates for search problems. In Proc. Workshop on Theory and Applications of Satisfiability Testing, June 2001.
G. Smith. The Object-Z Specification Language. Kluwer Academic Publishers, 2000.
J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, second edition, 1992.
Sun Microsystems. Java 2 Platform, Standard Edition, v1.3.1 API Specification. http://java.sun.com/j2se/1.3/docs/api/.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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