We present a modified semantics and an extension of the Alloy specification language. The results presented in this paper are: (a) We show how the modified semantics of Alloy allows us to avoid the higher-order quantification currently used both in the composition of operations and in specifications, keeping the language first-order. (b) We show how the extended language, which includes features from dynamic logic, enables a cleaner (with respect to previous papers) treatment of properties of executions. (c) We show that the automatic analysis currently available for Alloy specifications can be fully applied in the analysis of specifications under the new semantics. (d) We present a calculus for the extended language that is complete with respect to the extended semantics. This allows us to complement the analysis currently provided in Alloy with theorem proving. (e) Finally, we show how to use the theorem prover PVS in order to verify Alloy specifications.
%0 Book Section
%1 frias_03_taking
%A Frias, Marcelo
%A Pombo, Carlos L.
%A Baum, Gabriel
%A Aguirre, Nazareno
%A Maibaum, Tom
%D 2003
%J FME 2003: Formal Methods
%K _hardcopy pvs semantics alloy 2003 _no_doi
%P 678--697
%T Taking Alloy to the Movies
%U http://www.springerlink.com/content/a0dlgtdppbnnr83w
%X We present a modified semantics and an extension of the Alloy specification language. The results presented in this paper are: (a) We show how the modified semantics of Alloy allows us to avoid the higher-order quantification currently used both in the composition of operations and in specifications, keeping the language first-order. (b) We show how the extended language, which includes features from dynamic logic, enables a cleaner (with respect to previous papers) treatment of properties of executions. (c) We show that the automatic analysis currently available for Alloy specifications can be fully applied in the analysis of specifications under the new semantics. (d) We present a calculus for the extended language that is complete with respect to the extended semantics. This allows us to complement the analysis currently provided in Alloy with theorem proving. (e) Finally, we show how to use the theorem prover PVS in order to verify Alloy specifications.
@incollection{frias_03_taking,
abstract = {We present a modified semantics and an extension of the Alloy specification language. The results presented in this paper are: (a) We show how the modified semantics of Alloy allows us to avoid the higher-order quantification currently used both in the composition of operations and in specifications, keeping the language first-order. (b) We show how the extended language, which includes features from dynamic logic, enables a cleaner (with respect to previous papers) treatment of properties of executions. (c) We show that the automatic analysis currently available for Alloy specifications can be fully applied in the analysis of specifications under the new semantics. (d) We present a calculus for the extended language that is complete with respect to the extended semantics. This allows us to complement the analysis currently provided in Alloy with theorem proving. (e) Finally, we show how to use the theorem prover PVS in order to verify Alloy specifications.},
added-at = {2009-02-11T22:25:47.000+0100},
author = {Frias, Marcelo and Pombo, Carlos L. and Baum, Gabriel and Aguirre, Nazareno and Maibaum, Tom},
biburl = {https://www.bibsonomy.org/bibtex/25dc2fa414faab452a513b1dd7ae11d99/leonardo},
citeulike-article-id = {1569396},
interhash = {210309a7703e8dbc4133e3abdcea3863},
intrahash = {5dc2fa414faab452a513b1dd7ae11d99},
journal = {FME 2003: Formal Methods},
keywords = {_hardcopy pvs semantics alloy 2003 _no_doi},
pages = {678--697},
posted-at = {2007-10-26 00:55:39},
priority = {3},
timestamp = {2009-02-11T22:25:47.000+0100},
title = {Taking Alloy to the Movies},
url = {http://www.springerlink.com/content/a0dlgtdppbnnr83w},
year = 2003
}