de.uka.ilkd.key.proof.join

Class JoinIsApplicable

java.lang.Object

de.uka.ilkd.key.proof.join.JoinIsApplicable

public class JoinIsApplicable
extends java.lang.Object

Methods for checking the applicability of a join for a given selection and thereby computing the prospective join partners.

Author:

Benjamin Niedermann

See Also:

JoinProcessor

Field Summary

Fields

Modifier and Type	Field and Description
static JoinIsApplicable	INSTANCE

Constructor Summary

Constructors

Modifier	Constructor and Description
private	JoinIsApplicable()

Method Summary

Modifier and Type	Method and Description
private ProspectivePartner	areProspectivePartners(Goal g1, PosInOccurrence pio, Goal g2) Checks if two given goals are possible join partners for a given selected sequent formula (defined by pio); returns a ProspectivePartner object if this is the case and null otherwise.
java.util.List<ProspectivePartner>	computeProspecitvePartner(Goal goal, PosInOccurrence pio) Computes the partners for the given selection.
java.util.List<ProspectivePartner>	isApplicable(Goal goal, PosInOccurrence pio)

Methods inherited from class java.lang.Object

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

Field Detail

INSTANCE

public static final JoinIsApplicable INSTANCE

Constructor Detail

JoinIsApplicable

private JoinIsApplicable()

Method Detail

isApplicable

public java.util.List<ProspectivePartner> isApplicable(Goal goal,
                                                       PosInOccurrence pio)

Parameters:

goal - The goal to join.

pio - Selected formula (symblic state - program counter part) for the join.

Returns:

The list of possible join partner objects -- may be empty (then, the join is not applicable).

computeProspecitvePartner

public java.util.List<ProspectivePartner> computeProspecitvePartner(Goal goal,
                                                                    PosInOccurrence pio)

Computes the partners for the given selection.

Parameters:

goal - Goal which should be joined.

pio - Selected formula (symblic state - program counter part) for the join.

Returns:

The list of possible join partners.

areProspectivePartners

private ProspectivePartner areProspectivePartners(Goal g1,
                                                  PosInOccurrence pio,
                                                  Goal g2)

Checks if two given goals are possible join partners for a given selected sequent formula (defined by pio); returns a ProspectivePartner object if this is the case and null otherwise.

Parameters:

g1 - Goal for the first node to join.

pio - Selected formula (symbolic state - program counter part) for the join.

g2 - Second goal for the join.

Returns:

A ProspectivePartner object if the given goals may be joined or null otherwise.