Paper Info
Title
Alchemy: transmuting base alloy specifications into implementations
Abstract
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.
Year
DOI
Venue
2008
10.1145/1453101.1453123
SIGSOFT FSE
Keywords
Field
DocType
imperative update operation,persistent databases,alchemy translates,alloy predicate,lightweight model,imperative implementation,non-trivial specification,transmuting base alloy specification,imperative action,database integrity constraint,alloy specification
Programming language,Program synthesis,Computer science,Alchemy,Implementation,Data integrity,Predicate (grammar),Semantics
Conference
Citations 
PageRank 
References 
10
0.66
24
Authors
4
Name
Order
Citations
PageRank
Shriram Krishnamurthi12446178.81
Kathi Fisler288258.08
Daniel J. Dougherty341332.13
Daniel Yoo411822.61