de.uka.ilkd.key.taclettranslation.lemma

Class ProofObligationCreator

java.lang.Object

de.uka.ilkd.key.taclettranslation.lemma.ProofObligationCreator

public class ProofObligationCreator
extends java.lang.Object

Creates for a given set of taclets the corresponding set of proof obligation. For more information see public method create(...).

Constructor Summary

Constructors

Constructor and Description
ProofObligationCreator()

Method Summary

Modifier and Type	Method and Description
private UserDefinedSymbols	analyzeTaclets(ImmutableSet<Taclet> taclets, NamespaceSet referenceNamespaces)
private void	collectUserDefinedSymbols(Term term, UserDefinedSymbols userDefinedSymbols)
ProofAggregate	create(ImmutableSet<Taclet> taclets, InitConfig[] initConfigs, ImmutableSet<Taclet> axioms, java.util.Collection<TacletSoundnessPOLoader.LoaderListener> listeners) Creates for each taclet in taclets a proof obligation containing the corresponding FOL formula of the taclet.
private ProofAggregate	create(Taclet taclet, InitConfig initConfig, UserDefinedSymbols symbolsForAxioms)
private java.lang.String	createName(ProofAggregate[] singleProofs)

Methods inherited from class java.lang.Object

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

Constructor Detail

ProofObligationCreator

public ProofObligationCreator()

Method Detail

createName

private java.lang.String createName(ProofAggregate[] singleProofs)

create

public ProofAggregate create(ImmutableSet<Taclet> taclets,
                             InitConfig[] initConfigs,
                             ImmutableSet<Taclet> axioms,
                             java.util.Collection<TacletSoundnessPOLoader.LoaderListener> listeners)

Creates for each taclet in taclets a proof obligation containing the corresponding FOL formula of the taclet.

Parameters:

taclets - Sets of taclets the proof obligations should be created for.

initConfig - the initial configuration that should be used for creating the proofs.

axioms - The set of user-defined taclets that should be used as additional rules. This taclets are added to the single proof obligation so that they can be used for the proof.

listeners - a listener that observes the single steps. Used for status information.

Returns:

A proof aggregate containing the proofs created by this method.

analyzeTaclets

private UserDefinedSymbols analyzeTaclets(ImmutableSet<Taclet> taclets,
                                          NamespaceSet referenceNamespaces)

collectUserDefinedSymbols

private void collectUserDefinedSymbols(Term term,
                                       UserDefinedSymbols userDefinedSymbols)

create

private ProofAggregate create(Taclet taclet,
                              InitConfig initConfig,
                              UserDefinedSymbols symbolsForAxioms)