de.uka.ilkd.key.symbolic_execution.util

Class SymbolicExecutionSideProofUtil.ContainsModalityOrQueryVisitor

java.lang.Object

de.uka.ilkd.key.logic.DefaultVisitor

de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil.ContainsModalityOrQueryVisitor

All Implemented Interfaces:

Visitor

Enclosing class:

SymbolicExecutionSideProofUtil

protected static class SymbolicExecutionSideProofUtil.ContainsModalityOrQueryVisitor
extends DefaultVisitor

Utility method used by QuerySideProofRule#containsModalityOrQuery(Term).

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
(package private) boolean	containsModalityOrQuery The result.

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	ContainsModalityOrQueryVisitor()

Method Summary

Modifier and Type	Method and Description
boolean	isContainsModalityOrQuery() Returns the result.
void	visit(Term visited) the entry method for the visitor pattern

Methods inherited from class de.uka.ilkd.key.logic.DefaultVisitor

subtreeEntered, subtreeLeft, visitSubtree

Methods inherited from class java.lang.Object

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

Field Detail

containsModalityOrQuery

boolean containsModalityOrQuery

The result.

Constructor Detail

ContainsModalityOrQueryVisitor

protected ContainsModalityOrQueryVisitor()

Method Detail

visit

public void visit(Term visited)

the entry method for the visitor pattern

Parameters:

visited - the Term to be visited

isContainsModalityOrQuery

public boolean isContainsModalityOrQuery()

Returns the result.

Returns:

true contains at least one modality or query, false contains no modalities and no queries.