KerML 1.0b2 FTF Avatar
  1. OMG Issue

KERML — Invariants only hold when evaluated

  • Key: KERML-63
  • Status: open  
  • Source: NIST ( Mr. Conrad Bock)
  • Summary:

    Clauses 7.4.8.1 (Functions Overview) and 8.4.4.8.2 (Expressions and Invariants) say

    An invariant, though, is a boolean expression that must always evaluate to either true at all times or false at all times. By default, an invariant is asserted to always evaluate to true, while a negated invariant is asserted to always evaluate to false.

    Expressions are kinds of Steps. The checkExpressionSpecialization constraint requires that Expressions specialize the base Expression Performances::evaluations (see 9.2.6.2.3), which is a specialization of Performances::performances.

    the checkInvariantSpecialization constraint requires that Invariants specialize either the BooleanExpression Performances::trueEvaluations (see 9.2.6.2.2) or, if the Invariant is negated, the BooleanExpression Performances::falseEvaluations (see 9.2.6.2.2), both of which are specializations of Performances::booleanEvaluations.

    where the Performance library defines

    abstract expr trueEvaluations subsets booleanEvaluations { true }
    
    abstract expr falseEvaluations subsets booleanEvaluations { false }
    

    but do not require models to specify when invariant expressions are evaluated, which are the only times the results are required to be true/false. The conditions they test for might be present only when the invariants happen to be evaluated (see KERML-58 for more about this).

  • Reported: KerML 1.0a1 — Fri, 5 May 2023 13:55 GMT
  • Updated: Tue, 9 Apr 2024 23:30 GMT