Re: What databases have taught me

From: erk <>
Date: 28 Jun 2006 12:22:41 -0700
Message-ID: <>

Bob Badour wrote:
> Perhaps it was not Alloy that I was looking at. Or perhaps it was just > my unfamiliarity with the syntax.

I'll just regurgitate a brief example, since we're on the topic. Note that within a sig, each named attribute establishes a relation with that name, from the "containing" sig to the domain of its type (Reinforces my belief that Date was right - encapsulation is a red herring.) So despite the "objecty" syntax later, it's all relations (from sig to sig - you define and constrain the sets), and you can treat them as such.

Modifiers like "lone", and the "fact" predicates, all establish constraints on the relations. "extends" is subtyping with the expected subset relationship.

The "check" commands simply run Alloy to find a counterexample - given the constraints you've specified, see whether any models violate the assertions you've made.

// A file system object in the file system
sig FSObject {
  parent: lone Dir

// A directory in the file system

sig Dir extends FSObject {
  contents: set FSObject

// A directory is the parent of its contents
fact defineContents {
  all d: Dir, o: d.contents | o.parent = d }

// A file in the file system

sig File extends FSObject {}

// All file system objects are either files or directories
fact fileDirPartition {
  File + Dir = FSObject

// There exists a root

one sig Root extends Dir {
  no parent

// File system is connected

fact fileSystemConnected {
  FSObject in Root.*contents

// The contents path is acyclic

assert acyclic {
  no d: Dir | d in d.^contents

check acyclic for 5

// File system has one root

assert oneRoot {
  one d: Dir | no d.parent

check oneRoot for 5

// Every fs object is in at most one directory
assert oneLocation {
  all o: FSObject | lone d: Dir | o in d.contents }

check oneLocation for 5 Received on Wed Jun 28 2006 - 21:22:41 CEST

Original text of this message