Skip to main content


Eclipse Community Forums
Forum Search:

Search      Help    Register    Login    Home
Home » Modeling » OCL » Safe OCL
Safe OCL [message #1803966] Thu, 14 March 2019 14:53 Go to next message
Denis Nikiforov is currently offline Denis NikiforovFriend
Messages: 218
Registered: August 2013
Senior Member
Hi

Maybe it will be interesting for somebody.

I described formally the OCL type system, its abstract syntax, typing rules and safe navigation normaliztion rules: https://www.isa-afp.org/entries/Safe_OCL.html

The main difference from Featherweight OCL is that I use the deep embedding approach instead of the shallow embedding. So my theory seems to be simpler, at least for me :)

I described formally T[1] and T[?] types. Also I added an OclSuper type - a super type of all other types (basic type, collections, tuples). It allowed me to define the type hierarchy as an upper semilattice. As a result the typing rules for OCL expressions looks very elegant and cool.

Also the typing rules a much stricter than rules given in the OCL specification.

Most of the theory is technical. I guess that the most interesting sections are the following:

The beginning of 2.1 - basic types and their subtype relation
The beginning of 2.3 - supremum of two basic types
The beginning of 3.1 - general OCL types and their subtype relation
The beginning of 3.4 - supremum of two OCL types
4 - abstract syntax
6.1 - standard library operations typing
6.2 - expressions typing
7.1 - normaliztion rules
8 - examples and test cases

I plan to describe all this stuff in details in the article. And also I plan to define OCL semantics. But I don't know when.
Re: Safe OCL [message #1803971 is a reply to message #1803966] Thu, 14 March 2019 15:18 Go to previous messageGo to next message
Ed Willink is currently offline Ed WillinkFriend
Messages: 6538
Registered: July 2009
Senior Member
Hi

Thanks. I'll try to look at, but it doesn't seem like an easy read ...

FYI. Your OclSuper may be the same as OclElement/OclAny. Have a look at https://git.eclipse.org/c/ocl/org.eclipse.ocl.git/tree/plugins/org.eclipse.ocl.pivot/model/OCL-2.5.oclstdlib to see the current OclAny/OclElement/OclType etc hierarchy in the Pivot Eclipse OCL.

Collection conforms to OclAny is something that challenges rigorous type systems. I think it was a mistake. You might be interested in the comment on https://issues.omg.org/browse/OCL25-77 that replaces it by a wrapper type.

I hope you do T as a template parameter rather than a magic macro.

T[1] and T[?] extend to Set(T[*|1]) for collections; collection-multiplicity|element-multiplicity.

Regards

Ed Willink



Re: Safe OCL [message #1803978 is a reply to message #1803971] Thu, 14 March 2019 17:31 Go to previous messageGo to next message
Denis Nikiforov is currently offline Denis NikiforovFriend
Messages: 218
Registered: August 2013
Senior Member
Here is the basic types from the theory:
datatype 'a basic_type =
  OclAny
| OclVoid
| Boolean
| Real
| Integer
| UnlimitedNatural
| String
| ObjectType 'a
| Enum "'a enum"

with the following subtype relation:
inductive basic_subtype (infix "⊏⇩B" 65) where
  "OclVoid ⊏⇩B Boolean"
| "OclVoid ⊏⇩B UnlimitedNatural"
| "OclVoid ⊏⇩B String"
| "OclVoid ⊏⇩B ⟨C⟩⇩T"
| "OclVoid ⊏⇩B Enum E"

| "UnlimitedNatural ⊏⇩B Integer"
| "Integer ⊏⇩B Real"
| "C < D ⟹ ⟨C⟩⇩T ⊏⇩B ⟨D⟩⇩T"

| "Boolean ⊏⇩B OclAny"
| "Real ⊏⇩B OclAny"
| "String ⊏⇩B OclAny"
| "⟨C⟩⇩T ⊏⇩B OclAny"
| "Enum E ⊏⇩B OclAny"


And general OCL types:
datatype 'a type =
  OclSuper
| Required "'a basic_type" ("_[1]" [1000] 1000)
| Optional "'a basic_type" ("_[?]" [1000] 1000)
| Collection "'a type"
| Set "'a type"
| OrderedSet "'a type"
| Bag "'a type"
| Sequence "'a type"
| Tuple "telem ⇀ 'a type"

with the following subtype relation:
inductive subtype :: "'a::order type ⇒ 'a type ⇒ bool" (infix "⊏" 65) where
  "τ ⊏⇩B σ ⟹ τ[1] ⊏ σ[1]"
| "τ ⊏⇩B σ ⟹ τ[?] ⊏ σ[?]"
| "τ[1] ⊏ τ[?]"
| "OclAny[?] ⊏ OclSuper"

| "τ ⊏ σ ⟹ Collection τ ⊏ Collection σ"
| "τ ⊏ σ ⟹ Set τ ⊏ Set σ"
| "τ ⊏ σ ⟹ OrderedSet τ ⊏ OrderedSet σ"
| "τ ⊏ σ ⟹ Bag τ ⊏ Bag σ"
| "τ ⊏ σ ⟹ Sequence τ ⊏ Sequence σ"
| "Set τ ⊏ Collection τ"
| "OrderedSet τ ⊏ Collection τ"
| "Bag τ ⊏ Collection τ"
| "Sequence τ ⊏ Collection τ"
| "Collection OclSuper ⊏ OclSuper"

| "strict_subtuple (λτ σ. τ ⊏ σ ∨ τ = σ) π ξ ⟹
   Tuple π ⊏ Tuple ξ"
| "Tuple π ⊏ OclSuper"


For example the following rule means that τ[1] conforms to σ[1] if basic type τ conforms to basic type σ.
"τ ⊏⇩B σ ⟹ τ[1] ⊏ σ[1]"

For example UnlimitedNatural[1] conforms to Integer[1] because UnlimitedNatural conforms to Integer.
Also UnlimitedNatural[1] conforms to Integer[?], Real[?], OclAny[1], OclAny[?], ...

The general OCL types are defined as a recursive algebraic datatype, with the following instances:
Boolean[1]
Set(Integer[?])
Sequence(Set(Integer[?]))
...

Basic types are not used directly. They only required to define general OCL types. So, OclAny is not a valid type in the theory. It should always be used either as OclAny[1] or OclAny[?].

The OCL specification says that collection types doesn't conform to OclAny. And it seems to me a good idea. I always know that an expression with a type which conforms to OclAny[?] is a single valued.

For example, when I define a normalization rules for navigation shorthands and safe navigations in Chapter 7 I need to check whether an expression is a single-valued or collection-valued. And OclAny[?] type is very handy.

The same is true of OclVoid. It can be used only for single values in the form of OclVoid[1] or OclVoid[?]. It doesn't conform to collection types. Because collections can't be null.

In other words it's handy to have a super type of all single values. For example it allows one to define a specific operations only for single values and not for collections (please see Section 6.1.4). I'm not sure about toString(), oclIsNew() and oclIsInvalid() operations. I guess it should be defined for collections and tuples as well. However, I guess that oclAsSet() and oclIsUndefined() should be defined only for single values.

However, I need also a super type of all types, so I added OclSuper.

I don't have access to https://issues.omg.org/browse/OCL25-77 Maybe you could quote it here?


Quote:
I hope you do T as a template parameter rather than a magic macro.

T is just a type variable in the theory. I'm sure that expression typing rules are looks very tricky. I'll try to describe them.

For example, consider the following typing rules for binary collection operations from Section 6.1.8:

| collection-binop-type UnionOp (Set τ ) (Set σ) (Set (τ ⊔ σ))
| collection-binop-type UnionOp (Set τ ) (Bag σ) (Bag (τ ⊔ σ))
| collection-binop-type UnionOp (Bag τ ) (Set σ) (Bag (τ ⊔ σ))
| collection-binop-type UnionOp (Bag τ ) (Bag σ) (Bag (τ ⊔ σ))

collection-binop-type is a relation with 4 arguments:
1) A kind of the operation
2) A type of a source expression
3) A type of an argument
4) A (resulting) type of the whole expression

