Type check error message with the RTESC WG AADL Library

Syside Bug Reports
, ,
1

Hi, I am using Syside 0.8.1 to test the SMC RTESC WG AADL library. I have many similar errors.

The following is a reproducer:

package syside_issue_1 {

    attribute def foo :> ScalarValues::Positive {}

    part def bar {
        attribute foo_bar : foo;
    }

    part def baz :> bar {
        :>> foo_bar = 42; // error here
    }
}

I get the following error: “ScalarValues::Positive does not conform to syside_issue_1::foo”

I do not have this error with the Reference Implementation.

I have all types of variants of this error message.

2

Hi @Jerome_Hugues,

This is an intended type checker diagnostic as foo is a subset of Positive, meaning that not all Positive values can also be foo which would break type/interface contracts at runtime if there was one. This diagnostic can be silence with new foo(42).

3

Indeed, it silences the error message. I presume the issue has to be discussed with other tool vendors as the validity of models should be consistent across vendors.

I understand your notion of subsetting is closer to Ada typing where you force explicit type to be mentioned while the reference implementation may either check that in the absence of an additional constraint as any Positive is also a valid value for foo; or does not check anything (which is confirmed if I put -42 as a value)

Note that Syside does not reject :>> foo_bar = new foo(-42);which obviously violates the predicate that it should be positive. It is also true that the KerML library file does not specify any constraint for Positive like Ada does .. (yes, I am an Ada fan)

4

Including the specification. It currently lacks any type checking rules that would apply to assignments and such.

This is also consistent with every common typed programming language. They do not allow assignments of values to more derived types while assigning a more derived type is accepted.

This stems from the specification that forces -42 to be assigned to self implicitly which is inherited from DataValue and is typed by DataValue. The biggest problem is that self (similarly to this and that) is a library feature instead of a keyword which requires relatively expensive checks to infer.

Currently, type checking is enabled only for assignments through FeatureValues, invocation/constructor arguments included, so it may not cover all cases.

5

Thanks. We are in full agreement here when it comes to the missing rules in the standard document. This is also something we experiment in the definition of the RTESC WG AADL library.

Yet, from a user perspective, we have to think about a typeckecking mechanism that would avoid having new. It is natural for Software Engineers, not for Systems Engineers. I get this is not in the spec as of today.