Pre-/Postconditions Semantics
The semantics of SSE pre-/postconditions is to understand as follows:
- Pre-/Postconditions are always defined for a single operations.
- Pre-/Postconditions follow the principle of design-by-contract.
In this contract for an operation, a precondition defines conditions, which have to hold for the execution of the operation, and a postcondition defines conditions, which have to hold after the execution of the operation.
- In SSE, we allow to define several pre- or postconditions, which are conjuncted into a single pre- or post-condition correspondingly.
- SSE pre-/postconditions are defined over the parameters of the operation they belong to.
Furthermore, they can be defined over additional objects (called variables in the grammar), which have data types coming from either an ontology used for the data types in the operation or from any other ontology.
- Conditions on properties of the parameters and additional variables are expressed by predicates.
Predicates are modelled as object or data properties in an ontology.
Only predicates defined in referenced ontology(ies) are allowed in SSE pre-/postconditions.
- In SSE conditions, no multiple variable definitions are allowed in one pre- oder postcondition because it leads to an ambiguous usage of such variables.
- Parameters from the corresponding operation signature are allowed te be used in conditions, however, there should not be any duplicated variable definitions of them.
- No data types for variables that are not a part of the referenced ontology(ies) are allowed.
- No undefined variables (variables without a corresponding data type) are allowed in conditions.
- Data types of variables used in predicates have to correspond to data types that those predicates expect at a certain place.
For example, for a predicate belongsTo(Room, Building) with two places (domain and range in OWL), the first variable used have to be of data type of domain, e.g., Room, and the second variable have to be of data type of range, e.g., Building.
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:
-
A variable is defined with the same name as another variable or signature parameter.
-
A variable is defined with an illegal name (only consists of numbers or is surrounded by quotation marks).
-
In a variable definition a data type is used which is not present in any of the ontologies of any signature parameter.
-
The first variable of a predicate is neither one of the signature parameters nor defined in a variable definition.
-
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).
-
The identifier of a predicate is not an ontology property of the data type of the first variable of the predicate.
-
The second variable of a predicate is not in the range of the ontology property of the data type of the first variable.
-
A predicate of a precondition contains outgoing one or more signature parameters as variables.
-
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.