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:
     '<=>';