edu.buffalo.cse.jive.ui.search.queries
Class InvariantViolatedSearchQuery

java.lang.Object
  edu.buffalo.cse.jive.ui.search.AbstractJiveSearchQuery
      edu.buffalo.cse.jive.ui.search.ExecutionHistorySearchQuery
          edu.buffalo.cse.jive.ui.search.queries.InvariantViolatedSearchQuery

All Implemented Interfaces:

SequenceModel.EventVisitor, IJiveSearchQuery, ISearchQuery

public class InvariantViolatedSearchQuery
extends ExecutionHistorySearchQuery

An IJiveSearchQuery that is used to check whether a class invariant was violated. The check occurs at the return of each method of the class. The query is capable of checking for invariant violations on a single instance or over all instances of a class (if an instance number is not provided).

Nested Class Summary

protected class

InvariantViolatedSearchQuery.AssignEventExporter An exporter used to examine AssignEvents and to determine if the event is an assignment to a variable represented by a JiveSearchPattern.

Field Summary

protected InvariantViolatedSearchQuery.AssignEventExporter	assignmentExporter An exporter used to examine AssignEvents.
protected Map<String,Value>	instanceToLeftValueMap A mapping between an instance number and a value currently assigned with the variable of the left search pattern.
protected Map<String,Value>	instanceToRightValueMap A mapping between an instance number and a value currently assigned with the variable of the right search pattern.
protected JiveSearchPattern	leftPattern A search pattern for the invariant's left operand.
protected RelationalOperator	operator The invariant's relational operator.
protected JiveSearchPattern	rightPattern A search pattern for the invariant's right operand.

Constructor Summary

InvariantViolatedSearchQuery(JiveSearchPattern leftPattern, RelationalOperator operator, JiveSearchPattern rightPattern)
Constructs a new search query with the supplied patterns and relational operator.

Method Summary

protected void	checkForUpdates(AssignEvent event) Checks if the instance-to-value maps need updating.
protected boolean	checkInvariantViolated(MessageSend event) Checks whether the invariant was violated at the current point in the execution history.
ImageDescriptor	getImageDescriptor() Returns an ImageDescriptor used to represent the search query's result in the Search view's 'Show Previous Searches' tool bar action.
String	getResultLabel(int matchCount) Returns a label describing the search result used in the Search view.
Class<? extends Object>	getResultType() Returns the type of search result matches collected by the search query.
void	visit(EventOccurrence event) Visits an EventOccurrernce (other than a MessageSend).
void	visit(MessageSend event) Visits an occurrence of a MessageSend event.

Methods inherited from class edu.buffalo.cse.jive.ui.search.ExecutionHistorySearchQuery

addMatch, performSearch

Methods inherited from class edu.buffalo.cse.jive.ui.search.AbstractJiveSearchQuery

canRerun, canRunInBackground, createSearchResult, getLabel, getSearchResult, run

Methods inherited from class java.lang.Object

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

Field Detail

assignmentExporter

protected InvariantViolatedSearchQuery.AssignEventExporter assignmentExporter

An exporter used to examine AssignEvents.

leftPattern

protected JiveSearchPattern leftPattern

A search pattern for the invariant's left operand.

operator

protected RelationalOperator operator

The invariant's relational operator.

rightPattern

protected JiveSearchPattern rightPattern

A search pattern for the invariant's right operand.

instanceToLeftValueMap

protected Map<String,Value> instanceToLeftValueMap

A mapping between an instance number and a value currently assigned with the variable of the left search pattern. As the program's execution history is traversed by this visitor, the values in the map are updated.

instanceToRightValueMap

protected Map<String,Value> instanceToRightValueMap

A mapping between an instance number and a value currently assigned with the variable of the right search pattern. As the program's execution history is traversed by this visitor, the values in the map are updated.

Constructor Detail

InvariantViolatedSearchQuery

public InvariantViolatedSearchQuery(JiveSearchPattern leftPattern,
                                    RelationalOperator operator,
                                    JiveSearchPattern rightPattern)

Constructs a new search query with the supplied patterns and relational operator. The method names provided by the patterns are ignored. An instance number is optional.

Parameters:

leftPattern - the left operand

operator - the relational operator

rightPattern - the right operand

Method Detail

getResultType

public Class<? extends Object> getResultType()

Description copied from interface: IJiveSearchQuery

Returns the type of search result matches collected by the search query. This is used by the Search view to determine how to display the search result tabularly.

NOTE: This will be changed in the future. For now, return Event.class for a result containing matches of mixed event types or return the specific class literal for a result containing matches of a single event type (e.g., AssignEvent.class).

Specified by:

getResultType in interface IJiveSearchQuery

Overrides:

getResultType in class ExecutionHistorySearchQuery

Returns:

the type of search result matches

getResultLabel

public String getResultLabel(int matchCount)

Description copied from interface: IJiveSearchQuery

Returns a label describing the search result used in the Search view. Typically, this describes what is being searched for and the number of matches, as supplied by matchCount.

Parameters:

matchCount - the number of matches thus far

Returns:

a description of what is being searched

getImageDescriptor

public ImageDescriptor getImageDescriptor()

Description copied from interface: IJiveSearchQuery

Returns an ImageDescriptor used to represent the search query's result in the Search view's 'Show Previous Searches' tool bar action.

Returns:

an image descriptor representing the result

visit

public void visit(EventOccurrence event)

Description copied from interface: SequenceModel.EventVisitor

Visits an EventOccurrernce (other than a MessageSend).

Parameters:

event - the event occurrence being visited

visit

public void visit(MessageSend event)

Description copied from interface: SequenceModel.EventVisitor

Visits an occurrence of a MessageSend event.

Parameters:

event - the message send being visited

checkForUpdates

protected void checkForUpdates(AssignEvent event)

Checks if the instance-to-value maps need updating.

Parameters:

event - the event causing a change to a variable

checkInvariantViolated

protected boolean checkInvariantViolated(MessageSend event)

Checks whether the invariant was violated at the current point in the execution history. The supplied event wraps a ReturnEvent.

Parameters:

event - the message send wrapping a return event

Returns:

true if the invariant is violated, false otherwise