Let's consider the following expression:
Set{1,2}->union(Bag{'a',null})

The type of the expression is determinied using this rule:
collection-binop-type UnionOp (Set τ ) (Bag σ) (Bag (τ ⊔ σ))

τ = Set(Integer[1])
σ = Bag(String[?])

and so the type of expression is
Bag(τ ⊔ σ) = Bag(Integer[1] ⊔ String[?]) = Bag(OclAny[?])


Here is a more complicated rule for includes() operation from the same section:
element_type τ ρ ⟹ σ ≤ to_optional_type_nested ρ ⟹
collection_binop_type IncludesOp τ σ Boolean[1]

At first we get an element type (ρ) of a source collection using "element_type τ ρ". Then we transform the inner-most type to a nullable type using "to_optional_type_nested ρ". And at last we check that the type of argument of includes() operation (σ) conforms to this type. If all conditions are true then the whole expression has the Boolean[1] type.

Consider the following expression:
let x : Integer[?] = 7 in
Sequence{1..5}->includes(x)

τ = Sequence(Integer[1])
ρ = Integer[1]
to_optional_type_nested ρ = Integer[?]
σ = Integer[?]
σ ≤ to_optional_type_nested ρ = true

So the expression is well-typed and has the Boolean[1] type.

Quote:
T[1] and T[?] extend to Set(T[*|1]) for collections; collection-multiplicity|element-multiplicity.

My theory doesn't support collection-multiplicity. It supports null-free collections: Set(Integer[1]), Sequence(Bag(Boolean[1])), ... It supports also collection with nullable elements: Set(Real[?]), Set(Bag(Real[?])). However please note that Set(Bag(Real[?])) can contain nulls only in the inner Bag, not in the outter Set, because null is not a valid instance of Bag(Real[?]). Collections can't be nullable in my theory.

The theory doesn't allow one to restrict minimum and maximum count of elements in collections, because it complicates the type system significantly. Collections becomes a dependent types (types dependent on values). Most of the languages doesn't support dependent types. And I'm not sure that OCL should support them.

However the Object Model described in Section 1.5 support min and max element occurs:

type_synonym 'c assoc_end = "'c × nat × enat × bool × bool"
definition "assoc_end_class :: 'c assoc_end ⇒ 'c ≡ fst"
definition "assoc_end_min :: 'c assoc_end ⇒ nat ≡ fst ∘ snd"
definition "assoc_end_max :: 'c assoc_end ⇒ enat ≡ fst ∘ snd ∘ snd"
definition "assoc_end_ordered :: 'c assoc_end ⇒ bool ≡ fst ∘ snd ∘ snd ∘ snd"
definition "assoc_end_unique :: 'c assoc_end ⇒ bool ≡ snd ∘ snd ∘ snd ∘ snd"

An association end is a tuple of 5 elements:
1) A destination class of the association end
2) Min occurs
3) Max occurs
4) Ordered indicatior
5) Unique indicator

And the function from Section 5 calculates a datatype for an association end:
definition
  "assoc_end_type end ≡
    let C = assoc_end_class end in
    if assoc_end_max end ≤ (1 :: nat) then
      if assoc_end_min end = (0 :: nat)
      then ⟨C⟩⇩T[?]
      else ⟨C⟩⇩T[1]
    else
      if assoc_end_unique end then
        if assoc_end_ordered end
        then OrderedSet ⟨C⟩⇩T[1]
        else Set ⟨C⟩⇩T[1]
      else
        if assoc_end_ordered end
        then Sequence ⟨C⟩⇩T[1]
        else Bag ⟨C⟩⇩T[1]"

So the information on min and max occurs is defined in the object model but it's lost in the type system.

[Updated on: Thu, 14 March 2019 17:37]

Report message to a moderator

