BoundExpressionIF.java

package edu.udel.cis.vsl.tass.model.IF.expression;

import edu.udel.cis.vsl.tass.model.IF.variable.BoundVariableIF;

/**
 * A bound expression is an expression built around a bound variable, such as
 * "forall x such that 0<x<10, x*y>z". In that expression x is the bound
 * variable, bound by the operator "forall". The expression "0<x<10" is the
 * "bound restriction". The expression "x*y>z" is the "expression". The type of
 * a forall expression is boolean.
 * 
 * Other operators, in addition to forall, are exists and lambda. Exists is
 * exactly like forall.
 * 
 * Lambda is used in the sense of the lambda calculus. It has the form
 * "lambda(x).e(x)". It represents the function that, when given x, returns the
 * result of evaluating e(x). The type of the expression if function from S to
 * T, where S is the type of x and T is the type of e.
 * 
 * */
public interface BoundExpressionIF extends ExpressionIF {

	/**
	 * The different kinds of quantifiers which are possible. FORALL: the
	 * universal quantifier, EXISTS: the existential quantifier. LAMBDA: used to
	 * represent a lambda expression.
	 */
	public enum Quantifier {
		FORALL, EXISTS, LAMBDA
	};

	/** The operator binding the variable: forall, exists, or lambda. */
	Quantifier operator();

	/** The bound variable (x). */
	BoundVariableIF boundVariable();

	/** Boolean-valued expression assumed to hold when evaluating expression. */
	ExpressionIF boundRestriction();

	/** The expression e(x). */
	ExpressionIF expression();
}