de.uka.ilkd.key.logic.op

Class ProgramVariable

java.lang.Object

de.uka.ilkd.key.logic.op.AbstractOperator

de.uka.ilkd.key.logic.op.AbstractSortedOperator

de.uka.ilkd.key.logic.op.ProgramVariable

All Implemented Interfaces:

Expression, ModelElement, ProgramElement, ReferencePrefix, ReferenceSuffix, SourceElement, TerminalProgramElement, Named, IProgramVariable, Operator, ParsableVariable, SortedOperator, SVSubstitute, ProgramInLogic, Sorted

Direct Known Subclasses:

LocationVariable, ProgramConstant

public abstract class ProgramVariable
extends AbstractSortedOperator
implements SourceElement, ProgramElement, Expression, ReferencePrefix, IProgramVariable, ParsableVariable, ReferenceSuffix, ProgramInLogic

The objects of this class represent program variables and program constants (resulting from static final declarations in programs; TODO: it is weird that constants are a special case of variables). Additionally, as a legacy of the past, the RecodeR front end of KeY still creates objects of this class also for fields (aka. attributes, member variables), even though theoretically, these are *not* program variables (not any more)! Such fake "program variables" can be recognized by the fact that calling isMember() on them returns true. Thus, they must never occur in actual proofs. The method HeapLDT.getFieldSymbolForPV() serves to convert such fake program variables to the appropriate constant symbols.

Field Summary

Fields

Modifier and Type	Field and Description
private KeYJavaType	containingType
private boolean	isFinal
private boolean	isGhost
private boolean	isModel
private boolean	isStatic
private KeYJavaType	type

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	ProgramVariable(ProgramElementName name, Sort s, KeYJavaType t, KeYJavaType containingType, boolean isStatic, boolean isModel, boolean isGhost)
protected	ProgramVariable(ProgramElementName name, Sort s, KeYJavaType t, KeYJavaType containingType, boolean isStatic, boolean isModel, boolean isGhost, boolean isFinal)

Method Summary

