SE462:2007-07-23

SE462 Meeting of 23 July 2007

Alloy

• Everything in Alloy is a set of tuples. A basic datatype is a set of tuples.
• There are NO numbers in Alloy.
• ATOMS exist.. Scope {Book 0, Book 1, Book 2...

• Book = { (Book 0, Book 1, Book 2) }
• addr = { (Book 0, Name 1, Addr 2), (Book 0, Name 2, Addr 2) }
• names = { (Book 0, Name 0), (Book 0, Name 1), (Book 0, Name 2) }

Lab: 1

• Tutor - Scott
• Tues 1-3pm in Ground floor lab
• a) Exercise in relation types, b) What types to use
• Do exercise & WRITE UP a lab report, we will have a discussion on this in class.

Dot Operator

• b.addr => dot operator

first = {(Book 0)}

• n->t

{ (N0) } -> { (Addr0) } = { (N0, Addr0) }

Set Intersection

• Name & t

{ (N0), (N1), (N2) } & {(N0)} = {(N0)}

Set Difference a - b

{ (N0), (N1), (N2) } - {(N0)} = { (N1), (N2) }

Union a + b

{ (N0), (N1), (N2) } + {(N0)} = { (N0), (N1), (N2) }

Binary Relations

• Functional, Non injective
• Injective, Non fuctional
• Injective, Functional
• Non injective, Non functional

Domain & Range

• Domain = Right side of the relation
• Range = Left side of the relation

• For domain or range, we join on univ set
• Domain (rel) = rel.univ
• Range (rel) = univ.rel

• dot(join) . or [ ]
  • a.b is b[a]

Transitive Closure

• Given rel, ^rel is transitive closure

Reflective

• Given rel, *rel (includes iden)

Arithmetic

• Alloy can do SOME arithmetic
  • # a + # b > # c

• Integers are atoms.. 1,2,3,...

• Everything is a RELATION

Sbas022 15:22, 24 July 2007 (NZST)