RE: OCL challenge



Date view Thread view Subject view Author view

Daniel Jackson (dnj@lcs.mit.edu)
Mon, 11 Dec 2000 21:10:54 -0500


mark, 1. flattening thanks for your explanation about flattening. yes, i see that seq->asSet should not be called flattening. sorry also for the stupid comment about implicit flattening in general. btw, i've been reading your ER98 paper and trying to figure out the consequences of not having implicit flattening OCL-style. does it mean that if i have two relations, p and q say, then i can't write the navigation x.p.q if p is not a function? 2. undefinedness it seems to me that a great advantage of having a scheme based on relational image (as in Alloy) is that you don't have to worry about these issues: the meaning of x.p.q when x.p is empty is just the empty set. but perhaps you need it because you have a higher-order expression language? or is it because you allow integer-valued attributes, so x.p might be expected to be an integer? 3. operations do you think OCL really benefits from having operations? they seem to me very complicated: non-termination, as you explain it, really means that the constraint you wrote down doesn't have the meaning you might expect. also it's a pity that they make OCL non-declarative. why not just include transitive closure? do you have examples that need operations? 4. static typing ....Your Alloy specification really looks nicer and more ....concise for this ....model. But I wonder, whether your approach to the typing issue is ....still manageable in context of large specifications. For example, we ....have translated the UML 1.3 metamodel together with the ....well-formedness rules into a USE specification. The specification ....contains 151 invariants and 41 additional operations some ....of which are ....quite complex. A large number of type errors could be found with our ....tool thanks to the strong type checking rules of OCL (details are in ....our UML'2000 paper). How are your experiences with larger Alloy ....specifications? well first, i'll have to say that we haven't written many big Alloy specs. our focus has been more on doing analysis. we've found that even with small specs (less than 200 lines say) we can do some interesting things. my student Sarfraz Khurshid found serious flaws in the design of a resource discovery service, and used Alloy to design a fix. recently, we've been working on Alloy specs of routing protocols that propagate topology changes -- ideal for object modelling, since model checkers don't handle changing topologies well. we're actually in the process of completing the design of a new version of Alloy with proper structuring mechanisms. we've been at it for about a year, and expect to implement it in the next few months. i've been delaying it because i wanted to make sure we had a very small language, and all my initial attempts ended up looking like a C++ of modelling languages. we also have generally followed the principle of only making expressible things we can do full analysis on, but now, thanks to advances in our engine by my student Ilya Shlyakhter, we can handle bigger things. we expect to add arbitrary arity relations, as in your OCL semantics, but we won't have any truly higher-order datatypes. we also translated the UML metamodel, and ran it through our analyzer. the analyzer demonstrated its consistency, and showed us, by generating some bogus UML models, that we didn't have enough constraints -- probably because there all kinds of constraints implicit in UML that we didn't include. fyi, i'm appending our Alloy version of the constraints below (done by my student Mandana Vaziri). regards, /daniel model uml-core{ domain {Element, Name, AssociationClassDom, IndexDom } state{ ModelElement: Element //ModelElement attributes name: ModelElement! -> Name! //associationClass ElementOwnership ElementOwnership: AssociationClassDom elementOwnership_private: ElementOwnership elementOwnership_protected: ElementOwnership //no need for public elementOwnership: ModelElement -> ElementOwnership! Relationship: ModelElement+ Association: Relationship+ AssociationEnd: ModelElement+ //AssociationEnd attributes aggregation: AssociationEnd composition: AssociationEnd //no need for none isNavigable: AssociationEnd multiplicity_max1: AssociationEnd name1: AssociationEnd -> Name //No Constraints on this //Needed for translation. Namespace: ModelElement+ Feature: ModelElement+ //Attributes of Feature feature_private : Feature feature_protected: Feature StructuralFeature: Feature+ Attribute: StructuralFeature+ BehavioralFeature: Feature+ //BehavioralFeature attributes isQuery: BehavioralFeature //BehavioralFeature operation hasSameSignature: BehavioralFeature -> BehavioralFeature Operation: BehavioralFeature+ Method: BehavioralFeature+ GeneralizableElement: ModelElement+ // GeneralizableElement attributes isRoot: GeneralizableElement isLeaf: GeneralizableElement isAbstract: GeneralizableElement // GeneralizableElement operations parent: GeneralizableElement -> GeneralizableElement allParents: GeneralizableElement -> GeneralizableElement Parameter: ModelElement+ Index: IndexDom+ //Index relation same: Index -> Index Constraint: ModelElement+ UseCase: ModelElement+ Collaboration: ModelElement+ Dependency: Relationship+ Classifier: GeneralizableElement+ //Classifier operations parentClassifier: Classifier -> Classifier allFeatures: Classifier -> Feature allOperations: Classifier -> Operation allMethods: Classifier -> Method allContents: Classifier -> ModelElement associations: Classifier -> Association oppositeAssociationEnds: Classifier -> AssociationEnd allOppositeAssociationEnds: Classifier -> AssociationEnd allAttributes: Classifier -> Attribute specification: Classifier -> Classifier Class: Classifier+ //Class attribute AssociationClass: ModelElement+ //AssociationClass operations parentAssociation: AssociationClass -> Association allConnections: AssociationClass -> AssociationEnd Generalization: Relationship+ //Generalization Attribute discriminator: Generalization -> Name Interface: Classifier+ DataType: Classifier+ Component: Classifier+ //Component operations parentComponent: Component -> Component allResidentElements: Component -> ModelElement //Association class between Component and ModelElement ElementResidence: AssociationClassDom component: ElementResidence -> Component? modelElement(~elementResidence): ElementResidence -> ModelElement? elementResidence_private: ElementResidence elementResidence_protected: ElementResidence // Relationships connection(~association): Association! -> AssociationEnd+ namespace(~ownedElement): ModelElement -> Namespace? type(~associationEnd): AssociationEnd -> Classifier! ptype: Parameter -> Classifier! feature(~owner): Classifier! -> Feature specialization(~parent1): GeneralizableElement! -> Generalization generalization(~child): GeneralizableElement! -> Generalization index: BehavioralFeature? -> Index parameter: Index? -> Parameter? //specification: Method -> Operation! powertypeRange: Classifier? -> Generalization constrainedElement: Constraint -> ModelElement+ resident: Component -> ModelElement } // OPERATION DEFINITIONS cond GeneralizableElementOp { //Definition of parent all e: GeneralizableElement | e.parent = e.generalization.parent1 //Definition of allParents all e: GeneralizableElement | e.allParents = e.+parent } cond AssociationClassOp{ //include operations GeneralizableElementOp //Definition of allConnections all a: AssociationClass | a.allConnections = a.+parent.connection } cond BehavioralFeatureOp{ all b1, b2: BehavioralFeature | b1.index != b2.index all b: BehavioralFeature | all i: b.index | some i.parameter //Definition of same - equivalence relation all i: Index | i in i.same all i1, i2: Index | i1 in i2.same -> i2 in i1.same all i1, i2, i3: Index | i1 in i2.same && i2 in i3.same -> i1 in i3.same //Definition of hasSameSignature all b: BehavioralFeature | b.hasSameSignature = {b1: BehavioralFeature | b.name = b1.name && b1.index in b.index.same && b.index in b1.index.same && (all i: b.index | all i1: b1.index | i1 in i.same -> i.parameter.ptype = i1.parameter.ptype)} } cond ClassifierOp{ //include operations GeneralizableElementOp all c: Classifier | c.parentClassifier = c.parent & Classifier //Definition of allFeatures all c: Classifier | c.allFeatures = c.+parentClassifier.feature //Definition of allOperations all c: Classifier | c.allOperations = c.allFeatures & Operation //Definition of allMethods all c: Classifier | c.allMethods = c.allFeatures & Method //Definition of allContents all c: Classifier | c.allContents = c.+parentClassifier.ownedElement & {e: ModelElement | e.elementOwnership !in elementOwnership_private} //Definition of associations all c: Classifier | c.associations = c.associationEnd.association //Definition of oppositeAssociationEnds all c: Classifier | c.oppositeAssociationEnds = {e: AssociationEnd | e in {a: c.associations | one c1 : a.connection.type | c1 = c}.connection && c !in e.type} + {e: AssociationEnd | e in {a: c.associations | some c1,c2: a.connection.type | c1 = c && c2 = c && c1 != c2}} //Definition of allOppositeAssociationEnds all c: Classifier | c.allOppositeAssociationEnds = c.+parent.oppositeAssociationEnds //Definition of allAttributes all c: Classifier | c.allAttributes = c.allFeatures & Attribute //Definition of specification -- INCOMPLETE } cond ComponentOp{ all c: Component | c.parentComponent = c.parent & Component //Definition of allResidentElements all c: Component | c.allResidentElements = c.*parentComponent.resident & {e: ModelElement | e.elementResidence !in elementResidence_private} } // WELL-FORMEDNESS CONDITIONS inv AssociationWF{ // connection multiplicity all a: Association | not one a.connection // Association [1] all a: Association | all e1,e2: a.connection | e1.name = e2.name -> e1 = e2 // Association [2] all a: Association | sole a.connection & (aggregation + composition) // Association [3] all a: Association | some e1,e2,e3: a.connection | (e1 != e2 && e1 != e3 && e2 != e3) -> a.connection !in (aggregation + composition) // Association [4] all a: Association | a.connection.type in a.namespace.ownedElement } inv AssociationClassWF{ //Multiple inheritance AssociationClass = Association & Class //Include operations AssociationClassOp ClassifierOp //AssociationClass [1] all a: AssociationClass | no (a.allConnections.name & (a.allFeatures & StructuralFeature).name) //AssocoationClass [2] all a: AssociationClass | a !in a.allConnections.type } inv AssociationEndWF{ //agregation and composition are disjoint no aggregation & composition //AssociationEnd [1] all e: AssociationEnd | (e.type in (Interface + DataType)) -> (e.association.connection - e) !in isNavigable //AssociationEnd [2] all e: AssociationEnd | e in composition -> e in multiplicity_max1 } inv BehavioralFeatureWF{ //BehavioralFeature [1] all b: BehavioralFeature | all p1,p2 : b.index.parameter | p1.name = p2.name -> p1 = p2 //BehavioralFeature [2] all b: BehavioralFeature | b.index.parameter.ptype in b.owner.namespace.ownedElement } inv ClassWF{ //include operations ClassifierOp //Class [1] all c: Class | c !in isAbstract -> all o: c.allOperations | some m: c.allMethods | o in m.specification //Class [2] all c: Class | c.allContents in (Class + Association + Generalization + UseCase + Constraint + Dependency + Collaboration + DataType + Interface) } inv ClassifierWF{ //include operations ClassifierOp //Classifier [1] all c: Classifier | all f,g: c.feature | (((f in Operation && g in Operation) || (f in Method && g in Method)) && g in f.hasSameSignature) -> f = g //Classifier [2] all c: Classifier | all p,q :(c.feature & Attribute) | p.name = q.name -> p = q //Classifier [3] all c: Classifier | all p,q: c.oppositeAssociationEnds | p.name = q.name -> p = q //Classifier [4] all c: Classifier | all a: c.feature & Attribute | a.name !in (c.allOppositeAssociationEnds + c.allContents).name //Classifier [5] all c: Classifier | all o: c.oppositeAssociationEnds | o.name !in (c.allAttributes + c.allContents).name //Classifier [6] //INCOMPLETE //Classifier [7] all c: Classifier | all g1, g2: c.powertypeRange | g1.discriminator = g2.discriminator } inv ComponentWF{ //include operations ComponentOp //vibility constraints for ElementResidence no elementResidence_private & elementResidence_protected //Component [1] Component.allContents in Component //Component [2] all e: Component.allResidentElements | e in (DataType + Interface + Class + Association + Dependency + Constraint) } inv ConstraintWF{ //Constraint [1] all c: Constraint | c !in c.constrainedElement } inv DatatypeWF{ //DataType [1] all d: DataType | all f: d.allFeatures | f in Operation & isQuery //DataType [2] all d: DataType | no d.allContents } inv ElementOwnershipWF{ //visibility constraint no elementOwnership_private & elementOwnership_protected } inv GeneralizableElementWF{ //include operations GeneralizableElementOp //GeneralizableElement [1] all e: GeneralizableElement | e in isRoot -> no e.generalization //GeneralizableElement [2] all e: GeneralizableElement | no (e.parent & isLeaf) //GenrelizableElement [3] all e: GeneralizableElement | e !in e.allParents //GeneralizableElement [4] all e: GeneralizableElement | all g: e.generalization | g.parent1 in e.namespace.allContents } inv GeneralizationWF{ //Generalization [1] INCOMPLETE } inv InterfaceWF{ //Interface [1] all i: Interface | i.allFeatures in Operation //Interface [2] no Interface.allContents //Interface [3] Interface.allFeatures !in (feature_private + feature_protected) } inv MethodWF{ //Method [1] all m: Method | m.specification in isQuery -> m in isQuery //Method [2] all m: Method | m.specification in m.hasSameSignature //Method [3] all m: Method | m in feature_private && m.specification in feature_private || m in feature_protected && m.specification in feature_protected || m !in (feature_private + feature_protected) && m.specification !in (feature_private + feature_protected) //Method [4] all m: Method | m.specification in m.owner.allOperations //Method [5] all m: Method | (m.owner.allOperations & {o: Operation | o in m.hasSameSignature}) in m.specification.owner.allOperations } inv ModelElementWF{ //visibility constraint for Feature no feature_private & feature_protected } inv NamespaceWF{ //Namespace [1] all n: Namespace | all e1,e2: n.allContents | (e1 !in Association && e2 !in Association && one e1.name && one e2.name && e1.name = e2.name) -> e1 = e2 //Namespace [2] all n: Namespace | all a1, a2: n.allContents & Association | (a1.name = a2.name && a1.connection.type = a2.connection.type) -> a1 = a2 } inv StructuralFeatureWF{ //StructuralFeature [1] all s: StructuralFeature | s.type in s.owner.namespace.allContents //StructuralFeature [2] all s: StructuralFeature | s.type in (Class + DataType + Interface) } }


Date view Thread view Subject view Author view