A pre or a post condition is a boolean expression that may be a simple equality checking or a lambda expression. The Kermeta interpreter evaluates the body content like a boolean result

The "pre condition" are declared just before the "is" of the operation body

operation opName(c : String) : String
    
    // Declaration of the pre-condition
    pre notVoidInput is do
        c != void and c != ""
    end

    // Declaration of the post-condition
    post notVoidOutput is
        result != void and result != ""

is
    do
        // operation body
    end

An invariant constraint is declared anywhere in a ClassDefinition block.

An invariant declaration is a boolean expression that may be a simple equality checking or a lambda expression. The Kermeta interpreter evaluates the body content like a boolean result.

A very simple example :

class className {

    ...

    // Declaration of the invariant : deterministicTransition
    inv nameOfTheInvariant is do
        self.name != ""
    end

    ...
}

A lambda expression can be used into an invariant declaration:

// Declaration of the invariant : deterministicTransition
inv deterministicTransition is do
    self.outgoingTransition.forAll{tr1 |
        self.outgoingTransition.forAll{ tr2 |
            ( tr2.input==tr1.input ) == (tr1==tr2)
        }
    }
end

The activation of the checking of the pre - post conditions depends of the run configuration, see the Kermeta UI user guide for more information.

If the boolean statement is evaluated to "false" then the pre or post condition is violated and an exception ConstraintViolatedPre or ConstraintViolatedPost is raised.

In order to check the well-formedness rules of a model element, there are two methods in Kermeta. The first-one : checkInvariants , consists to check only the current model element and the second-one : checkAllInvariants , checks recursively the element being a containment link with the checked element.

theModelElement.checkInvariants

The checkAllInvariants operation is a recursive method which checks all the elements having a containment relation by transitivity with the checked element.

checkAllInvariants is used especially to check the validity of a model fragment or a complete model.

theModelElement.checkAllInvariants

If the boolean statement is evaluated to " false " then the invariant constraint is violated and an exception ConstraintViolatedInv is raised. This exception can be handled by a rescue call.

// Call the invariant verification
do
    theModelElement.checkInvariants
    rescue (err : ConstraintViolatedInv)
        stdio.writeln(err.toString)
        stdio.write(err.message)
end