Module dev.civl.sarl

Package dev.civl.sarl.IF

Class CoreUniverse.ForallStructure

java.lang.Object

dev.civl.sarl.IF.CoreUniverse.ForallStructure

Enclosing interface:

CoreUniverse

public static class CoreUniverse.ForallStructure
extends Object

The result of analyzing certain "forall" expressions. The expression must be equivalent to

 forall int i . lowerBound invalid input: '<'= i invalid input: '<'= upperBound -> body
 

Field Summary

Fields

Modifier and Type	Field	Description
BooleanExpression	body	The body of the expression: the boolean formula that is claimed to hold if i is between the lower and upper bounds (inclusive).
NumericSymbolicConstant	boundVariable	The integer bound variable used in the forall expression.
NumericExpression	lowerBound	The lower bound (inclusive) of the bound variable.
NumericExpression	upperBound	The upper bound (inclusive) of the bound variable.

Constructor Summary

Constructors

Constructor	Description
ForallStructure()

Method Summary

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Details

boundVariable

public NumericSymbolicConstant boundVariable

The integer bound variable used in the forall expression.

lowerBound

public NumericExpression lowerBound

The lower bound (inclusive) of the bound variable.

upperBound

public NumericExpression upperBound

The upper bound (inclusive) of the bound variable.

body

public BooleanExpression body

The body of the expression: the boolean formula that is claimed to hold if i is between the lower and upper bounds (inclusive).

Constructor Details

ForallStructure

public ForallStructure()