de.uka.ilkd.key.taclettranslation.lemma

Class TacletSoundnessPOLoader

java.lang.Object

de.uka.ilkd.key.taclettranslation.lemma.TacletSoundnessPOLoader

public class TacletSoundnessPOLoader
extends java.lang.Object

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static interface	TacletSoundnessPOLoader.LoaderListener
static interface	TacletSoundnessPOLoader.TacletFilter
static class	TacletSoundnessPOLoader.TacletInfo
private class	TacletSoundnessPOLoader.Working

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	isOnlyUsedForProvingTaclets
private java.util.List<TacletSoundnessPOLoader.LoaderListener>	listeners
private boolean	loadAsLemmata
private InitConfig	originalConfig If this InitConfig is unequal to null, the taclets will be loaded using this config as well.
private ProofAggregate	resultingProof
private ImmutableSet<Taclet>	resultingTaclets
private ImmutableSet<Taclet>	resultingTacletsForOriginalProof
private TacletSoundnessPOLoader.TacletFilter	tacletFilter
private TacletLoader	tacletLoader

Constructor Summary

Constructors

Constructor and Description
TacletSoundnessPOLoader(TacletSoundnessPOLoader.LoaderListener listener, TacletSoundnessPOLoader.TacletFilter filter, boolean loadAsLemmata, TacletLoader loader, InitConfig originalConfig, boolean isOnlyUsedForProvingTaclets)

Method Summary

Modifier and Type	Method and Description
void	addListener(TacletSoundnessPOLoader.LoaderListener listener)
private boolean	check(Taclet taclet)
private ImmutableSet<Taclet>	computeCommonTaclets(ImmutableList<Taclet> taclets, ImmutableSet<Taclet> reference)
private void	computeResultingTaclets(java.util.List<TacletSoundnessPOLoader.TacletInfo> collectionOfTacletInfo)
private ProofAggregate	createProof(ProofEnvironment proofEnvForTaclets, ImmutableSet<Taclet> tacletsToProve, ImmutableSet<Taclet> axioms, ImmutableList<Taclet> loadedTaclets)
private java.util.Vector<TacletSoundnessPOLoader.TacletInfo>	createTacletInfo(ImmutableList<Taclet> taclets, ImmutableSet<Taclet> base)
private void	doWork()
private ImmutableSet<Taclet>	getAlreadyInUseTaclets()
ProofAggregate	getResultingProof()
ImmutableSet<Taclet>	getResultingTaclets()
ImmutableSet<Taclet>	getResultingTacletsForOriginalProof()
private boolean	isUsedOnlyForProvingTaclets()
void	registerProofs(ProofAggregate aggregate, ProofEnvironment proofEnv)
void	removeListener(TacletSoundnessPOLoader.LoaderListener listener)
void	start()
void	startSynchronously()

Methods inherited from class java.lang.Object

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

Field Detail

loadAsLemmata

private final boolean loadAsLemmata

originalConfig

private final InitConfig originalConfig

If this InitConfig is unequal to null, the taclets will be loaded using this config as well. This is used for the mode when a proof obligation already exists and the taclets should be added to that proof obligation. The taclets then are loaded twice. Once for generating proof obligations and once for adding them to the already existing proof obligation. This is necessary in order to omit name clashes.

listeners

private final java.util.List<TacletSoundnessPOLoader.LoaderListener> listeners

resultingProof

private ProofAggregate resultingProof

resultingTaclets

private ImmutableSet<Taclet> resultingTaclets

resultingTacletsForOriginalProof

private ImmutableSet<Taclet> resultingTacletsForOriginalProof

isOnlyUsedForProvingTaclets

private final boolean isOnlyUsedForProvingTaclets

tacletLoader

private final TacletLoader tacletLoader

tacletFilter

private final TacletSoundnessPOLoader.TacletFilter tacletFilter

Constructor Detail

TacletSoundnessPOLoader

public TacletSoundnessPOLoader(TacletSoundnessPOLoader.LoaderListener listener,
                               TacletSoundnessPOLoader.TacletFilter filter,
                               boolean loadAsLemmata,
                               TacletLoader loader,
                               InitConfig originalConfig,
                               boolean isOnlyUsedForProvingTaclets)

Method Detail

addListener

public void addListener(TacletSoundnessPOLoader.LoaderListener listener)

removeListener

public void removeListener(TacletSoundnessPOLoader.LoaderListener listener)

start

public void start()

startSynchronously

public void startSynchronously()

getResultingTacletsForOriginalProof

public ImmutableSet<Taclet> getResultingTacletsForOriginalProof()

createTacletInfo

private java.util.Vector<TacletSoundnessPOLoader.TacletInfo> createTacletInfo(ImmutableList<Taclet> taclets,
                                                                              ImmutableSet<Taclet> base)

check

private boolean check(Taclet taclet)

doWork

private void doWork()
             throws ProofInputException

Throws:

ProofInputException

computeCommonTaclets

private ImmutableSet<Taclet> computeCommonTaclets(ImmutableList<Taclet> taclets,
                                                  ImmutableSet<Taclet> reference)

computeResultingTaclets

private void computeResultingTaclets(java.util.List<TacletSoundnessPOLoader.TacletInfo> collectionOfTacletInfo)

getAlreadyInUseTaclets

private ImmutableSet<Taclet> getAlreadyInUseTaclets()

isUsedOnlyForProvingTaclets

private boolean isUsedOnlyForProvingTaclets()

Returns:

returns true if and only if the taclets should be proved sound and are not added to an already existing proof obligation.

createProof

private ProofAggregate createProof(ProofEnvironment proofEnvForTaclets,
                                   ImmutableSet<Taclet> tacletsToProve,
                                   ImmutableSet<Taclet> axioms,
                                   ImmutableList<Taclet> loadedTaclets)

registerProofs

public void registerProofs(ProofAggregate aggregate,
                           ProofEnvironment proofEnv)

getResultingProof

public ProofAggregate getResultingProof()

getResultingTaclets

public ImmutableSet<Taclet> getResultingTaclets()