de.uka.ilkd.key.informationflow.macros

Class SelfcompositionStateExpansionMacro

java.lang.Object

de.uka.ilkd.key.macros.AbstractProofMacro

de.uka.ilkd.key.macros.StrategyProofMacro

de.uka.ilkd.key.macros.AbstractPropositionalExpansionMacro

de.uka.ilkd.key.informationflow.macros.SelfcompositionStateExpansionMacro

All Implemented Interfaces:

ProofMacro

public class SelfcompositionStateExpansionMacro
extends AbstractPropositionalExpansionMacro

The macro SelfcompositionStateExpansionMacro applies rules to extract the self-composed states after the merge of the symbolic execution goals which is included in the proof obligation generation from information flow contracts. This macro splits the goal. The rules that are applied can be set in ADMITTED_RULES.

Author:

christoph

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	SelfcompositionStateExpansionMacro.SelfCompExpansionStrategy This strategy accepts all rule apps for which the rule name is in the admitted set or has INF_FLOW_UNFOLD_PREFIX as a prefix and rejects everything else.

Nested classes/interfaces inherited from interface de.uka.ilkd.key.macros.ProofMacro

ProofMacro.ProgressBarListener

Field Summary

Fields

Modifier and Type	Field and Description
private static java.lang.String[]	ADMITTED_RULES
private static java.util.Set<java.lang.String>	ADMITTED_RULES_SET
private static java.lang.String	INF_FLOW_UNFOLD_PREFIX

Constructor Summary

Constructors

Constructor and Description
SelfcompositionStateExpansionMacro()

Method Summary

Modifier and Type	Method and Description
protected boolean	allowOSS() Whether this macro includes One Step Simplification.
boolean	canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc) Can this macro be applied on the given goals?
protected Strategy	createStrategy(Proof proof, PosInOccurrence posInOcc)
protected java.util.Set<java.lang.String>	getAdmittedRuleNames() Gets the set of admitted rule names.
java.lang.String	getDescription() Gets the description of this macro.
java.lang.String	getName() Gets the name of this macro.
protected boolean	ruleApplicationInContextAllowed(RuleApp ruleApp, PosInOccurrence pio, Goal goal) Checks whether the application of the passed rule is ok in the given context.

Methods inherited from class de.uka.ilkd.key.macros.AbstractPropositionalExpansionMacro

asSet, getCategory

Methods inherited from class de.uka.ilkd.key.macros.StrategyProofMacro

applyTo, doPostProcessing

Methods inherited from class de.uka.ilkd.key.macros.AbstractProofMacro

applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter

Methods inherited from class java.lang.Object

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

Field Detail

ADMITTED_RULES

private static final java.lang.String[] ADMITTED_RULES

INF_FLOW_UNFOLD_PREFIX

private static final java.lang.String INF_FLOW_UNFOLD_PREFIX

See Also:

Constant Field Values

ADMITTED_RULES_SET

private static final java.util.Set<java.lang.String> ADMITTED_RULES_SET

Constructor Detail

SelfcompositionStateExpansionMacro

public SelfcompositionStateExpansionMacro()

Method Detail

getName

public java.lang.String getName()

Description copied from interface: ProofMacro

Gets the name of this macro. Used as menu entry

Returns:

a non-null constant string

getDescription

public java.lang.String getDescription()

Description copied from interface: ProofMacro

Gets the description of this macro. Used as tooltip.

Returns:

a non-null constant string

getAdmittedRuleNames

protected java.util.Set<java.lang.String> getAdmittedRuleNames()

Description copied from class: AbstractPropositionalExpansionMacro

Gets the set of admitted rule names.

Specified by:

getAdmittedRuleNames in class AbstractPropositionalExpansionMacro

Returns:

a constant non-null set

createStrategy

protected Strategy createStrategy(Proof proof,
                                  PosInOccurrence posInOcc)

Overrides:

createStrategy in class AbstractPropositionalExpansionMacro

ruleApplicationInContextAllowed

protected boolean ruleApplicationInContextAllowed(RuleApp ruleApp,
                                                  PosInOccurrence pio,
                                                  Goal goal)

Description copied from class: AbstractPropositionalExpansionMacro

Checks whether the application of the passed rule is ok in the given context.

Overrides:

ruleApplicationInContextAllowed in class AbstractPropositionalExpansionMacro

Parameters:

ruleApp - rule to be applied

pio - context

goal - context

Returns:

true if rule may be applied

canApplyTo

public boolean canApplyTo(Proof proof,
                          ImmutableList<Goal> goals,
                          PosInOccurrence posInOcc)

Can this macro be applied on the given goals? This method should not make any changes but check if the macro can be applied or not on the given goals. This method may be called from within the GUI thread and be compatible with that fact. This macro can always be applied (does not change anything perhaps) TODO make this only applicable if it has an impact.

This compound macro is applicable if and only if the first macro is applicable. If there is no first macro, this is not applicable.

Specified by:

canApplyTo in interface ProofMacro

Overrides:

canApplyTo in class StrategyProofMacro

Parameters:

proof - the current Proof (not null)

goals - the goals (not null)

posInOcc - the position in occurrence (may be null)

Returns:

true, if the macro is allowed to be applied

allowOSS

protected boolean allowOSS()

Description copied from class: AbstractPropositionalExpansionMacro

Whether this macro includes One Step Simplification.

Specified by:

allowOSS in class AbstractPropositionalExpansionMacro