de.uka.ilkd.key.java

Class ContextStatementBlock

java.lang.Object

de.uka.ilkd.key.java.JavaSourceElement

de.uka.ilkd.key.java.JavaProgramElement

de.uka.ilkd.key.java.JavaNonTerminalProgramElement

de.uka.ilkd.key.java.statement.JavaStatement

de.uka.ilkd.key.java.StatementBlock

de.uka.ilkd.key.java.ContextStatementBlock

All Implemented Interfaces:

TypeDeclarationContainer, ModelElement, NonTerminalProgramElement, ProgramElement, ScopeDefiningElement, SourceElement, Statement, StatementContainer, TypeScope, VariableScope, SVSubstitute, ProgramPrefix

public class ContextStatementBlock
extends StatementBlock

In the DL-formulae description of Taclets the program part can have the following form < pi alpha;...; omega > Phi where pi is a prefix consisting of open brackets, try's and so on and omega is the rest of the program. Between the prefix pi and the postfix omega there can stand an arbitrary program. This pattern is realized using this class.

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.java.JavaProgramElement

JavaProgramElement.NameAbstractionTableDisabled

Field Summary

Fields

Modifier and Type	Field and Description
private IExecutionContext	executionContext the last execution context of the context term
private int	patternPrefixLength length of this progran prefix

Constructor Summary

Constructors

Constructor and Description
ContextStatementBlock(ExtList children) creates a ContextStatementBlock
ContextStatementBlock(ExtList children, IExecutionContext executionContext) creates a ContextStatementBlock
ContextStatementBlock(Statement[] body, IExecutionContext executionContext)
ContextStatementBlock(Statement s, IExecutionContext executionContext)

Method Summary

