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

Class ForallAstVisitor

java.lang.Object

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

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

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

All Implemented Interfaces:

AstVisitor<java.lang.Boolean>, ExprVisitor<za.ac.sun.cs.green.expr.Expression>

public class ForallAstVisitor
extends AstIterVisitor<java.lang.Boolean>

Field Summary

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

combine, defaultVal, eva, exprVisitor

Constructor Summary

Constructors

Constructor and Description
ForallAstVisitor(ForallExprVisitor v) Visits all statements for checking invariants over statements.

Method Summary

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

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

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

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

ForallAstVisitor

public ForallAstVisitor(ForallExprVisitor v)

Visits all statements for checking invariants over statements.

Parameters:

v -