VAlloy – Virtual functions meet a relational language

Darko Marinov, Sarfraz Khurshid

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 modelling 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.

Original languageEnglish (US)
Title of host publicationFME 2002
Subtitle of host publicationFormal Methods - Getting IT Right - International Symposium of Formal Methods Europe, Proceedings
EditorsLars-Henrik Eriksson, Peter Alexander Lindsay
Number of pages18
ISBN (Electronic)9783540439288
StatePublished - 2002
Externally publishedYes
Event11th International Symposium of Formal Methods Europe, FME 2002 - Copenhagen, Denmark
Duration: Jul 22 2002Jul 24 2002

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other11th International Symposium of Formal Methods Europe, FME 2002

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'VAlloy – Virtual functions meet a relational language'. Together they form a unique fingerprint.

Cite this