| java.lang.Object
 de.uka.ilkd.key.proof.examples.CloseProofForTrue
| CloseProofForTrue | | public class CloseProofForTrue (Code) | | The
CloseProofForTrue.run method of this class will construct a proof object
for the sequent that has the formula true in the succedent.
It then prints out the proof and its list of open goals.
Next, it constructs a taclet that will close such a goal and
applies it.
Note that it is not strictly necessary to put our taclet into
the Taclet index. We do it here, because TacletApp objects are
rather complicated to construct by hand and the
RuleAppIndex can do it for us.
|
| buildBuiltInRuleIndex | | public BuiltInRuleIndex buildBuiltInRuleIndex()(Code) | | Return an empty built-in rule index
|
| buildInitialProof | | public Proof buildInitialProof()(Code) | | return the proof for the constructed sequent.
|
| buildRuleAppIndex | | public RuleAppIndex buildRuleAppIndex()(Code) | | Return a RuleAppIndex appropriate for our rules.
|
| buildSequent | | public Sequent buildSequent()(Code) | | return a sequent containing the formula true.
|
| buildTaclet | | public Taclet buildTaclet()(Code) | | return the taclet find(==>true) close goal
|
| buildTacletIndex | | public TacletIndex buildTacletIndex()(Code) | | Return a taclet index with our taclet in it.
|
| getRuleApp | | public RuleApp getRuleApp(Goal goal)(Code) | | Return a
RuleApp that will apply
taclet on the first formula of the succedent.
|
| run | | public void run()(Code) | | Build an initial proof with a formula in it.
|
|
|