Alloy is a language for modeling systems using first order logic and relational algebra. In this paper we examine the use of Alloy for creating models of stateful systems, and we explore semantics for Alloy that define transition systems over database instances based on Alloy specifications written in the state-signature idiom. One such semantics is fully adequate for the original semantics of Alloy. We prove an undecidability result concerning the automatic synthesis of programs from specifications under this semantics.

• This report represents the work of one or more WPI undergraduate students submitted to the faculty as evidence of completion of a degree requirement. WPI routinely publishes these reports on its website without editorial or peer review.

Creator

• Giannakopoulos, Theophilos John

Publisher

• Worcester Polytechnic Institute

Identifier

• E-project-031609-013504

Advisor

• Dougherty, Daniel J.

Year

• 2009

Date created

• 2009-03-16

Resource type

• Major Qualifying Project

Major

• Computer Science

Rights statement

• In Copyright

License

• All rights reserved