Syntax of Pre-/Postconditions
The syntax of SSE pre-/postconditions is represented by an Xtext grammar.
This Xtext grammar models a language based on the first-order logic (FOL).
We apply the FOL on concepts and predicates from signatures and ontologies, over which one wants to define pre-/postconditions.
You find the grammar in the plug-in de.upb.crc901.sse.core.prepostconditions.FOL with org.eclipse.xtext.common.Terminals.
Generate fol "http://www.uni-paderborn.de/crc901/sse/core/fol".
Read more about the semantics of SSE pre-/postconditions in Section Pre-/Postconditions Semantics.
Condition:
condition=Expression;
Expression:
first=UnaryExpression (next=BinaryExpression)? | equiv=VariableEquivalence;
UnaryExpression:
ComplexExpression | NotExpression | QuantifiedExpression;
NotExpression:
NOT negated=ComplexExpression;
ComplexExpression returns Expression:
Predicate | '(' Expression ')';
QuantifiedExpression:
ForallExpression | ExistsExpression;
ForallExpression:
FORALL variables+=VariableDefinition (',' variables+=VariableDefinition)* quantifiedExpression=ComplexExpression;
ExistsExpression:
EXISTS variables+=VariableDefinition (',' variables+=VariableDefinition)* quantifiedExpression=ComplexExpression;
BinaryExpression:
Conjunction | Disjunction | Implication | Equivalence;
Conjunction:
AND next=ComplexExpression;
Disjunction:
OR next=ComplexExpression;
Implication:
IMPLY next=ComplexExpression;
Equivalence:
EQUIV next=ComplexExpression;
Predicate:
name=PredicateName '(' firstParam=VariableUsage (',' secondParam=VariableUsage)? ')';
VariableDefinition:
variable=Variable ':' datatype=Datatype;
VariableUsage:
variable= (Variable | Constant);
VariableEquivalence:
firstVariable=VariableUsage EQUIV secondVariable=VariableUsage;
PredicateName:
ID;
Constant:
INT | STRING;
Datatype:
ID;
Variable:
ID;
terminal EXISTS:
'exists';
terminal FORALL:
'forall';
terminal AND:
'&';
terminal OR:
'|';
terminal NOT:
'!';
terminal IMPLY:
'=>';
terminal EQUIV:
'<=>';