de.uka.ilkd.key.symbolic_execution.rule

Class AbstractSideProofRule

java.lang.Object

de.uka.ilkd.key.symbolic_execution.rule.AbstractSideProofRule

All Implemented Interfaces:

BuiltInRule, Rule

Direct Known Subclasses:

ModalitySideProofRule, QuerySideProofRule

public abstract class AbstractSideProofRule
extends java.lang.Object
implements BuiltInRule

Provides the basic functionality of BuiltInRule which computes something in a side proof.

Author:

Martin Hentschel

Constructor Summary

Constructors

Constructor and Description
AbstractSideProofRule()

Method Summary

Modifier and Type	Method and Description
protected java.util.List<Triple<Term,java.util.Set<Term>,Node>>	computeResultsAndConditions(Services services, Goal goal, ProofEnvironment sideProofEnvironment, Sequent sequentToProve, Function newPredicate) Starts the side proof and extracts the result Term and conditions.
protected Function	createResultConstant(Services services, Sort sort) Creates a constant which is used in the original Proof to store the computed result in form of QueryResult = ...
protected Function	createResultFunction(Services services, Sort sort) Creates the result Function used in a predicate to compute the result in the side proof.
boolean	isApplicableOnSubTerms()
protected static SequentFormula	replace(PosInOccurrence pio, Term newTerm, Services services) Replaces the Term defined by the given PosInOccurrence with the given new Term.

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.rule.BuiltInRule

createApp, isApplicable

Methods inherited from interface de.uka.ilkd.key.rule.Rule

apply, displayName, name

Constructor Detail

AbstractSideProofRule

public AbstractSideProofRule()

Method Detail

createResultConstant

protected Function createResultConstant(Services services,
                                        Sort sort)

Creates a constant which is used in the original Proof to store the computed result in form of QueryResult = ...

The used name is registered in the Namespace of the Services.

Parameters:

services - The Services to use-

sort - The Sort to use.

Returns:

The created constant.

createResultFunction

protected Function createResultFunction(Services services,
                                        Sort sort)

Creates the result Function used in a predicate to compute the result in the side proof.

Parameters:

services - The Services to use.

sort - The Sort to use.

Returns:

The created result Function.

computeResultsAndConditions

protected java.util.List<Triple<Term,java.util.Set<Term>,Node>> computeResultsAndConditions(Services services,
                                                                                            Goal goal,
                                                                                            ProofEnvironment sideProofEnvironment,
                                                                                            Sequent sequentToProve,
                                                                                            Function newPredicate)
                                                                                     throws ProofInputException

Starts the side proof and extracts the result Term and conditions.

New used names are automatically added to the Namespace of the Services.

Parameters:

services - The Services to use.

goal - The Goal on which this BuiltInRule should be applied on.

sideProofEnvironment - The given ProofEnvironment of the side proof.

sequentToProve - The Sequent to prove in a side proof.

newPredicate - The Function which is used to compute the result.

Returns:

The found result Term and the conditions.

Throws:

ProofInputException - Occurred Exception.

replace

protected static SequentFormula replace(PosInOccurrence pio,
                                        Term newTerm,
                                        Services services)

Replaces the Term defined by the given PosInOccurrence with the given new Term.

Parameters:

pio - The PosInOccurrence which defines the Term to replace.

newTerm - The new Term.

Returns:

The created SequentFormula in which the Term is replaced.

isApplicableOnSubTerms

public boolean isApplicableOnSubTerms()

Specified by:

isApplicableOnSubTerms in interface BuiltInRule