Modifier and Type	Method and Description
boolean	compatibleBlockSize(int pos, int max) overrides the check of the superclass as unmatched elements will disappear in the suffix of this ContextStatementBlock
ProgramElement	getChildAt(int index) Returns the child at the specified index in this node's "virtual" child array
int	getChildCount() Returns the number of children of this node.
IExecutionContext	getExecutionContext()
private static ProgramPrefix	getPrefixElementAt(ProgramPrefix prefix, int i)
TypeDeclaration	getTypeDeclarationAt(int index)
int	getTypeDeclarationCount() Get the number of type declarations in this container.
private MatchConditions	makeContextInfoComplete(MatchConditions matchCond, SourceData newSource, ProgramPrefix prefix, int pos, PosInProgram relPos, ProgramElement src, Services services) completes match of context block by adding the prefix end position and the suffix start position
MatchConditions	match(SourceData source, MatchConditions matchCond) matches the source "text" (@link SourceData#getSource()) against the pattern represented by this object.
private MatchConditions	matchInnerExecutionContext(MatchConditions matchCond, Services services, ExecutionContext lastExecutionContext, ProgramPrefix prefix, int pos, ProgramElement src) matches the inner most execution context in prefix, used to resolve references in succeeding matchings
private PosInProgram	matchPrefixEnd(ProgramPrefix prefix, int pos, PosInProgram relPos) computes the PosInProgram of the first element, which is not part of the prefix
void	prettyPrint(PrettyPrinter w) Pretty printing the source element.
boolean	requiresExplicitExecutionContextMatch()
java.lang.String	toString() toString
void	visit(Visitor v) calls the corresponding method of a visitor in order to perform some action/transformation on this element

Methods inherited from class de.uka.ilkd.key.java.StatementBlock

computePrefixElements, equalsModRenaming, getBody, getFirstActiveChildPos, getFirstElement, getFirstElementIncludingBlocks, getInnerMostMethodFrame, getLastPrefixElement, getNextPrefixElement, getPrefixElements, getPrefixLength, getStatementAt, getStatementCount, hasNextPrefixElement, isEmpty

Methods inherited from class de.uka.ilkd.key.java.JavaNonTerminalProgramElement

computeHashCode, equals, getArrayPos, matchChildren

Methods inherited from class de.uka.ilkd.key.java.JavaProgramElement

getComments, hashCode, prettyPrintMain, reuseSignature

Methods inherited from class de.uka.ilkd.key.java.JavaSourceElement

getEndPosition, getLastElement, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.java.ProgramElement

getComments

Methods inherited from interface de.uka.ilkd.key.java.SourceElement

getEndPosition, getLastElement, getPositionInfo, getRelativePosition, getStartPosition

Field Detail

executionContext

private final IExecutionContext executionContext

the last execution context of the context term

patternPrefixLength

private final int patternPrefixLength

length of this progran prefix

Constructor Detail

ContextStatementBlock

public ContextStatementBlock(ExtList children)

creates a ContextStatementBlock

Parameters:

children - the body of the context term

ContextStatementBlock

public ContextStatementBlock(ExtList children,
                             IExecutionContext executionContext)

creates a ContextStatementBlock

Parameters:

children - the body of the context term

executionContext - the required execution context

ContextStatementBlock

public ContextStatementBlock(Statement s,
                             IExecutionContext executionContext)

ContextStatementBlock

public ContextStatementBlock(Statement[] body,
                             IExecutionContext executionContext)

Method Detail

requiresExplicitExecutionContextMatch

public boolean requiresExplicitExecutionContextMatch()

getExecutionContext

public IExecutionContext getExecutionContext()

getChildCount

public int getChildCount()

Returns the number of children of this node.

Specified by:

getChildCount in interface NonTerminalProgramElement

Overrides:

getChildCount in class StatementBlock

Returns:

an int giving the number of children of this node

getChildAt

public ProgramElement getChildAt(int index)

Returns the child at the specified index in this node's "virtual" child array

Specified by:

getChildAt in interface NonTerminalProgramElement

Overrides:

getChildAt in class StatementBlock

Parameters:

index - an index into this node's "virtual" child array

Returns:

the program element at the given position

Throws:

java.lang.ArrayIndexOutOfBoundsException - if index is out of bounds

visit

public void visit(Visitor v)

calls the corresponding method of a visitor in order to perform some action/transformation on this element

Specified by:

visit in interface SourceElement

Overrides:

visit in class StatementBlock

Parameters:

v - the Visitor

prettyPrint

public void prettyPrint(PrettyPrinter w)
                 throws java.io.IOException

Description copied from class: JavaSourceElement

Pretty printing the source element.

Specified by:

prettyPrint in interface SourceElement

Overrides:

prettyPrint in class StatementBlock

Parameters:

w - a pretty printer.

Throws:

java.io.IOException - occasionally thrown.

toString

public java.lang.String toString()

Description copied from class: JavaSourceElement

toString

Overrides:

toString in class JavaSourceElement

getTypeDeclarationCount

public int getTypeDeclarationCount()

Description copied from class: StatementBlock

Get the number of type declarations in this container.

Specified by:

getTypeDeclarationCount in interface TypeDeclarationContainer

Overrides:

getTypeDeclarationCount in class StatementBlock

Returns:

the number of type declarations.

getTypeDeclarationAt

public TypeDeclaration getTypeDeclarationAt(int index)

Specified by:

getTypeDeclarationAt in interface TypeDeclarationContainer

Overrides:

getTypeDeclarationAt in class StatementBlock

compatibleBlockSize

public boolean compatibleBlockSize(int pos,
                                   int max)

overrides the check of the superclass as unmatched elements will disappear in the suffix of this ContextStatementBlock

Overrides:

compatibleBlockSize in class JavaNonTerminalProgramElement

match

public MatchConditions match(SourceData source,
                             MatchConditions matchCond)

Description copied from interface: ProgramElement

matches the source "text" (@link SourceData#getSource()) against the pattern represented by this object. In case of a successful match the resulting MatchConditions with the found instantiations of the schemavariables. If the match failed, null is returned instead.

Specified by:

match in interface ProgramElement

Overrides:

match in class JavaNonTerminalProgramElement

Parameters:

source - the SourceData with the program element to match

matchCond - the MatchConditions found up to this point

Returns:

the resulting match conditions or null if the match failed

makeContextInfoComplete

private MatchConditions makeContextInfoComplete(MatchConditions matchCond,
                                                SourceData newSource,
                                                ProgramPrefix prefix,
                                                int pos,
                                                PosInProgram relPos,
                                                ProgramElement src,
                                                Services services)

completes match of context block by adding the prefix end position and the suffix start position

matchInnerExecutionContext

private MatchConditions matchInnerExecutionContext(MatchConditions matchCond,
                                                   Services services,
                                                   ExecutionContext lastExecutionContext,
                                                   ProgramPrefix prefix,
                                                   int pos,
                                                   ProgramElement src)

matches the inner most execution context in prefix, used to resolve references in succeeding matchings

Parameters:

matchCond - the MatchCond the matchonditions already found

services - the Services

lastExecutionContext - the ExecutionContext if already found

prefix - the oute rmost prefixelement of the original source

pos - an int as the number of prefix elements to disappear in the context

src - the original source

Returns:

the inner most execution context

matchPrefixEnd

private PosInProgram matchPrefixEnd(ProgramPrefix prefix,
                                    int pos,
                                    PosInProgram relPos)

computes the PosInProgram of the first element, which is not part of the prefix

Parameters:

prefix - the ProgramPrefix the outer most prefix element of the source

pos - the number of elements to disappear in the context

relPos - the position of the first active statement of element prefix.getPrefixElementAt(pos);

Returns:

the PosInProgram of the first element, which is not part of the prefix

getPrefixElementAt

private static ProgramPrefix getPrefixElementAt(ProgramPrefix prefix,
                                                int i)