de.uka.ilkd.key.symbolic_execution.util

Class SideProofStore

java.lang.Object

de.uka.ilkd.key.symbolic_execution.util.SideProofStore

public final class SideProofStore
extends java.lang.Object

The only instance of this class DEFAULT_INSTANCE is used to manage performed side proofs.

Side proofs are added via #disposeOrStore(String, ApplyStrategyInfo) when they are no longer needed. If the SideProofStore is enabled (isEnabled()) the side Proof is not disposed; instead it is added via addProof(String, Proof) and available for a later access until it is removed via removeEntries(Collection).

Author:

Martin Hentschel

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	SideProofStore.Entry An SideProofStore.Entry of a SideProofStore.

Field Summary

Fields

Modifier and Type	Field and Description
static SideProofStore	DEFAULT_INSTANCE The default and only instance of this class.
private boolean	enabled The enabled state.
private java.util.List<SideProofStore.Entry>	entries All contained SideProofStore.Entrys.
private java.util.List<ISideProofStoreListener>	listener All available ISideProofStoreListener.
private java.beans.PropertyChangeSupport	pcs The PropertyChangeSupport.
static java.lang.String	PROP_ENABLED Property isEnabled().

Constructor Summary

Constructors

Modifier	Constructor and Description
private	SideProofStore() Forbid other instances.

Method Summary

Modifier and Type	Method and Description
void	addProof(java.lang.String description, Proof proof) Adds a new Proof.
void	addProofStoreListener(ISideProofStoreListener l) Registers the ISideProofStoreListener.
void	addPropertyChangeListener(java.beans.PropertyChangeListener listener) Adds the given listener.
void	addPropertyChangeListener(java.lang.String propertyName, java.beans.PropertyChangeListener listener) Adds the given listener for the given property only.
void	clearProofs() Removes all SideProofStore.Entrys.
boolean	containsEntry(Proof proof) Checks if an SideProofStore.Entry for the given Proof exist.
boolean	containsEntry(SideProofStore.Entry entry) Checks if the given SideProofStore.Entry is contained.
int	countEntries() Returns the number of contained SideProofStore.Entrys.
protected void	fireEntriesAdded(SideProofStoreEvent e) Fires the event ISideProofStoreListener.entriesAdded(SideProofStoreEvent).
protected void	fireEntriesRemoved(SideProofStoreEvent e) Fires the event ISideProofStoreListener.entriesRemoved(SideProofStoreEvent).
SideProofStore.Entry[]	getEntries() Returns all available SideProofStore.Entrys.
SideProofStore.Entry	getEntry(Proof proof) Returns the SideProofStore.Entry for the given Proof.
SideProofStore.Entry	getEntryAt(int index) Returns the SideProofStore.Entry at the given index.
ISideProofStoreListener[]	getProofStoreListener() Returns all registered ISideProofStoreListener.
boolean	isEnabled() Checks if the SideProofStore is enabled or not.
void	removeEntries(java.util.Collection<SideProofStore.Entry> entries) Removes the given SideProofStore.Entrys.
void	removeProofStoreListener(ISideProofStoreListener l) Unregisters the ISideProofStoreListener.
void	removePropertyChangeListener(java.beans.PropertyChangeListener listener) Removes the given listener.
void	removePropertyChangeListener(java.lang.String propertyName, java.beans.PropertyChangeListener listener) Removes the given listener from the given property.
void	setEnabled(boolean enabled) Defines the enabled state.

Methods inherited from class java.lang.Object

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

Field Detail

PROP_ENABLED

public static final java.lang.String PROP_ENABLED

Property isEnabled().

See Also:

Constant Field Values

DEFAULT_INSTANCE

public static final SideProofStore DEFAULT_INSTANCE

The default and only instance of this class.

entries

private final java.util.List<SideProofStore.Entry> entries

All contained SideProofStore.Entrys.

listener

private final java.util.List<ISideProofStoreListener> listener

All available ISideProofStoreListener.

enabled

private boolean enabled

The enabled state.

pcs

