From Relational Specifications to Logic Programs

This paper presents a compiler from expressive, relational specifications to logic programs. Specifically, the compiler translates the Imperative Alloy specification language to Prolog. Imperative Alloy is a declarative, relational specification language based on first-order logic and extended with imperative constructs; Alloy specifications are traditionally not executable. In spite of this theoretical limitation, the compiler produces useful prototype implementations for many specifications.

• Type: Conference
• Year: 2010
• Where: ICLP
• Authors: Joseph P. Near
• Keywords: Automated Reasoning, ICLP 2010, Imperative Alloy, Imperative Alloy Specification, Relational Specification