Re: Safe OCL [message #1803993 is a reply to message #1803978] Fri, 15 March 2019 02:53 Go to previous messageGo to next message
Denis Nikiforov is currently offline Denis NikiforovFriend
Messages: 218
Registered: August 2013
Senior Member
The previous message have been cropped because of unsupported unicode symbols. I updated it.

I guess that the following notation could be confusing:
⟨C⟩⇩T[?]

C - is a class. A down arrow - means that the next symbol is a subscript. A class with a subscript T - is an object type corrseponding to the class. And [?] notes that the object type is nullable.

There is no such problem in the formatted text or the PDF document.

I use lower greek letters for type variables: τ, σ, ρ.
Re: Safe OCL [message #1803996 is a reply to message #1803993] Fri, 15 March 2019 06:36 Go to previous messageGo to next message
Denis Nikiforov is currently offline Denis NikiforovFriend
Messages: 218
Registered: August 2013
Senior Member
I have some additional points on collection type declarations.

I found the following notation hard to understand: Sequence(Sequence(Integer)[3|1])[3|1]

1) I guess that collections itself should not be nullable. The OCL specification is ambiguous on this point. The Section 8.2 of OCL specification states the following:
Quote:
VoidType is the metaclass of the OclVoid type that conforms to all types except the OclInvalid type.

In other words collections are nullable, because OclVoid conforms to collection types.

From the other point of view the Section A.2.5.1 defines the set of set types as follows:
I(Set(t)) = F (I(t)) U {invalid}

In other words a set is either a set of values or an invalid value. And it couldn't be null. I think that this point is better. Collections shouldn't be null.

So this type declaration Sequence(Sequence(Integer)[3|1])[3|1] should be Sequence(Sequence(Integer)[3|1])[3] because the inner sequence never can be null, only its elements could potentialy be null.

2) I think that basic types should always be used with a multiplicity quantifier. Instead of Integer one should use either Integer[1] or Integer[?].

So the declaration Sequence(Sequence(Integer)[3|1])[3] should be transformed into Sequence(Sequence(Integer[1])[3])[3]

3) I think that square braces for collection types are a little bit misleading. For example Sequence(Integer[1])[3] looks like three sequences of integers.

Maybe the following notation would be a more natural:
Sequence(Sequence(Integer[1], 3), 3)
Sequence(String[1], 1..10)
Sequence(String[1], 1..*)
Sequence(String[1], *)
...

Actually it's not a big deal to add min and max occurs to collection types. The Safe OCL type system could be easily updated. However as I said earlier it makes collection types dependent on values. It complicates the typing rules. For example how to determine the types of the following expressions?
Set{1,2,3}->including(1) : Set(Integer[1], 3)
Set{1,2,3}->including(5) : Set(Integer[1], 4)

or maybe the type should be Set(Integer[1], 3..4)

However why not. I think min and max occurs annotations could be added to the type system. It would be interesting to update the Safe OCL theory.
Re: Safe OCL [message #1803997 is a reply to message #1803996] Fri, 15 March 2019 06:50 Go to previous messageGo to next message
Denis Nikiforov is currently offline Denis NikiforovFriend
Messages: 218
Registered: August 2013
Senior Member
A last point on collections that I forget to mention. Perhaps this point will be a bit controversial.

I think collection types for association ends should always be null free. I can't imagine any example when the opposite would be required. So there is no need to explicitly annotate associations ends as null free in a model.
Re: Safe OCL [message #1804005 is a reply to message #1803997] Fri, 15 March 2019 12:00 Go to previous messageGo to next message
Ed Willink is currently offline Ed WillinkFriend
Messages: 6538
Registered: July 2009
Senior Member
Hi Denis

OCL has a very poor specification, which provides plenty of opportunities for 'clarification'. Despite these limitations OCL survives since its concrete syntax is fairly obvious. I therefore try hard to avoid anything that breaks traditional concrete syntax. The AS can certainly be significantly clarified. Mandating PrimitiveType multiplicities is not on. However I get confused, so you will find that the Eclipse OCL hovertext/error messages increasingly have explicit multiplicities for everything. The Collection multiplicity syntax is ugly, but other alternatives didn't work as nested collections.

Ed Seidewitz happened to be in the audience when I presented http://www.eclipse.org/modeling/mdt/ocl/docs/publications/OCL2015SafeNavigation/SafeNavigation.pdf and we had an interesting discussion. His goal is to make null non-existent in UML if it is not already non-existent. Null elements in collections are therefore not-UML so I switched the default in the Eclipse OCL tooling. nullable, rather than non-null collection elements must now be declared explicitly. null objects re however an unavoidable part of OCL, UML may try not to use them, but that can't change OCL. Of course a Constraint may have no name, so whoops a null element in UML after all.

https://bugs.eclipse.org/bugs/show_bug.cgi?id=543602 shows that null collections happen.

If you are looking seriously at the null-safe type system, you might also consider the invalid-safe type system. Short-circuit iteration evaluation requires a proof that a 'future' evaluation cannot be invalid, so we really want to carry invalid in the type system. My favourite idea is an additional ! in the concrete syntax. i.e. Integer[1!] is an integer or invalid. Operations such as Real::/ should have a Real[1!] return type, cf throws in Java.

In my null-safe paper I considered max/min bounds, but dismissed them as too much pedantic effort. However I keep coming up with OCL expressions that have spurious null-safe warnings because of inaccurate bounds/nullities and so org.eclipse.ocl.pivot.internal.manager.TemplateParameterSubstitutionHelper has a steadily growing set of manually coded computations of operation/iteration return types that should really be modelled.

Regards

Ed Willink





Re: Safe OCL [message #1804012 is a reply to message #1804005] Fri, 15 March 2019 16:50 Go to previous messageGo to next message
Denis Nikiforov is currently offline Denis NikiforovFriend
Messages: 218
Registered: August 2013
Senior Member
Hi

I think that multiplicity for single valued types could be optional for the backward compatibility. I guess that [?] could be a default multiplicity to be consistent with previous versions of the specification. And so for example Integer is interpreted as Integer[?].

I don't understand why, for example, the following notation is not suitable for collection multiplicities?
Sequence(Sequence(Integer[1], 3), 3)
It looks simpler. However collections should be non-nullable to use this notation.

I absolutely agree that the UML should not contain collections with null elements. However such a collections could be a result of some OCL expression. My theory is implemented in accordance with this assumption.

Thanks for the interesting example of nullable collections. Let me duplicate the problem here as follows: How to interpret the expression "operation?.ownedParameters->at(2)"?

As I can see there are 3 possible answers described in the bug report:

1) The expression is transformed into "(if operation <> null then operation.ownedParameters else null endif)->at(2)"

In this case a user will see a warning that the expression should be rewriten as follows:
operation?.ownedParameters?->at(2)

The bad thing is that it forces us 1) to allow nullable collections and 2) to complicate the transformation rule for ?-> as follows:

