UNM CS 580 - CS 580 LECTURE NOTES (36 pages)

Previewing pages 1, 2, 17, 18, 19, 35, 36 of 36 page document View the full content.
View Full Document

CS 580 LECTURE NOTES



Previewing pages 1, 2, 17, 18, 19, 35, 36 of actual document.

View the full content.
View Full Document
View Full Document

CS 580 LECTURE NOTES

64 views

Other


Pages:
36
School:
University of New Mexico
Course:
Cs 580 - The Specification of Software Systems

Unformatted text preview:

CS 580 Alloy Tutorial Session 2 Language and Analysis Greg Dennis and Rob Seater Software Design Group MIT Used and modified with permission by Robert Stehwien alloy language analysis language syntax for structuring specifications in logic shorthands puns sugar analysis tool for finding solutions to logical formulas searches for and visualizes counterexamples I m My Own Grandpa Song popular radio skit originally written in the 1930 s expanded into hit song by Lonzo and Oscar in 1948 I m My Own Grandpa in Alloy module examples tutorial grandpa abstract sig Person father lone Man mother lone Woman assert noSelfFather no m Man m m father check noSelfFather sig Man extends Person wife lone Woman fun grandpas p Person set Person p mother father father sig Woman extends Person husband lone Man pred ownGrandpa p Person p in grandpas p fact no p Person p in p mother father wife husband run ownGrandpa for 4 Person language module header module examples tutorial grandpa first non comment of an Alloy model saved as examples tutorial grandpa als relative to Alloy Analyzer s models directory language signatures sig A set of atoms A sig A sig B disjoint sets A and B no A B abstract sig A sig B extends A sig C extends A A partitioned by disjoint subsets B and C no B C A B C sig A B same as above sig B in A B is a subset of A not necessarily disjoint from any other set sig B extends A set B is a subset of A B in A sig C in A B C is a subset of the union of A and B sig B extends A sig C extends A B and C are disjoint subsets of A B in A C in A no B C one sig A lone sig B some sig C A is a singleton set B is a singleton or empty C is a non empty set sig B C extends A same as above grandpa signatures abstract sig Person sig Man extends Person sig Woman extends Person all men and women are persons no person is both a man and a woman all persons are either men or women language fields sig A f e f is a binary relation with domain A and range given by expression e f is constrained to be a



View Full Document

Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view CS 580 LECTURE NOTES and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view CS 580 LECTURE NOTES and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?