Module dev.civl.mc

Package dev.civl.mc.model.IF.expression

Interface QuantifiedExpression

All Superinterfaces:

Expression, Sourceable

public interface QuantifiedExpression
extends Expression

A CIVL-C quantified expression, including three components, bound variable declaration list, (optional) restriction and expression. It has the following syntax:

 quantified: 
   quantifier ( variable-decl-list | restrict? ) expression ;
 
 variable-decl-list:
   variable-decl-sub-list (; variable-decl-sub-list)* ;
   
 variable-decl-sub-list:
   type ID (, ID)* (: domain)?
   
 quantifier: $forall | $exists | $uniform
 

e.g.,

 $forall (int x, y: dom; double z | x > 0 invalid input: '&'invalid input: '&' zinvalid input: '<'5.9) x*z > -1
 

Nested Class Summary

Nested Classes

Modifier and Type	Interface	Description
static enum	QuantifiedExpression.Quantifier	The different kinds of quantifiers which are possible.

Nested classes/interfaces inherited from interface dev.civl.mc.model.IF.expression.Expression

Expression.ExpressionKind

Method Summary

Modifier and Type	Method	Description
List<Pair<List<Variable>,Expression>>	boundVariableList()	The list of bound variables.
Expression	expression()	The expression e(x).
int	numBoundVariables()
QuantifiedExpression.Quantifier	quantifier()
Expression	restriction()	Boolean-valued expression assumed to hold when evaluating expression.

Methods inherited from interface dev.civl.mc.model.IF.expression.Expression

calculateConstantValue, calculateDerefs, constantValue, containsHere, expressionKind, expressionScope, freeVariables, getExpressionType, hasConstantValue, hasDerefs, isErrorFree, isPurelyLocal, lowestScope, purelyLocalAnalysis, purelyLocalAnalysisOfVariables, replaceWith, replaceWith, setErrorFree, variableAddressedOf, variableAddressedOf

Methods inherited from interface dev.civl.mc.model.IF.Sourceable

getSource, setCIVLSource

Method Details

quantifier

QuantifiedExpression.Quantifier quantifier()

Returns:

The quantifier binding the variable.

boundVariableList

List<Pair<List<Variable>,Expression>> boundVariableList()

The list of bound variables.

Returns:

restriction

Expression restriction()

Boolean-valued expression assumed to hold when evaluating expression.

expression

Expression expression()

The expression e(x).

numBoundVariables

int numBoundVariables()