Pre-/Postconditions Semantics

The semantics of SSE pre-/postconditions is to understand as follows:

When adding a pre- or postcondition it is automatically checked for syntactic and semantic errors.
Read more about the syntax of SSE pre-/postconditions in Section Syntax of Pre-/Postconditions.

The semantic check alerts if:

  1. A variable is defined with the same name as another variable or signature parameter.
  2. A variable is defined with an illegal name (only consists of numbers or is surrounded by quotation marks).
  3. In a variable definition a data type is used which is not present in any of the ontologies of any signature parameter.
  4. The first variable of a predicate is neither one of the signature parameters nor defined in a variable definition.
  5. The second variable of a predicate is neither one of the signature parameters nor defined in a variable definition nor a constant (number or string).
  6. The identifier of a predicate is not an ontology property of the data type of the first variable of the predicate.
  7. The second variable of a predicate is not in the range of the ontology property of the data type of the first variable.
  8. A predicate of a precondition contains outgoing one or more signature parameters as variables.
  9. Constant values are correctly formatted. Strings need to have quotations on both sides, dates need to be YYYY-MM-DD formatted, timestamps as hh:mm:ss. The DateTime is formatted like YYYY-MM-DDThh:mm:ss. Date, Time and DateTime need to also have quotations on both sides like Strings. Booleans true and false are used without quotations.