VAlloy – Virtual functions meet a relational language

Darko Marinov; Sarfraz Khurshid

doi:10.1007/3-540-45614-7_14

VAlloy – Virtual functions meet a relational language

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 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 language	English (US)
Title of host publication	FME 2002
Subtitle of host publication	Formal Methods - Getting IT Right - International Symposium of Formal Methods Europe, Proceedings
Editors	Lars-Henrik Eriksson, Peter Alexander Lindsay
Publisher	Springer
Pages	234-251
Number of pages	18
ISBN (Electronic)	9783540439288
DOIs	https://doi.org/10.1007/3-540-45614-7_14
State	Published - 2002
Externally published	Yes
Event	11th International Symposium of Formal Methods Europe, FME 2002 - Copenhagen, Denmark Duration: Jul 22 2002 → Jul 24 2002

Publication series

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

Other

Other	11th International Symposium of Formal Methods Europe, FME 2002
Country/Territory	Denmark
City	Copenhagen
Period	7/22/02 → 7/24/02

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Online availability

10.1007/3-540-45614-7_14

Library availability

Discover UIUC Full Text

Cite this

Marinov, D., & Khurshid, S. (2002). VAlloy – Virtual functions meet a relational language. In L-H. Eriksson, & P. A. Lindsay (Eds.), FME 2002: Formal Methods - Getting IT Right - International Symposium of Formal Methods Europe, Proceedings (pp. 234-251). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2391). Springer. https://doi.org/10.1007/3-540-45614-7_14

VAlloy – Virtual functions meet a relational language. / Marinov, Darko; Khurshid, Sarfraz.

FME 2002: Formal Methods - Getting IT Right - International Symposium of Formal Methods Europe, Proceedings. ed. / Lars-Henrik Eriksson; Peter Alexander Lindsay. Springer, 2002. p. 234-251 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2391).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Marinov, D & Khurshid, S 2002, VAlloy – Virtual functions meet a relational language. in L-H Eriksson & PA Lindsay (eds), FME 2002: Formal Methods - Getting IT Right - International Symposium of Formal Methods Europe, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2391, Springer, pp. 234-251, 11th International Symposium of Formal Methods Europe, FME 2002, Copenhagen, Denmark, 7/22/02. https://doi.org/10.1007/3-540-45614-7_14

Marinov D, Khurshid S. VAlloy – Virtual functions meet a relational language. In Eriksson L-H, Lindsay PA, editors, FME 2002: Formal Methods - Getting IT Right - International Symposium of Formal Methods Europe, Proceedings. Springer. 2002. p. 234-251. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-45614-7_14

Marinov, Darko ; Khurshid, Sarfraz. / VAlloy – Virtual functions meet a relational language. FME 2002: Formal Methods - Getting IT Right - International Symposium of Formal Methods Europe, Proceedings. editor / Lars-Henrik Eriksson ; Peter Alexander Lindsay. Springer, 2002. pp. 234-251 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{624974ece6c04106a1eb9ea4489b27c3,

title = "VAlloy – Virtual functions meet a relational language",

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 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.",

author = "Darko Marinov and Sarfraz Khurshid",

year = "2002",

doi = "10.1007/3-540-45614-7_14",

language = "English (US)",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "234--251",

editor = "Lars-Henrik Eriksson and Lindsay, {Peter Alexander}",

booktitle = "FME 2002",

address = "Germany",

note = "11th International Symposium of Formal Methods Europe, FME 2002 ; Conference date: 22-07-2002 Through 24-07-2002",

}

TY - GEN

T1 - VAlloy – Virtual functions meet a relational language

AU - Marinov, Darko

AU - Khurshid, Sarfraz

PY - 2002

Y1 - 2002

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

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

UR - http://www.scopus.com/inward/record.url?scp=84873123944&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84873123944&partnerID=8YFLogxK

U2 - 10.1007/3-540-45614-7_14

DO - 10.1007/3-540-45614-7_14

M3 - Conference contribution

AN - SCOPUS:84873123944

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 234

EP - 251

BT - FME 2002

A2 - Eriksson, Lars-Henrik

A2 - Lindsay, Peter Alexander

PB - Springer

T2 - 11th International Symposium of Formal Methods Europe, FME 2002

Y2 - 22 July 2002 through 24 July 2002

ER -

VAlloy – Virtual functions meet a relational language

Abstract

Publication series

Other

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this