Module dev.civl.mc

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

Interface ArrayLambdaExpression

All Superinterfaces:

Expression, Sourceable

public interface ArrayLambdaExpression
extends Expression

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

 array-lambda: 
   $lambda ( variable-decl-list | restrict? ) expression ;
 
 variable-decl-list:
   variable-decl-sub-list (; variable-decl-sub-list)* ;
   
 variable-decl-sub-list:
   type ID (, ID)* (: domain)?
 
 

e.g.,

 (int[n]) $lambda (int i) i*4
 

Nested Class Summary

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).
CIVLCompleteArrayType	getExpressionType()
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, 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

boundVariableList

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

The list of bound variables. TODO: WHAT IS THE Expression for?

Returns:

restriction

Expression restriction()

Boolean-valued expression assumed to hold when evaluating expression.

expression

Expression expression()

The expression e(x).

getExpressionType

CIVLCompleteArrayType getExpressionType()

Specified by:

getExpressionType in interface Expression

Returns:

The type of this expression. For a primitive or variable, this is the type of the primitive or variable. For a cast expression it is the cast type. For operations it is the type of the operation result.