[ontoiop-forum] Call for final comments on DOL, UML

[Bock, Conrad]

Thanks, Till,

 >  > Why not define sets as restricted bags (bags with no duplicates),
 >  > like you did with ordered sets as restricted sequences?  Should be
 >  > at least: (forall (x) (if (form:Set x) (form:Bag x)) plus
 >  > no-duplicate restriction.

 >  Note that I did *not* define ordered sets as restricted
 >  sequences. Instead,

Then I'm probably misread this:

  oms ordered-sets = sequences with

to the uninitiated looks like ordered sets builds on sequences.

 >  In particular, the axiom
 >  // no element can be inserted twice
 >  (forall (x s)
 >    (if (from:ordered-set-member x s)
 >        (= (form:ordered-set-insert x s) s)))

 >  cannot be used for sequences.

Agreed, it's a restriction on sequences, and would only apply to ordered
sets as a specialization of sequences, not sequences in general.

 > I copied the theory of sequences and modified it. 

 >  If wanted, I can try to have a similar sharing of theories between
 >  sets and bags.

Sharing is better than copying, if you have the time to do it.

 >  > Did you intend to support infinite sets? Not that this requires it
 >  > (only allows it), but UnlimitedNatural in UML includes an
 >  > infinitely large value.  See comment about multiplicity in E.4.

 >  No, only finite sets are supported, assuming that system snapshots are
 >  always finite. Instead of UnlimitedNatural, we could also use natural
 >  numbers without an infinitely large value. What would be the name of
 >  such a type?

Looks like I was wrong, UnlimitedNatural means what what you said
above.  From Clause 8.2.4 (Notation) in UML 2.5:

  Note that "unlimited" denotes the lack of a limit on the value of
  some element (such as a multiplicity upper bound), not a value of
  "infinity."

Not sure if DOL requires any change for this or not, see next.

 >  > How are unlimited upper bounds represented?  This could be the
 >  > absence of a bound in DOL, I guess.  In UML, absence of a bound
 >  > defaults to 1, so there's no ambiguity translating to DOL this
 >  > way.  Where does UnlimitedNatural come in?

 >  Yes, unlimited upper bounds are represented by absence of bounds here.

OK.

 >  > Why not just (forall (x s)(form:set-member x (form:set-insert x s))) ?

 >  The original axiom is:

 >  (forall (x y s)
 >    (iff (form:set-member x (form:set-insert y s))
 >         (or (= x y)
 >              (form:set-member x s))))

 >  This is much stronger. In particular, from it you can derive non-
 >  memberships, like (not (form:set-member 2 (form:set.insert 1
 >  form:empty-set))), provided that 1 is not equal to 2.

I see.  Would be clearer to have membership and non-membership in
separate axioms:

  (forall (x s)(form:set-member x (form:set-insert x s)))

  (forall (x s1) (iff (form:set-member x s1)
                      (exists (s2) (= s1 (form:set-insert x s2)))))

but I guess it's all the same.

 >  > Not sure I'm reading this correctly, but it seems to say the
 >  > properties involved in a composition association are properties of
 >  > m, whereas they are usually properties of the classes at the ends
 >  > of the association.

 >  We have changed this, see attached corrected PDF.

It isn't changed in the update, but my understanding from Alexander is
the dot notation in property declarations (eg, m.p) here does not imply
p is an attribute of m.

BTW, the term "property declaration" appears here for the first time.
The terms "property" and "attribute" are synonyms in UML, would be
clearer to use a different word.

 >  > Properties can be composed without being member ends of an
 >  association.  The UML 2.5 spec describes aggregation in the Property
 >  subclause (9.5.3), without constraining the properties to be member
 >  ends of associations.  The phrase quoted here describes a composite
 >  property with ("grouping its") values.  Feel free to ask Ed and
 >  others, this is well known to be the interpretation of the spec, and
 >  is implemented in tools.

 >  We have changed this, see attached corrected PDF.

The text doesn't seem to be changed.  It still explains UML incorrectly.
Alexander seemed to have found this problem already in his reply.

 >  > Are the labels n2s, etc, association names?  If so they should be
 >  > capitalized.  If they are property names, they should be closer to
 >  > one of the classes at the end of the line.

 >  Yes, they are association names. We will capitalize them.

Would be good to mention it in the text.

BTW, the update still has an issue written into a comment:

 //The same-set relation is true for sets that have the same members.
 // but: why not replace same-set with = ?

on p 89, near the bottom.  You could file it with the FTF if you don't
want to address it in the submission.