Note: Language

16 Feb 2014

###4.1 An example: self-grandpas

###4.2 Signatures and Fields

####4.2.1 Signatures

• extends: extension or subsignature, mutually disjoint
• abstract: no elements of itself
• univ: can be viewed as an implicit abstract signature that all top-level signatures extend
• in: not necessarily mutually disjoint

• union of sets

    sig C in A + B {}
  

  the union is the only operator can appear in a sig declaration

• multiplicity keyword before sig

    m sig A {}
  

  enumeration

    abstract sig T {}
    one sig A, B, C extents T {}
  

####4.2.2 Basic Field Declarations

####4.2.3 Grouping Disjoint Fields

###4.4 Types and Type Checking

####4.4.1 Basic Types

####4.4.2 Relational Types

####4.4.3 Type Errors

####4.4.4 Field Overloading

---

###Questions:

1. P111 what exactly is overapproximation?
2. P113 Example alias?
3. all this: Course and some this: Course

---

###Notes during asgn 2

• I’ve never thought that we can use Alloy to model something like songs or lyrics. I guess it’s because sentence contains logic, and Alloy can model the logic.

###Feb 21 Class

• Alloy only runs within the scope, so it’s never exhaustive to the whole searching space. This should always be kept in mind.
• But, bugs tend to appear with smaller scope.(not always)

###Feb 24 Class

• seq vs order
• seq doc
• the existence of ++ operator

• override module name

    open util/ordering[Cats1] as trace1
    open util/ordering[Cats2] as trace2
  

###Feb 26 Class

####Skolemization

#####Skolem Depth:(my experiment)

• It counts all x: S| all y: S as one depth
• Same quantifiers in sequence is 1 depth
• top level is 0 depth

#####Useful for:

Debugging

#####Tradeoff:

Skolem	No	Yes
Constraints	Same	Less(some are shifted to Skolem variable)
Fields	Same	More(to represent some constraints)

###Note during asgn 3

• Don’t over-think things. Just follow the first instinct.
• The idea of representing infinity in Alloy is to be learned.