Module dev.civl.abc

Package dev.civl.abc.ast.node.IF.acsl

Interface ExtendedQuantifiedExpressionNode

All Superinterfaces:

ASTNode, ExpressionNode, ForLoopInitializerNode, InitializerNode, SizeableNode

public interface ExtendedQuantifiedExpressionNode
extends ExpressionNode

This represents an ACSL extended quantification expression. Section 2.6.7 from ACSL standards Extended quantifiers Terms \quant(t1,t2,t3) where quant is max, min, sum, product or numof are extended quantifications. t1 and t2 must have type integer, and t3 must be a unary function with an integer argument, and a numeric value (integer or real) except for \numof for which it should have a boolean value. Their meanings are given as follows:

 \max(i,j,f) = max{f(i), f(i+1), ..., f(j)}
 \min(i,j,f) = min{f(i), f(i+1), ..., f(j)}
 \sum(i,j,f) = f(i) + f(i+1) + ... + f(j)
 \product(i,j,f) = f(i) * f(i+1) * ... * f(j)
 \numof(i,j,f) = #{k | iinvalid input: '<'=kinvalid input: '<'=j ^ f(k)} = \sum(i, j, \lambda integer k ; f(k) ? 1 : 0)
 

If i>j then \sum and \numof above are 0, \product is 1,and \max and \min are unspecified.

Nested Class Summary

Nested Classes

Modifier and Type	Interface	Description
static enum	ExtendedQuantifiedExpressionNode.ExtendedQuantifier

Nested classes/interfaces inherited from interface dev.civl.abc.ast.node.IF.ASTNode

ASTNode.NodeKind

Nested classes/interfaces inherited from interface dev.civl.abc.ast.node.IF.expression.ExpressionNode

ExpressionNode.ExpressionKind

Method Summary

Modifier and Type	Method	Description
ExtendedQuantifiedExpressionNode.ExtendedQuantifier	extQuantifier()	returns the extended quantifier of this expression
ExpressionNode	function()	return the function
ExpressionNode	higher()	return the higher bound
ExpressionNode	lower()	return the lower bound

Methods inherited from interface dev.civl.abc.ast.node.IF.ASTNode

addAllTransformAnnotations, addTransformAnnotation, child, childIndex, children, diff, equiv, getAttribute, getOwner, getScope, getSource, id, keepOnly, nextDFS, nodeKind, numChildren, parent, prettyPrint, prettyRepresentation, prettyRepresentation, print, remove, removeChild, removeTransformAnnotation, setAttribute, setChild, setId, setOwner, setScope, toString, transformAnnotations

Methods inherited from interface dev.civl.abc.ast.node.IF.expression.ExpressionNode

addConversion, copy, expressionKind, getConversion, getConvertedType, getInitialType, getNumConversions, isConstantExpression, isLvalue, removeConversions, setInitialType

Methods inherited from interface dev.civl.abc.ast.node.IF.declaration.InitializerNode

isSideEffectFree

Methods inherited from interface dev.civl.abc.ast.node.IF.expression.SizeableNode

getType

Method Details

lower

ExpressionNode lower()

return the lower bound

Returns:

return the lower bound

higher

ExpressionNode higher()

return the higher bound

Returns:

return the higher bound

function

ExpressionNode function()

return the function

Returns:

return the function

extQuantifier

ExtendedQuantifiedExpressionNode.ExtendedQuantifier extQuantifier()

returns the extended quantifier of this expression

Returns:

the extended quantifier of this expression