OCL challenge



Date view Thread view Subject view Author view

Daniel Jackson (dnj@lcs.mit.edu)
Tue, 5 Dec 2000 11:59:15 -0500


dear PUML-ers, i'm writing a paper about object models of code. it's about how to give semantics to object models, paying special attention to issues that arise when modelling the heap of a program. i'd like to understand how my examples would look in OCL, and i fear that my critique of OCL may be coloured by my lack of expertise. would someone like to give me some help writing OCL constraints? the example is given below in Alloy, my own language. it's very simple. there's a standard list structure (a class List with subclasses EmptyList and NonEmptyList, with the former having a reference to an element and the next List cell), and a class Map that holds a List, and a class Pair that some Lists hold as elements. the constraints i want to write are: // no Lists that belong to different Maps overlap // Lists contained in Maps have Pairs as their elements // Lists contained in Maps do not hold null references as elements // no object is both a key of some Pair and a val of some Pair // Lists do not contain duplicates // no cyclic Lists // no List contains itself as an element // no List contains a List as an element // there is only one EmptyList object visual form of OM attached. it's not clear exactly how to draw this, since not all Lists contain Pairs, but the Lists contained by Maps do. one of the issues my paper addresses is how to make solve this problem, so thoughts on that also welcome. /daniel model Lists { domain {Object} state { disjoint Map, List, Pair: Object partition EmptyList, NonEmptyList: List list: Map? -> List! next: NonEmptyList -> List! elt: NonEmptyList -> Object? key, val: Pair -> Object? } inv { // no Lists that belong to different Maps overlap no m1, m2: Map - m1 | some (m1.list.*next & m2.list.*next) // Lists contained in Maps have Pairs as their elements Map.list.*next.elt in Pair // Lists contained in Maps do not hold null references as elements all p: Map.list.*next & NonEmptyList | some p.elt // no object is both a key of some Pair and a val of some Pair no Pair.key & Pair.val // Lists do not contain duplicates all p: List, o: Object | sole o & p.*next.elt // no cyclic Lists all p: List | p !in p.+next // no List contains itself as an element no p: List | p in p.*next.elt // no List contains a List as an element no List & List.elt // there is only one EmptyList object one EmptyList } } -------------------------------------------------- Daniel Jackson Associate Professor, Computer Science Massachusetts Institute of Technology http://sdg.lcs.mit.edu/~dnj


Date view Thread view Subject view Author view