Modifier and Type	Method and Description
Expression	convertToProgram(Term t, ExtList l)
boolean	equalsModRenaming(SourceElement se, NameAbstractionTable nat) equals modulo renaming is described in the corresponding comment in class SourceElement.
Comment[]	getComments() Get comments.
KeYJavaType	getContainerType() returns the KeYJavaType where the program variable is declared or null if the program variable denotes not a field
Position	getEndPosition() Returns the end position of the primary token of this element.
SourceElement	getFirstElement() Finds the source element that occurs first in the source.
SourceElement	getFirstElementIncludingBlocks() Finds the source element that occurs first in the source.
KeYJavaType	getKeYJavaType()
KeYJavaType	getKeYJavaType(Services javaServ)
KeYJavaType	getKeYJavaType(Services javaServ, ExecutionContext ec) returns the KeYJavaType of an expression
SourceElement	getLastElement() Finds the source element that occurs last in the source.
PositionInfo	getPositionInfo() complete position information
ProgramElementName	getProgramElementName()
ReferencePrefix	getReferencePrefix() We do not have a prefix, so fake it!
Position	getRelativePosition() Returns the relative position (number of blank heading lines and columns) of the primary token of this element.
Position	getStartPosition() Returns the start position of the primary token of this element.
boolean	isFinal() returns true iff the program variable has been declared as final
boolean	isGhost() returns true if the program variable has been declared as ghost
boolean	isImplicit()
boolean	isMember() returns true iff the program variable is a member
boolean	isModel() returns true iff the program variable has been declared as model
boolean	isStatic() returns true iff the program variable has been declared as static
MatchConditions	match(SourceData source, MatchConditions matchCond) matches the source "text" (@link SourceData#getSource()) against the pattern represented by this object.
void	prettyPrint(PrettyPrinter w) Pretty print.
java.lang.String	proofToString()
abstract Operator	rename(Name name) Returns an equivalent variable with the new name.
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.logic.op.AbstractSortedOperator

additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractOperator

arity, bindVarsAt, isRigid, name, toString, validTopLevel, whereToBind

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.logic.op.SortedOperator

argSort, argSorts, sort

Methods inherited from interface de.uka.ilkd.key.logic.op.Operator

arity, bindVarsAt, isRigid, sort, validTopLevel

Methods inherited from interface de.uka.ilkd.key.logic.Named

name

Field Detail

type

private final KeYJavaType type

isStatic

private final boolean isStatic

isModel

private final boolean isModel

isGhost

private final boolean isGhost

isFinal

private final boolean isFinal

containingType

private final KeYJavaType containingType

Constructor Detail

ProgramVariable

protected ProgramVariable(ProgramElementName name,
                          Sort s,
                          KeYJavaType t,
                          KeYJavaType containingType,
                          boolean isStatic,
                          boolean isModel,
                          boolean isGhost,
                          boolean isFinal)

ProgramVariable

protected ProgramVariable(ProgramElementName name,
                          Sort s,
                          KeYJavaType t,
                          KeYJavaType containingType,
                          boolean isStatic,
                          boolean isModel,
                          boolean isGhost)

Method Detail

getProgramElementName

public ProgramElementName getProgramElementName()

Returns:

name of the ProgramVariable

isStatic

public boolean isStatic()

returns true iff the program variable has been declared as static

isModel

public boolean isModel()

returns true iff the program variable has been declared as model

isGhost

public boolean isGhost()

returns true if the program variable has been declared as ghost

isFinal

public boolean isFinal()

returns true iff the program variable has been declared as final

isMember

public boolean isMember()

returns true iff the program variable is a member

getContainerType

public KeYJavaType getContainerType()

returns the KeYJavaType where the program variable is declared or null if the program variable denotes not a field

getFirstElement

public SourceElement getFirstElement()

Description copied from interface: SourceElement

Finds the source element that occurs first in the source.

Specified by:

getFirstElement in interface SourceElement

Returns:

the first source element in the syntactical representation of this element, may be equals to this element.

See Also:

SourceElement.getStartPosition()

getFirstElementIncludingBlocks

public SourceElement getFirstElementIncludingBlocks()

Description copied from interface: SourceElement

Finds the source element that occurs first in the source.

Specified by:

getFirstElementIncludingBlocks in interface SourceElement

Returns:

the first source element in the syntactical representation of this element, may be equals to this element.

See Also:

SourceElement.getStartPosition()

getLastElement

public SourceElement getLastElement()

Description copied from interface: SourceElement

Finds the source element that occurs last in the source.

Specified by:

getLastElement in interface SourceElement

Returns:

the last source element in the syntactical representation of this element, may be equals to this element.

See Also:

SourceElement.getEndPosition()

getComments

public Comment[] getComments()

Description copied from interface: ProgramElement

Get comments.

Specified by:

getComments in interface ProgramElement

Returns:

the comments.

visit

public void visit(Visitor v)

Description copied from interface: SourceElement

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

Specified by:

visit in interface SourceElement

Parameters:

v - the Visitor

prettyPrint

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

Description copied from interface: SourceElement

Pretty print.

Specified by:

prettyPrint in interface SourceElement

Parameters:

w - a pretty printer.

Throws:

java.io.IOException - occasionally thrown.

getStartPosition

public Position getStartPosition()

Description copied from interface: SourceElement

Returns the start position of the primary token of this element. To get the start position of the syntactical first token, call the corresponding method of getFirstElement().

Specified by:

getStartPosition in interface SourceElement

Returns:

the start position of the primary token.

getEndPosition

public Position getEndPosition()

Description copied from interface: SourceElement

Returns the end position of the primary token of this element. To get the end position of the syntactical first token, call the corresponding method of getLastElement().

Specified by:

getEndPosition in interface SourceElement

Returns:

the end position of the primary token.

getRelativePosition

public Position getRelativePosition()

Description copied from interface: SourceElement

Returns the relative position (number of blank heading lines and columns) of the primary token of this element. To get the relative position of the syntactical first token, call the corresponding method of getFirstElement().

Specified by:

getRelativePosition in interface SourceElement

Returns:

the relative position of the primary token.

getPositionInfo

public PositionInfo getPositionInfo()

Description copied from interface: SourceElement

complete position information

Specified by:

getPositionInfo in interface SourceElement

getKeYJavaType

public KeYJavaType getKeYJavaType()

Specified by:

getKeYJavaType in interface IProgramVariable

getKeYJavaType

public KeYJavaType getKeYJavaType(Services javaServ)

Specified by:

getKeYJavaType in interface IProgramVariable

getKeYJavaType

public KeYJavaType getKeYJavaType(Services javaServ,
                                  ExecutionContext ec)

Description copied from interface: Expression

returns the KeYJavaType of an expression

Specified by:

getKeYJavaType in interface Expression

Specified by:

getKeYJavaType in interface IProgramVariable

getReferencePrefix

public ReferencePrefix getReferencePrefix()

We do not have a prefix, so fake it! This way we implement ReferencePrefix

Specified by:

getReferencePrefix in interface ReferencePrefix

equalsModRenaming

public boolean equalsModRenaming(SourceElement se,
                                 NameAbstractionTable nat)

equals modulo renaming is described in the corresponding comment in class SourceElement. In this case two programvariables are considered to be equal if they are assigned to the same abstract name or if they are the same object.

Specified by:

equalsModRenaming in interface SourceElement

convertToProgram

public Expression convertToProgram(Term t,
                                   ExtList l)

Specified by:

convertToProgram in interface ProgramInLogic

proofToString

public java.lang.String proofToString()

isImplicit

public boolean isImplicit()

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

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

rename

public abstract Operator rename(Name name)

Returns an equivalent variable with the new name.

Parameters:

name - the new name

Returns:

equivalent operator with the new name