gov.nasa.jpf.symbc.veritesting.ast.visitors

Class ForallExprVisitor

java.lang.Object

gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor<java.lang.Boolean>

gov.nasa.jpf.symbc.veritesting.ast.visitors.ForallExprVisitor

All Implemented Interfaces:

ExprVisitor<java.lang.Boolean>

Direct Known Subclasses:

ValidGreenPredicate

public class ForallExprVisitor
extends ExprIterVisitor<java.lang.Boolean>

A visitor that enforces invariant checking on all expressions by passing the operation and expected result.

Field Summary

Fields inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

combine, defaultVal, eva

Constructor Summary

Constructors

Constructor and Description
ForallExprVisitor()

Method Summary

Methods inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Methods inherited from class java.lang.Object

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

Constructor Detail

ForallExprVisitor

public ForallExprVisitor()