private java.beans.PropertyChangeSupport pcs

The PropertyChangeSupport.

Constructor Detail

SideProofStore

private SideProofStore()

Forbid other instances.

Method Detail

isEnabled

public boolean isEnabled()

Checks if the SideProofStore is enabled or not.

Returns:

true enabled, false disabled.

setEnabled

public void setEnabled(boolean enabled)

Defines the enabled state.

Parameters:

enabled - true enabled, false disabled.

addProof

public void addProof(java.lang.String description,
                     Proof proof)

Adds a new Proof.

Parameters:

description - The description.

proof - The Proof to add.

removeEntries

public void removeEntries(java.util.Collection<SideProofStore.Entry> entries)

Removes the given SideProofStore.Entrys.

Parameters:

entries - The SideProofStore.Entrys to remove.

clearProofs

public void clearProofs()

Removes all SideProofStore.Entrys.

containsEntry

public boolean containsEntry(Proof proof)

Checks if an SideProofStore.Entry for the given Proof exist.

Parameters:

proof - The Proof to check.

Returns:

true SideProofStore.Entry for Proof exist, false otherwise.

getEntry

public SideProofStore.Entry getEntry(Proof proof)

Returns the SideProofStore.Entry for the given Proof.

Parameters:

proof - The Proof for which the SideProofStore.Entry is requested.

Returns:

The SideProofStore.Entry with the given Proof or null if not available.

containsEntry

public boolean containsEntry(SideProofStore.Entry entry)

Checks if the given SideProofStore.Entry is contained.

Parameters:

entry - The SideProofStore.Entry to check.

Returns:

true SideProofStore.Entry is contained, false SideProofStore.Entry is not contained.

countEntries

public int countEntries()

Returns the number of contained SideProofStore.Entrys.

Returns:

The number of contained SideProofStore.Entrys.

getEntryAt

public SideProofStore.Entry getEntryAt(int index)

Returns the SideProofStore.Entry at the given index.

Parameters:

index - The index.

Returns:

The SideProofStore.Entry at the given index.

getEntries

public SideProofStore.Entry[] getEntries()

Returns all available SideProofStore.Entrys.

Returns:

All available SideProofStore.Entrys.

addProofStoreListener

public void addProofStoreListener(ISideProofStoreListener l)

Registers the ISideProofStoreListener.

Parameters:

l - The ISideProofStoreListener to register.

removeProofStoreListener

public void removeProofStoreListener(ISideProofStoreListener l)

Unregisters the ISideProofStoreListener.

Parameters:

l - The ISideProofStoreListener to unregister.

getProofStoreListener

public ISideProofStoreListener[] getProofStoreListener()

Returns all registered ISideProofStoreListener.

Returns:

All registered ISideProofStoreListener.

fireEntriesAdded

protected void fireEntriesAdded(SideProofStoreEvent e)

Fires the event ISideProofStoreListener.entriesAdded(SideProofStoreEvent).

Parameters:

e - The event.

fireEntriesRemoved

protected void fireEntriesRemoved(SideProofStoreEvent e)

Fires the event ISideProofStoreListener.entriesRemoved(SideProofStoreEvent).

Parameters:

e - The event.

addPropertyChangeListener

public void addPropertyChangeListener(java.beans.PropertyChangeListener listener)

Adds the given listener.

Parameters:

listener - The listener to add.

addPropertyChangeListener

public void addPropertyChangeListener(java.lang.String propertyName,
                                      java.beans.PropertyChangeListener listener)

Adds the given listener for the given property only.

Parameters:

propertyName - The property to observe.

listener - The listener to add.

removePropertyChangeListener

public void removePropertyChangeListener(java.beans.PropertyChangeListener listener)

Removes the given listener.

Parameters:

listener - The listener to remove.

removePropertyChangeListener

public void removePropertyChangeListener(java.lang.String propertyName,
                                         java.beans.PropertyChangeListener listener)

Removes the given listener from the given property.

Parameters:

propertyName - The property to no longer observe.

listener - The listener to remove.