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.

REFERENCES

• 1: J.-R. Abrial, The B-book: assigning programs to meanings, Cambridge University Press, New York, NY, 1996
• 2: Antonio Albano , Luca Cardelli , Renzo Orsini, GALILEO: a strongly-typed, interactive conceptual language, ACM Transactions on Database Systems (TODS), v.10 n.2, p.230-260, June 1985 [doi>10.1145/3857.3859]
• 3: Joseph L. Bates , Robert L. Constable, Proofs as programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.1, p.113-136, Jan. 1985 [doi>10.1145/2363.2528]
• 4: F. Bouquet, F. Dadeau, B. Legeard, and M. Utting. Symbolic animation of JML specifications. In International Symposium of Formal Methods Europe, 2005.
• 5: R. M. Burstall , John Darlington, A Transformation System for Developing Recursive Programs, Journal of the ACM (JACM), v.24 n.1, p.44-67, Jan. 1977 [doi>10.1145/321992.321996]
• 6: Stefano Ceri , Piero Fraternali , Stefano Paraboschi , Letizia Tanca, Automatic generation of production rules for integrity maintenance, ACM Transactions on Database Systems (TODS), v.19 n.3, p.367-422, Sept. 1994 [doi>10.1145/185827.185828]
• 7: Stefano Ceri , Jennifer Widom, Deriving incremental production rules for deductive data, Information Systems, v.19 n.6, p.467-490, Sept. 1994 [doi>10.1016/0306-4379(94)90002-7]
• 8: Brian Demsky , Martin Rinard, Automatic detection and repair of errors in data structures, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 9: Robert Bruce Findler , John Clements , Cormac Flanagan , Matthew Flatt , Shriram Krishnamurthi , Paul Steckler , Matthias Felleisen, DrScheme: a programming environment for Scheme, Journal of Functional Programming, v.12 n.2, p.159-182, March 2002 [doi>10.1017/S0956796801004208]
• 10: Marcelo F. Frias , Carlos G. López Pombo , Gabriel A. Baum , Nazareno M. Aguirre , Thomas S. E. Maibaum, Reasoning about static and dynamic properties in alloy: A purely relational approach, ACM Transactions on Software Engineering and Methodology (TOSEM), v.14 n.4, p.478-526, October 2005 [doi>10.1145/1101815.1101819]
• 11: R. Gheyi, T. Massoni, and P. Borba. Formally introducing Alloy idioms. In Brazilian Symposium on Formal Methods, 2007.
• 12: C. C. Green. Application of theorem proving to problem solving. In International Joint Conference on Artificial Intelligence, 1969.
• 13: Michael Hammer , Brian Berkowitz, DIAL: a programming language for data intensive applications, Proceedings of the 1980 ACM SIGMOD international conference on Management of data, May 14-16, 1980, Santa Monica, California [doi>10.1145/582250.582263]
• 14: Michael Hammer , Dennis McLeod, The semantic data model: a modelling mechanism for data base applications, Proceedings of the 1978 ACM SIGMOD international conference on management of data, May 31-June 02, 1978, Austin, Texas [doi>10.1145/509252.509264]
• 15: Daniel Hazel , Paul Strooper , Owen Traynor, Possum: An Animator for the SUM Specification Language, Proceedings of the Fourth Asia-Pacific Software Engineering and International Computer Science Conference, p.42, December 02-05, 1997
• 16: Daniel Jackson, Automating first-order relational logic, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.130-139, November 06-10, 2000, San Diego, California, United States
• 17: D. Jackson. Software Abstractions. MIT Press, 2006.
• 18: D. Jackson and J. Wing. Lightweight formal methods. IEEE Computer, Apr. 1996.
• 19: Zohar Manna , Richard Waldinger, A Deductive Approach to Program Synthesis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.90-121, Jan. 1980 [doi>10.1145/357084.357090]
• 20: William W. McCune , Lawrence J. Henschen, Maintaining state constraints in relational databases: a proof theoretic basis, Journal of the ACM (JACM), v.36 n.1, p.46-68, Jan. 1989 [doi>10.1145/58562.59302]
• 21: J. McDonald and J. Anton. SPECWARE - producing software correct by construction. Technical Report KES.U.01.3, Kestrel Institute, Mar. 2001.
• 22: Stephen J. Mellor , Marc Balcer , Ivar Jacoboson, Executable UML: A Foundation for Model-Driven Architectures, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2002
• 23: Sergey Melnik , Atul Adya , Philip A. Bernstein, Compiling mappings to bridge applications and databases, Proceedings of the 2007 ACM SIGMOD international conference on Management of data, June 11-14, 2007, Beijing, China [doi>10.1145/1247480.1247532]
• 24: T. Miller, L. Freitas, P. Malik, and M. Utting. CZT support for Z extensions. In International Conference on Integrated Formal Methods, 2005.
• 25: Christian Nentwich , Wolfgang Emmerich , Anthony Finkelstein, Consistency management with repair actions, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
• 26: L. V. Orman, Transaction Repair for Integrity Enforcement, IEEE Transactions on Knowledge and Data Engineering, v.13 n.6, p.996-1009, November 2001 [doi>10.1109/69.971192]
• 27: Alan J. Perlis, Special Feature: Epigrams on programming, ACM SIGPLAN Notices, v.17 n.9, p.7-13, September 1982 [doi>10.1145/947955.1083808]
• 28: Charles Rich , Richard C. Waters, Automatic Programming: Myths and Prospects, Computer, v.21 n.8, p.40-51, August 1988 [doi>10.1109/2.75]
• 29: Douglas R. Smith, Top-down synthesis of divide-and-conquer algorithms, Artificial Intelligence, v.27 n.1, p.43-96, Sept. 1985 [doi>10.1016/0004-3702(85)90083-9]
• 30: David Stemple , Subhasish Mazumdar , Tim Sheard, On the modes and meaning of feedback to transaction designers, ACM SIGMOD Record, v.16 n.3, p.374-386, Dec. 1987
• 31: Helene Waeselynck , Salimeh Behnia, B Model Animation for External Verification, Proceedings of the Second IEEE International Conference on Formal Engineering Methods, p.36, December 09-11, 1998
• 32: R. J. Waldinger and R. C. T. Lee. PROW: A step toward automatic program writing. In International Joint Conference on Artificial Intelligence, 1969.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming

Additional Classification:
  H. Information Systems
  H.2 DATABASE MANAGEMENT
      H.2.3 Languages

General Terms:
Design, Languages

Keywords:
alloy, program synthesis, relational specification