Student Work

 

Towards a Transition System Semantics for Alloy Public

Downloadable Content

open in viewer

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.

Creator
Publisher
Identifier
  • E-project-031609-013504
Advisor
Year
  • 2009
Date created
  • 2009-03-16
Resource type
Major
Rights statement
License

Relationships

In Collection:

Items

Permanent link to this page: https://digital.wpi.edu/show/qj72p859m