fmrisc.ProofNavigator.Semantics

Class BoundVariables

java.lang.Object

fmrisc.ProofNavigator.Syntax.ASTVisitorBase

fmrisc.ProofNavigator.Semantics.BoundVariables

All Implemented Interfaces:

ASTVisitor

public final class BoundVariables
extends ASTVisitorBase

Compute the variables bound within an expression.

Constructor Summary

Constructors

Constructor and Description
BoundVariables()

Method Summary

Modifier and Type	Method and Description
static java.util.Vector<java.lang.String>	compute(Expression exp) Compute variables bound some quantifier within an expression.

Methods inherited from class fmrisc.ProofNavigator.Syntax.ASTVisitorBase

isCloned, visit

Methods inherited from class java.lang.Object

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

Constructor Detail

BoundVariables

public BoundVariables()

Method Detail

compute

public static java.util.Vector<java.lang.String> compute(Expression exp)

Compute variables bound some quantifier within an expression.

Parameters:

exp - an expression.

Returns:

a vector of Strings representing the names of the variables bound by some quantifier within the expression (each string occurs once in the vector).