Sciweavers

Share
SIGSOFT
2008
ACM

Alchemy: transmuting base alloy specifications into implementations

9 years 11 months ago
Alchemy: transmuting base alloy specifications into implementations
Alloy specifications are used to define lightweight models of systems. We present Alchemy, which compiles Alloy specifications into implementations that execute against persistent databases. Alchemy translates a subset of Alloy predicates into imperative update operations, and it converts facts into database integrity constraints that it maintains automatically in the face of these imperative actions. In addition to presenting the semantics and an algorithm for this compilation, we present the tool and outline its application to a non-trivial specification. We also discuss lessons learned about the relationship between Alloy specifications and imperative implementations. Categories and Subject Descriptors I.2.2 [Artificial Intelligence]: Automatic Programming; H.2.3 [Database Management]: Languages General Terms Design, Languages Keywords Alloy, relational specification, program synthesis
Shriram Krishnamurthi, Kathi Fisler, Daniel J. Dou
Added 20 Nov 2009
Updated 20 Nov 2009
Type Conference
Year 2008
Where SIGSOFT
Authors Shriram Krishnamurthi, Kathi Fisler, Daniel J. Dougherty, Daniel Yoo
Comments (0)
books