-
Key: KERML-186
-
Status: open
-
Source: Model Driven Solutions ( Mr. Ed Seidewitz)
-
Summary:
The semantics of an Invariant are given by its implicit specialization of one of two features in the Performances library model: either trueEvaluations or (if the Invariant is negated) falseEvaluations. These features bind the values true and false, respectively, to their result parameter. This gives the Invariant the semantics that, to be consistent, the result expression actually given in the Invariant must evaluate to true or false (respectively).
The result bindings for trueEvaluations and falseEvaluations are currently specified using ResultExpressionMemberships (to the expressions "true" and "false", respectively). However, the approved resolution to issue
KERML-20included adding the validateExpressionResultExpressionMembership constraint, which requires that an Expression has at most one ResultExpressionMembership among all its memberships, owned and inherited. In a typical Invariant of the form inv {invariantExpression}, the invariantExpression is parsed as being owned by the Invariant via a ResultExpressionMembership. But this now violates the validateExpressionResultExpressionMembership constraint, because it conflicts with the ResultExpressionMembership inherited from trueEvaluations (or falseEvaluations, if the invariant were negated). -
Reported: KerML 1.0b1 — Sat, 23 Sep 2023 22:27 GMT
-
Updated: Mon, 8 Apr 2024 21:42 GMT
KERML — Update semantic model of invariants for validateExpressionResultExpressionMembership constraint
- Key: KERML-186
- OMG Task Force: Kernel Modeling Language (KerML) 1.0 FTF