x?->y => if x <> null then x->excludingAll(null)->y else null endif

2) The expression is transformed into "(if operation <> null then operation.ownedParameters else Collection{} endif)->at(2)"

This solution is bad because it hides the fact that operation is missing. For example, let us consider another hypothetical expression:

aClass.operations->any(name = 'op')?.ownedParameters->size()

An expected semantics of this expression is as follows:
a) Find operation 'op' of aClass
b) Calculate the number of its parameters

This semantics is violated if the expression will return 0 instead of invalid.

3) And the last solution is to prohibit such an expression and to force a user to check that operation is not null explicitly:

if operation <> null then
operation.oclAsType(Operation[1]).ownedParameters->at(2)
else
null
endif


I was absolutely sure that the last solution is the only right one. And this variant is implemented in my theory as follows:

a) operation?.ownedParameters->at(2)
is transformed to
(if operation <> null then operation.oclAsType(Operation[1]).ownedParameters else null endif)->at(2)

b) The type of "operation.oclAsType(Operation[1]).ownedParameters" is Sequence(Parameter[1])
The type of null is OclVoid[?]
And so the type of the if expression is a least supertype of Sequence(Parameter[1]) and OclVoid[?] = OclSuper

c) ->at() operation is not defined for OclSuper. So the expression is ill-typed.


I think that safe navigation operations is just a syntactic sugar, which simplifies a life of a developer. But nullable collections is an absolute evil from my point of view. So if I have to choose between nullable collections and an extra code in OCL expressions, I prefer the last one.

The big problem with nullable collections is that we have to specify whether each collection is nullable or not. It makes collection type declaration very verbose, it complicates typing rules.

The idea of safe navigation, as I see it, is to simplify the life of a developer, which was complicated by the presence of nulls. The paradox is that we have to add extra nulls (nullable collections) to the language. I do not have a clear understanding of which solution is preferable.

(Maybe it will be interesting for you. I don't use excluding(null) operation for safe navigations. I use selectByKind(T[1]) instead, where T is a non-nullable version of the original type. Please see Table 7.1 on page 98)


With regard to invalid-safe type system. Actually my original idea was as follows. I implemented a transformation from OCL expressions to XPath expressions (in QVTo). I wanted to prove its correctness. To achieve this I required a formal specification of OCL and XPath. Featherweight OCL was too complicated to me, and also it use the shallow embedding approach (the OCL is build on top of Isabelle HOL). But I need a specification based on the deep embedding approach. It will allow me to describe a transformation from OCL to XPath formally and to prove all required theorems. That's why I implemented this formal specification.

The interesting thing is that OCL and XPath are very similar languages. However they differs significantly on the treatment of nulls and error values. So it's very important whether the type system distinct nullable and non-nullable types or not. For sure distinction between errorable and non-errorable types is very important too. But the definition of such a type system looked too complicated for me. I thought that I should analyze values during type checking phase. For example, "1 / 2" should have the Real[1] type, and "1 / 0" should have the errorable Real[1] type. I see now that it's enough to use the errorable type for the division operation always.

Quote:
However I keep coming up with OCL expressions that have spurious null-safe warnings because of inaccurate bounds/nullities and so org.eclipse.ocl.pivot.internal.manager.TemplateParameterSubstitutionHelper has a steadily growing set of manually coded computations of operation/iteration return types that should really be modelled.

It would be interesting to me to know some details on this problem. Because it is implemented very simply in my theory. For example the following expressions are ill-typed:

1) let x : Integer[?] = 1 in x + 2
2) Sequence{1..5}?->max()
3) Sequence{1..5, null}->sum()

At first an expression is normalized using rules described in Table 7.1 on page 98. The 2nd expression will fail on this step because ?-> can be applied only to a collection with nullable elements.

