public class ProofObligationCreator
extends java.lang.Object
create(...)
.Constructor and Description |
---|
ProofObligationCreator() |
Modifier and Type | Method and Description |
---|---|
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. |
public ProofAggregate create(ImmutableSet<Taclet> taclets, InitConfig[] initConfigs, ImmutableSet<Taclet> axioms, java.util.Collection<TacletSoundnessPOLoader.LoaderListener> listeners)
taclets
a proof obligation
containing the corresponding FOL formula of the taclet.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.Copyright © 2003-2019 The KeY-Project.