de.unisaarland.cs.st.jerify.verifier.typestate
Class State

java.lang.Object
  de.unisaarland.cs.st.jerify.verifier.typestate.State

public class State
extends java.lang.Object

The State class represents a State in the typestate analysis.

Author:

Daniel Wand (typestate@ewand.de)

Field Summary

static java.lang.String	ErrorState The name of the State that represents an error state
static java.lang.String	UnkownState The name of the State that represents an uninitialized state

Constructor Summary

State()
Create a new empty State

State(java.util.Collection<java.lang.String> startStates)
Creates a State which is initialized to a collection of possibles states

State(State s)
Create a copy of s

State(java.lang.String startState)
Create a State which is initialized to one state

Method Summary

State	applyStateChange(StateChanges stateChanges, com.sun.source.tree.Tree tree) Takes a Mapping from State to states , and applies it to the current Set of states by returning the new State.
boolean	equals(java.lang.Object o)
void	filter(java.util.Collection<java.lang.String> filterSet) filters the States of this State, so that only States that also occur in the filter set are present
boolean	isSubsetOf(State otherState) Check whether this state is a subset of an other State.
State	merge(State otherState) Includes the information in the other State into this State
java.lang.String	toString()

Methods inherited from class java.lang.Object

getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

UnkownState

public static final java.lang.String UnkownState

The name of the State that represents an uninitialized state

See Also:

Constant Field Values

ErrorState

public static final java.lang.String ErrorState

The name of the State that represents an error state

See Also:

Constant Field Values

Constructor Detail

State

public State()

Create a new empty State

State

public State(java.lang.String startState)

Create a State which is initialized to one state

Parameters:

startState - the initialized State

State

public State(java.util.Collection<java.lang.String> startStates)

Creates a State which is initialized to a collection of possibles states

Parameters:

startStates - the initialized States

State

public State(State s)

Create a copy of s

Parameters:

s - the State to make a copy of

Method Detail

merge

public State merge(State otherState)

Includes the information in the other State into this State

Parameters:

otherState - the State to include

Returns:

this with the other state incorporated

isSubsetOf

public boolean isSubsetOf(State otherState)

Check whether this state is a subset of an other State.

Parameters:

otherState -

Returns:

if this State is a subset of the otherState

applyStateChange

public State applyStateChange(StateChanges stateChanges,
                              com.sun.source.tree.Tree tree)

Takes a Mapping from State to states , and applies it to the current Set of states by returning the new State. There may be no state in the current State that is not mapped to a new State. If there is one this is reported as an error. Not all conversions must map, but one must.

Parameters:

conversion - The changes that are to be applied.

tree - The part of the code that caused the state changes to be applied (for error reporting).

Returns:

The new States we might be in.

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class java.lang.Object

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

filter

public void filter(java.util.Collection<java.lang.String> filterSet)

filters the States of this State, so that only States that also occur in the filter set are present

Parameters:

filterSet - the additional information that only these states are possible