The 1st and 3rd expressions will fail on type checking phase, because + is defined only for Integer[1] (it's not defined for Integer[?]). And ->sum() is defined either for a collection of non-nullable numbers or for a collection of elements with + operation defined.
Re: Safe OCL [message #1804026 is a reply to message #1804012] Sat, 16 March 2019 06:19 Go to previous messageGo to next message
Denis Nikiforov is currently offline Denis NikiforovFriend
Messages: 218
Registered: August 2013
Senior Member
Quote:
I think that multiplicity for single valued types could be optional for the backward compatibility. I guess that [?] could be a default multiplicity to be consistent with previous versions of the specification. And so for example Integer is interpreted as Integer[?].

It seems that it was a bad idea, becuase in the most of the languages [1] is the default multiplicity, and [?] should be specified explicitly.

Also I think that you are right and collections should be nullable. Because in some cases we need to state the fact that a collection is absent. For example, "a set of paramenters of non-existent operation" and "an empty set of parameters" are different things. Both of them should be expressible in the language. Tuples should be nullable for completeness too.

I'll try to replace OclSuper by OclAny in my theory. Maybe a separate super type of basic types is not actually required.
Re: Safe OCL [message #1804030 is a reply to message #1804026] Sat, 16 March 2019 08:21 Go to previous messageGo to next message
Ed Willink is currently offline Ed WillinkFriend
Messages: 6538
Registered: July 2009
Senior Member
Hi

In Java Integer[?], int[1] are the defaults. Very pragmatic.

I am open to retaining OclAny for non-Collections and introducing a further very very thin super type, I had toyed with OclObject, OclThing, ... as a genuine bottom type. Perhaps OclBottom, OclRoot, ..

Googling, I find "unit type". Perhaps OclAny stays but gets thinner...

OclAny < OclUnit < OclElement < OclType < OclStereotype
OclAny < CollectionType
OclElement < user-class-types, TupleType
OclUnit < OclLambda < user-lambda-types
OclUnit < OclSelf
OclUnit < OclTuple < user-tuple-types
OclUnit < primitive-types
OclUnit < user-data-types
OclStereotype < user-stereotypes
(OclComparable, OclSummable mix-ins for <,> etc and +)

But you still have the problem that a Collection(OclAny) is needed for nested Collections, unless you restrict to Collection(OclUnit) and provide a wrapper to wrap an aggregate as a unit.

Regards

Ed Willink
Re: Safe OCL [message #1804033 is a reply to message #1804030] Sat, 16 March 2019 09:34 Go to previous messageGo to next message
Denis Nikiforov is currently offline Denis NikiforovFriend
Messages: 218
Registered: August 2013
Senior Member
The same nullable defaults was in C#. But since C# 8.0 it was changed:
https://msdn.microsoft.com/en-us/magazine/mt829270.aspx
https://dotnetcoretutorials.com/2018/12/19/nullable-reference-types-in-c-8/

Both value and reference types are non-nullable by default now. For sure it's a non-backward compatible change. So to enable it one should set a special compiler flag.

In XPath all types (primitive and elements) are non-nullable by default.

Nested collections is not a problem in my theory. Here is a subtype relation:
inductive subtype :: "'a::order type ⇒ 'a type ⇒ bool" (infix "⊏" 65) where
  "τ ⊏⇩B σ ⟹ τ[1] ⊏ σ[1]"
| "τ ⊏⇩B σ ⟹ τ[?] ⊏ σ[?]"
| "τ[1] ⊏ τ[?]"
| "OclAny[?] ⊏ OclSuper"

| "τ ⊏ σ ⟹ Collection τ ⊏ Collection σ"
| "τ ⊏ σ ⟹ Set τ ⊏ Set σ"
| "τ ⊏ σ ⟹ OrderedSet τ ⊏ OrderedSet σ"
| "τ ⊏ σ ⟹ Bag τ ⊏ Bag σ"
| "τ ⊏ σ ⟹ Sequence τ ⊏ Sequence σ"
| "Set τ ⊏ Collection τ"
| "OrderedSet τ ⊏ Collection τ"
| "Bag τ ⊏ Collection τ"
| "Sequence τ ⊏ Collection τ"
| "Collection OclSuper ⊏ OclSuper"

| "strict_subtuple (λτ σ. τ ⊏ σ ∨ τ = σ) π ξ ⟹
   Tuple π ⊏ Tuple ξ"
| "Tuple π ⊏ OclSuper"

Please note that
Collection OclSuper ⊏ OclSuper

Maybe it's a problem for objet oriented models. But it works fine in a logical theory.

However I described only a type system and typing rules for expressions. Maybe I will experience problems when I will try to describe OCL semantics...
Re: Safe OCL [message #1804137 is a reply to message #1804012] Tue, 19 March 2019 08:20 Go to previous messageGo to next message
Ed Willink is currently offline Ed WillinkFriend
Messages: 6538
Registered: July 2009
Senior Member
Hi

Denis Nikiforov wrote on Fri, 15 March 2019 12:50

Quote:
However I keep coming up with OCL expressions that have spurious null-safe warnings because of inaccurate bounds/nullities and so org.eclipse.ocl.pivot.internal.manager.TemplateParameterSubstitutionHelper has a steadily growing set of manually coded computations of operation/iteration return types that should really be modelled.

It would be interesting to me to know some details on this problem. Because it is implemented very simply in my theory.


The most recent example was https://bugs.eclipse.org/bugs/show_bug.cgi?id=494536 whose discovery was a consequence of adding the missing null-safe iteration return type WFR.

It appears that as I have added the null-safe WFRs, I have encountered problems that have caused me to omit some. After resolving the problem, I neglect to go back and add the WFR. There have therefore been at least three phases of null-safe validation strengthening. Each phase has been triggered by an observation (often a run-time NPE) that a null-safe hazard had not been diagnosed.

AFAAIA the only 'missing' validation is for null-safe operation call arguments, which isn't really a null-safe issue; it's a calling convention mis-match. I haven't decided whether to broaden the argument type-check or add a separate null-safe check. In either case I have an API compatibility detail to cope with internally.

Regards

Ed Willink

Re: Safe OCL [message #1804666 is a reply to message #1804137] Fri, 29 March 2019 18:50 Go to previous messageGo to next message
Denis Nikiforov is currently offline Denis NikiforovFriend
Messages: 218
Registered: August 2013
Senior Member
Hi

I added nullable collections and tuples to the theory. Also I added errorable and error-free types. Here is a development version of the theory: https://github.com/AresEkb/Safe_OCL

You can find an informal outline of the theory on the main page of the repository (in README.md).

It is a very preliminary version. I'm sure that it contains a lot of errors. An informal description still over-complicated. I think it will take a couple of weeks or a month to finish it.
Re: Safe OCL [message #1804735 is a reply to message #1803978] Sat, 30 March 2019 19:18 Go to previous messageGo to next message
Ed Willink is currently offline Ed WillinkFriend
Messages: 6538
Registered: July 2009
Senior Member
Hi

Denis Nikiforov wrote on Thu, 14 March 2019 13:31
I don't have access to https://issues.omg.org/browse/OCL25-77 Maybe you could quote it here?


Quote:
OMG Issue No: 12948
Title: Making OclAny denote any object
Source:
M. Belaunde, Orange Labs
Summary:
In the actual OCL2 spec OclAny represents any object except collections.
However this is unaligned with UML2 and MOF2 where such kind of type does not exist
Instead in MOF we have the generic Object which represents any object including
primitive and collection values.
Also, looking at the list of operations defined for OclAny we see that there is no real
justification for creating this special type. Operations like 'allInstances' and 'oclIsNew' are
also invalid for primitive types and hence are not specifically invalid for collections.
Making OclAny to represent any object (equivalent to MOF::Object) will simplify the
stdlib and will be consistent with UML2 and MOF2.
Resolution:
OclAny denotes now any object including collections. This makes the type system
aligned with MOF.
Revised Text:
(1) In Section 8.2, AnyType, replace the actual AnyType definition:
AnyType is a special type that complies to all the types except the collection types. AnyType has a unique
instance named OclAny. It is defined to allow defining generic operations that can be invoked in any object
or primitive literal value.
By the following:
AnyType is the metaclass of the special type OclAny, which is the type to which all other
types conform. OclAny is the sole instance of AnyType. This metaclass allows defining
the special property of being the generalization of all other Classifiers, including Classes,
DataTypes and PrimitiveTypes.
(2) In Section "8.2.1 Type Conformance", remove the second rule for Classifiers (All
classifiers except collections conform to OclAny)
(3) In Section "11.2.1 OclAny", replace the sentences
"All types in the UML model and the primitive types in the OCL standard library complies with the type
OclAny. Conceptually, OclAny behaves as a supertype for all the types except for the OCL pre-defined
collection types."
By
"All types in the UML model and the primitive and collection types in the OCL standard library conforms
to the type OclAny. Conceptually, OclAny behaves as a supertype for all the types."


What is your motivation for all this hard work? a PhD thesis, a paid contract, enthusiasm, ...

Potentially this should replace Annex A in a next OCL version. But it needs a couple of pages of friendly intro. I can guess at a lot of it but am totally bemused by "65" and "1000" and "'a".

UnlimitedNatural is not a subtype of Integer. since the unlimited value is not convertible. Rather UnlimitedNatural is an open enumeration of all the non-negative integer values plus *, with conversion operators to/from Integer that tooling may deduce for legacy purposes.

(There is also the Map type....)

Regards

Ed Willink

Re: Safe OCL [message #1804748 is a reply to message #1804735] Sun, 31 March 2019 10:20 Go to previous messageGo to next message
Denis Nikiforov is currently offline Denis NikiforovFriend
Messages: 218
Registered: August 2013
Senior Member
Hi

My motivation is just to satisfy interest in the field of formal languages. In my main job, we develop integration projects for inter-government or inter-bank information exchange. The cornerstone of such projects is the data model. For some projects we use an existing data models (for example, ISO 20022), for another projects we develop a custom data model (for example this one, it has no English version). Many integration projects are limited to this. However, we also formalize business rules for validation of exchanged data in OCL.

These OCL specifications are transformed into XSLT or Java code + XPath expressions. Here is an article and a presentation. The transformation is implemented in QVTo, here is a very outdated version. Here is an XPath 2.0 metamodel + parser/printer based on EMFText. However, now, I would rewrite it on Xtext.

I am very interested in proving that this OCL to XPath transformation is correct (it preserves a semantics of expressions). However, at first I need a formal type system and semantics of OCL.

Actually I plan to get a PhD. But at first I need to finish this theory and describe it in several articles. Then I plan to deal with organizational issues (search for an academic advisor, dissertation council, etc.). I'm sure it's a wrong order of steps, but anyway.



"'a" is a type parameter. You can consider "'a type" as a generic datatype named "type" with a parameter 'a. In this case 'a is a datatype of UML/Ecore classes.

Please see Chapter 8. Examples, where I define an example datatype of classes:
datatype classes1 = Object | Person | Employee | Customer | Project | Task | Sprint

And then I use a specialized "classes1 type" - a type of OCL types specialized for classes1.


Here is a fragment of OCL types definition:
datatype 'a type =
  OclAny
| OclVoid
...
| ObjectType 'a ("⟨_⟩<sub>T</sub>" [0] 1000)
...

When I bind a parameter 'a to a particular datatype representing classes (for example classes1 datatype), I get a concrete OCL type system for these classes.

OclAny, OclVoid are parameter-less constructors of this datataype. And ObjectType is a constructor, which takes one parameter of type 'a.

For example, "Person" is a class in an UML model. "ObjectType Person" is an OCL type, which corresponds to this class.

An alternative notation for a type constructor, a function, or an inductive predicate can be specified in parenthesis. "0", "1000", "65", ... is an operator priority, which used by Isabelle HOL to parse this notation.

For example, instead of "ObjectType Person" I can write "⟨Person⟩<sub>T</sub>".

Actually these priority numbers is a technical details. I think they could be omitted in the informal description.


I think I agree with the quotation on OclAny. It seems that where is no need for a special supertype of all primitive types. oclIsUndefined(), =, <>, etc. should be defined for all types including collections.


From my point of view it's good that UnlimitedNatural is not a subtype of Integer. This fact simplifies a typing rule for oclAsType(), because upcasting never returns invalid now. The only exclusion from this rule was the upcasting from * to Integer. Also it seems that most of the typing rules for numeric operations are wrong in my theory. Because UnlimitedNatural casted to Integer or Real could be invalid. And so for example a sum of UnlimitedNatural and Real could be invalid. But, now, the plus operartor is always error-free in the theory. I'll fix it.


Could you please give some details on the map type? What types are allowed for keys and values? I guess that keys could have any primitive type (boolean, real, integer, unlimited natural, string, object types, enum)? Collections are prohibited for keys? OclVoid and OclAny are prohibited? Any tuple keys are prohibited? Or tuples of primitive values are allowed?
Values can be of any type? What operations and iterations are defined for maps?
Re: Safe OCL [message #1804751 is a reply to message #1804748] Sun, 31 March 2019 11:58 Go to previous messageGo to next message
Ed Willink is currently offline Ed WillinkFriend
Messages: 6538
Registered: July 2009
Senior Member
Hi

I guess what I really want to know is whether you will still be interested in three years time ow whether I will be left holding the baby if I try to exploit your work.

Rather than provide briefg explnations as in your previous reply, please provide n extra couple of pages of into so that typical readers of the OCL specification Annex A, who know nothing of Isabelle, can appreciate your formalization.

The Map type is defined in https://git.eclipse.org/c/ocl/org.eclipse.ocl.git/tree/plugins/org.eclipse.ocl.pivot/model/OCL-2.5.oclstdlib

It might be interesting to see a conversion between *.oclstdlib / Isabelle declarations, perhaps of bodies too. See Boolean::not() etc.

Regards

Ed Willink
Re: Safe OCL [message #1804759 is a reply to message #1804751] Sun, 31 March 2019 17:19 Go to previous messageGo to next message
Denis Nikiforov is currently offline Denis NikiforovFriend
Messages: 218
Registered: August 2013
Senior Member
I agree that all this stuff should be described in such a way that it does not require knowledge of Isabelle HOL.

Could you please explain the meaning of "validating" and "invalidating" annotations in the oclstdlib file?

My theory doesn't contain the following things:

  • metatypes (BagType, PrimitiveType, etc.) - they are important for the layered MOF architecture. However they doesn't affect typing rules or semantics. So, I don't model them
  • type properties and static properties (allLiterals, elementType) - from my point of view, they are used actively in the OCL specification, but not in a usual OCL expressions. Therefore, I have not modeled them in the first place.
  • coercions (toUnlimitedNatural) - I think I will add them to expression normalization rules, which applied to an AST before type analysis
  • abstract types or interfaces (OclComparable) - they are important from the implementation point of view. But I afraid, that they will complicate the theory
  • OclType - required only for a few reflexive operations and complicates the logical theory
  • operation body specifications - it related to language semantics. At this moment I'm trying to describe typing rules only. Semantics is the next big step. Actually my theory allows specification of user-defined operation bodies (there are some examples in Chapter 8). But I think that I must use another approach for standard operations belonging to the language core.

Also my theory defines a much stronger typing rules, than rules given in the oclstdlib file. For example consider the union operation:
abstract type UniqueCollection(T) : CollectionType conformsTo Collection(T) {
	operation union(s : UniqueCollection(T)) : Set(T) => 'org.eclipse.ocl.pivot.library.collection.CollectionUnionOperation';
}

All 3 collections (source, argument, and result) has the same element type T.
But in my theory source and argument collections could have totaly unrelated element types (T and S). And the element type of the resulting collection is a least super type of S and T. I don't understand how to express this typing rule in the oclstdlib file.

In short:

  • It's hard to model MOF-like multiple layers of models, metamodels, ..., reflexive operations, etc. in the logical model. I think it's possible, but it complicates the theory. And it's not required, because I don't use this reflexive operations and static type properties in the language specification. They are defined directly in the theory as a usual Isabelle HOL functions
  • Abstract types or interfaces aren't required in the theory, because they only complicates it.
  • Most of the typing rules can't be expressed in oclstdlib.

In other words I think that there can't be a one-to-one correspondence between a logical theory and an object-oriented model. They are based on different approaches.

On the other hand, Isabelle HOL supports Haskell, ML, and even Scala code generation from a logical theory. So I think that a type analysis code, parser, or even OCL interpreter could be generated from the specification.

Anyway I want to finish the theory without all this complicated reflexive and metamodel stuff. Then I think that some kind of a bridge between the logical specification and oclstdlib should be created. Maybe it should be a transformation from the specification to oclstdlib, or it should be a tool which check that oclstdlib conforms to the logical specification, or something else.


On synchronization of the specification and implementation. Nobody knows what will happen 3 years later. I think it will be still interesting for me. Anyway I'm trying to make this theory as simple as possible. So it can be reimplemented on another specification language (Coq, etc.), or extended with just a basic experience of Isabelle HOL.
Re: Safe OCL [message #1804782 is a reply to message #1804751] Mon, 01 April 2019 08:08 Go to previous messageGo to next message
Ed Willink is currently offline Ed WillinkFriend
Messages: 6538
Registered: July 2009
Senior Member
Hi

Quote:
Could you please explain the meaning of "validating" and "invalidating" annotations in the oclstdlib file?


invalidating: a function such as divide-by-zero or at-minus-one that may return invalid from valid source+arguments.

validating: a function such as oclIsInvalid that may return non-invalid from invalid source+arguments.

Otherwise:

all non-invalid source+arguments => non-invalid result
any invalid source+arguments => invalid result

(The UnlimitedNatural-is-not-a-subtype-of-Integer conclusion arises from precisely your kind of type analysis. If something is really painful, then it may well justify revision/clarification.)

Regards

Ed Willink
Re: Safe OCL [message #1804904 is a reply to message #1804782] Wed, 03 April 2019 07:01 Go to previous messageGo to next message
Denis Nikiforov is currently offline Denis NikiforovFriend
Messages: 218
Registered: August 2013
Senior Member
Hi

Could you please clarify what types can be used for a Map keys? I'm sure that Boolean, Integer, String, enums and objects are ok for keys.

I'm not so sure on Real (if it's precise, not approximate, then it can be used I guess) and UnlimitedNatural (because of infinity).

Collections, tuples and maps most probably can't be used for keys, because they requires a complicated hash calculation algorithm? Or they can be used and compared by reference, not by value?
Re: Safe OCL [message #1804916 is a reply to message #1804904] Wed, 03 April 2019 09:19 Go to previous messageGo to next message
Ed Willink is currently offline Ed WillinkFriend
Messages: 6538
Registered: July 2009
Senior Member
Hi

No restriction. They are just template types.

Obviously Map(Real,Real) just like Set(Real) will be of dubious implementation dependent utility.

But I think every programmer in any language learns that "aReal == 1.0" or printf("%f", aReal) gives off-by-epsilon effects.

Class-typed values are always equal by object identity (memory address in practice). This 'simple' concept seemed to be problematic for Featherweight OCL. I suspect that the identity/address has to be an explicitly modeled immutable 'object field' in Isabelle, rather than a memory allocation side effect in a real implementation.

DataType-typed values may be arbitrarily re-used, sometimes e.g. Integer by copying, sometimes e.g. String by sharing; an implementation choice. They therefore have no guaranteed unique memory address and so are compared by deep value.

Collections are DataTypes, so two collections at different memory addresses are compared by deep value. Yes an implementation can be very inefficient.

It is this distinction between DataType-typed and Class-typed 'value' that causes so much difficulty when trying to treat both as OclAny and passing them to operations. The Class-typed element is passed by reference, the DataType-typed element by value; this is not polymorphic. Not too bad in OCL where the recipient is side-effect free, but in QVTo somehow the recipient must be able to change a List(T) argument that was passed by value! IIRC QVT 1.3 requires that a reference-to-value is used for inout parameters.

Regards

Ed Willink
Re: Safe OCL [message #1805003 is a reply to message #1804916] Thu, 04 April 2019 13:12 Go to previous messageGo to next message
Denis Nikiforov is currently offline Denis NikiforovFriend
Messages: 218
Registered: August 2013
Senior Member
Hi

Thanks for the answer! It's good, because it simplifies the type system.

Could you please clarify the typing of closure iteration? Here is a signature from oclstdlib:
type Set(T) : SetType conformsTo UniqueCollection(T) {
	iteration closure(i : T[1] | lambda : Lambda T() : Set(T)) : Set(T) => 'org.eclipse.ocl.pivot.library.iterator.ClosureIteration';
}

According to the definition a body (a lambda expression) should return a collection (Set(T) in this case).

But according to the Section 11.9.1 of the OCL specification:
source->closure(iterator | body) =
  anonRecurse(source, Result{})

where:
anonRecurse is an invocation-site-specific helper function synthesized by lexical substitution of iterator, body, add, and Result in:

context OclAny
def: anonRecurse(anonSources : Collection(T), anonInit : Result(T)) : Result(T) =
  anonSources->iterate(iterator : T; anonAcc : Result(T) = anonInit |
    if anonAcc->includes(iterator)
    then anonAcc
    else let anonBody : OclAny = body in
      let anonResults : Result(T) = anonAcc->add(iterator) in
      if anonBody.oclIsKindOf(CollectionType)
      then anonRecurse(anonBody.oclAsType(Collection(T)), anonResults)
      else anonRecurse(anonBody.oclAsType(T)->asSet(), anonResults)
      endif
    endif)

anonBody can have a single value:
anonBody.oclAsType(T)->asSet()

The question is can the body have a single value or it should be a collection-typed?

Originally, I implemented the variant from the OCL specification. But now I'm not sure that it's right.
Re: Safe OCL [message #1805018 is a reply to message #1805003] Thu, 04 April 2019 15:40 Go to previous messageGo to next message
Ed Willink is currently offline Ed WillinkFriend
Messages: 6538
Registered: July 2009
Senior Member
Hi

As you can see, the specification uses the language of textual macros to explain the lambdas of closure. It is not executable. It is a paraphrase of the modeling in OCL-2.5.oclstdlib which contributes to real OCL tooling and type checking. I would therefore tend to go with the OCL-2.5.oclstdlib modeling augmented by the yet-to-be-modelled functionality in org.eclipse.ocl.pivot.internal.manager.TemplateParameterSubstitutionHelper.

It is certainly possible for a singleton body value of type T to be auto-converted to a Set(T), but long experience has shown me that this undermines the type system. What if T is a Set(Z)? There is an irregularity, just as with "collect" necessitating a "collectNested" to fix the language design bug. I therefore work hard to relegate 'helpful' type conversions to the CS level and hopefully eliminate them there too.

Regards

Ed Willink

Re: Safe OCL [message #1805888 is a reply to message #1805018] Fri, 26 April 2019 16:16 Go to previous messageGo to next message
Denis Nikiforov is currently offline Denis NikiforovFriend
Messages: 218
Registered: August 2013
Senior Member
Hi

I have some news on the specification. Actually I defined all these types (nullable collections, errorable types, maps). I added all of the operations from the oclstdlib to the theory (includingAll, includesMap, ...). I defined a pseudo-OCL syntax for abstract syntax trees, so examples are much more redable now.

And also I removed complicated type manipulation functions from the theory. For example there was an element_type function which takes a collection type and returns its element type. There was also an update_element_type function, which changes an element of a collection type an so on. Without these functions the typing rules are much simpler now. As you can see, most of the typing rules on the main page contains only 2 type operations: type conformance check (<) and calculation of a least common supertype of two types (⊔).

However to achieve it I had to define some pseudo-types: Iterable, NonIterable, NonCollection, UniqueCollection, ... The good thing is that the theory is very similar to your oclstdlib file. The bad thing is that all of these types are not part of the type system. Actually it's just type operations, for example the Iterable operation checks that a type is either a collection type, or a map type.

I think that I should add all these pseudo-types to the type system. However I think it will take a month or so to refactor the type system one more time.
Re: Safe OCL [message #1805889 is a reply to message #1805888] Fri, 26 April 2019 16:22 Go to previous message
Denis Nikiforov is currently offline Denis NikiforovFriend
Messages: 218
Registered: August 2013
Senior Member
I've also forget to note. I added a normalization rules for the closure iteration. You can see them in the last section on the main page. Dependent on the context oclAsSet(), selectByKind(), if/then/else are added to the closure body. However all of these rules are very preliminary. I will recheck them when I'll finish the theory.
Previous Topic:how to reach OCLMessage from OCL API?
Next Topic:NPE while loading OCL file
Goto Forum:
  


Current Time: Sat Dec 14 10:59:56 GMT 2019

Powered by FUDForum. Page generated in 0.03222 seconds
.:: Contact :: Home ::.

Powered by: FUDforum 3.0.2.
Copyright ©2001-2010 FUDforum Bulletin Board Software

Back to the top