de.uka.ilkd.key.speclang

Class MethodWellDefinedness

java.lang.Object

de.uka.ilkd.key.speclang.WellDefinednessCheck

de.uka.ilkd.key.speclang.MethodWellDefinedness

All Implemented Interfaces:

Contract, SpecificationElement

public final class MethodWellDefinedness
extends WellDefinednessCheck

A contract for checking the well-definedness of a specification for a method or model field. Additionally to the general well-definedness contract, it consists of other definitions for the contract.

Author:

Michael Kirsten

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.speclang.WellDefinednessCheck

WellDefinednessCheck.Condition, WellDefinednessCheck.POTerms, WellDefinednessCheck.TermAndFunc, WellDefinednessCheck.Type

Nested classes/interfaces inherited from interface de.uka.ilkd.key.speclang.Contract

Contract.OriginalVariables

Field Summary

Fields

Modifier and Type	Field and Description
private Term	axiom
private Contract	contract
private Term	globalDefs
private boolean	modelField

Fields inherited from class de.uka.ilkd.key.speclang.WellDefinednessCheck

INV_TACLET, OP_EXC_TACLET, OP_TACLET, TB

Fields inherited from interface de.uka.ilkd.key.speclang.Contract

INVALID_ID

Constructor Summary

Constructors

Modifier	Constructor and Description
	MethodWellDefinedness(DependencyContract contract, Services services)
	MethodWellDefinedness(FunctionalOperationContract contract, Services services)
	MethodWellDefinedness(RepresentsAxiom rep, Services services)
private	MethodWellDefinedness(java.lang.String name, int id, WellDefinednessCheck.Type type, IObserverFunction target, LocationVariable heap, Contract.OriginalVariables origVars, WellDefinednessCheck.Condition requires, Term assignable, Term accessible, WellDefinednessCheck.Condition ensures, Term mby, Term rep, Contract contract, Term globalDefs, Term axiom, boolean model, TermBuilder tb)

Method Summary

Modifier and Type	Method and Description
MethodWellDefinedness	combine(WellDefinednessCheck wdc, TermServices services) Combines two well-definedness checks having the same name, id, target, type, behaviour and are either both model fields or both not a model field.
RewriteTaclet	combineTaclets(RewriteTaclet t1, RewriteTaclet t2, TermServices services) Combines two well-definedness taclets for (pure) method invocations.
RewriteTaclet	createOperationTaclet(Services services) Creates a well-definedness for a (pure) method invocation of this method.
private boolean	findExcNull(Term t, ProgramVariable exc) Finds an -on top level- conjuncted term of the form (exc = null) in the given term.
(package private) Term	generateMbyAtPreDef(ParsableVariable self, ImmutableList<ParsableVariable> params, Function mbyAtPreFunc, Services services) Generates a term of the form (mbyAtPre = mby) if mby is specified.
(package private) Function	generateMbyAtPreFunc(Services services)
private Term[]	getArgs(SchemaVariable sv, ParsableVariable heap, ParsableVariable heapAtPre, boolean isStatic, boolean twoState, ImmutableList<ParsableVariable> params) Gets the argument list for the operator of the method
Term	getAxiom() Only for contracts with model_behaviour, the result is different from null.
java.lang.String	getBehaviour() Detects the specification element's behaviour
Term	getGlobalDefs()
KeYJavaType	getKJT() Returns the KeYJavaType representing the class/interface to which the specification element belongs.
Contract	getMethodContract()
(package private) ImmutableList<Term>	getRest() Collects all remaining (implicitly or explicity) specified clauses (except for pre-condition, post-condition and assignable-clause).
java.lang.String	getTypeName() Returns technical name for the contract type.
VisibilityModifier	getVisibility() Returns the visibility of the invariant (null for default visibility)
boolean	isModel() Tells whether the method is a model method, i.e. has model behaviour or not.
boolean	isNormal(TermServices services) Used to determine if the contract of this method has normal behaviour or is a model field/method and can thus not throw any exception.
boolean	isPure() Tells whether the method is pure or not.
boolean	modelField() Detects if the specification element is a true (i.e. not an invariant) model field
private ImmutableList<ParsableVariable>	paramsSV() Converts the original parameters into schema variables
MethodWellDefinedness	setID(int newId) Returns a contract which is identical this contract except that the id is set to the new id.
MethodWellDefinedness	setTarget(KeYJavaType newKJT, IObserverFunction newPM) Returns a contract which is identical to this contract except that the KeYJavaType and IObserverFunction are set to the new values.
boolean	transactionApplicableContract()

Methods inherited from class de.uka.ilkd.key.speclang.WellDefinednessCheck

addEnsures, addEnsures, addRepresents, addRequires, addRequires, combineAccessible, combineAssignable, createExcTaclet, createPOTerms, createProofObl, createProofObl, createProofObl, createTaclet, createTaclet, equals, getAccessible, getAccessible, getAssignable, getAssignable, getDep, getDep, getDisplayName, getEnsures, getEnsures, getGlobalDefs, getHeap, getHTMLText, getMby, getMby, getMby, getName, getOrigVars, getPlainText, getPost, getPre, getPre, getPre, getPre, getPre, getProofObl, getRepresents, getRequires, getRequires, getTarget, getUpdates, hashCode, hasMby, hasSelfVar, id, isConstructor, isOn, name, proofToString, replace, replace, replace, replaceSV, setAccessible, setAssignable, setEnsures, setMby, setRequires, toBeSaved, toString, type

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.speclang.Contract

isAuxiliary

Field Detail

contract

private final Contract contract

globalDefs

private Term globalDefs

axiom

private Term axiom

modelField

private final boolean modelField

Constructor Detail

MethodWellDefinedness

private MethodWellDefinedness(java.lang.String name,
                              int id,
                              WellDefinednessCheck.Type type,
                              IObserverFunction target,
                              LocationVariable heap,
                              Contract.OriginalVariables origVars,
                              WellDefinednessCheck.Condition requires,
                              Term assignable,
                              Term accessible,
                              WellDefinednessCheck.Condition ensures,
                              Term mby,
                              Term rep,
                              Contract contract,
                              Term globalDefs,
                              Term axiom,
                              boolean model,
                              TermBuilder tb)

MethodWellDefinedness

public MethodWellDefinedness(FunctionalOperationContract contract,
                             Services services)

MethodWellDefinedness

public MethodWellDefinedness(DependencyContract contract,
                             Services services)

MethodWellDefinedness

public MethodWellDefinedness(RepresentsAxiom rep,
                             Services services)

Method Detail

getArgs

private Term[] getArgs(SchemaVariable sv,
                       ParsableVariable heap,
                       ParsableVariable heapAtPre,
                       boolean isStatic,
                       boolean twoState,
                       ImmutableList<ParsableVariable> params)

Gets the argument list for the operator of the method

Parameters:

sv - schema variable for self

heap - schema variable for the heap

isStatic - information whether this is a static method

params - schema variables for the parameters

Returns:

the term array of arguments used to construct the method term

findExcNull

private boolean findExcNull(Term t,
                            ProgramVariable exc)

Finds an -on top level- conjuncted term of the form (exc = null) in the given term.

Parameters:

t - the term to be searched in

exc - the exception variable

Returns:

true if the term guarantees exc to be equal to null

paramsSV

private ImmutableList<ParsableVariable> paramsSV()

Converts the original parameters into schema variables

Returns:

a list of schema variables

generateMbyAtPreFunc

Function generateMbyAtPreFunc(Services services)

Specified by:

generateMbyAtPreFunc in class WellDefinednessCheck

generateMbyAtPreDef

Term generateMbyAtPreDef(ParsableVariable self,
                         ImmutableList<ParsableVariable> params,
                         Function mbyAtPreFunc,
                         Services services)

Generates a term of the form (mbyAtPre = mby) if mby is specified.

Parameters:

self - the self variable

params - the list of parameters

mbyAtPreFunc - the measured-by function

services -

Returns:

the measured by at pre equation for the precondition

getRest

ImmutableList<Term> getRest()

Description copied from class: WellDefinednessCheck

Collects all remaining (implicitly or explicity) specified clauses (except for pre-condition, post-condition and assignable-clause).

Overrides:

getRest in class WellDefinednessCheck

Returns:

a list of all remaining clauses

getMethodContract

public Contract getMethodContract()

createOperationTaclet

public RewriteTaclet createOperationTaclet(Services services)

Creates a well-definedness for a (pure) method invocation of this method.

Parameters:

services -

Returns:

the taclet

combineTaclets

public RewriteTaclet combineTaclets(RewriteTaclet t1,
                                    RewriteTaclet t2,
                                    TermServices services)

Combines two well-definedness taclets for (pure) method invocations.

Parameters:

t1 - taclet one

t2 - taclet two

services -

Returns:

the combined taclet

getBehaviour

public java.lang.String getBehaviour()

Description copied from class: WellDefinednessCheck

Detects the specification element's behaviour

Specified by:

getBehaviour in class WellDefinednessCheck

Returns:

behaviour string

isNormal

public boolean isNormal(TermServices services)

Used to determine if the contract of this method has normal behaviour or is a model field/method and can thus not throw any exception.

Returns:

true for either normal behaviour or model fields

isPure

public boolean isPure()

Tells whether the method is pure or not.

Returns:

true for pure methods and pure (model) fields

isModel

public boolean isModel()

Tells whether the method is a model method, i.e. has model behaviour or not.

Returns:

true for model methods

modelField

public boolean modelField()

Description copied from class: WellDefinednessCheck

Detects if the specification element is a true (i.e. not an invariant) model field

Specified by:

modelField in class WellDefinednessCheck

Returns:

true for model fields

combine

public MethodWellDefinedness combine(WellDefinednessCheck wdc,
                                     TermServices services)

Description copied from class: WellDefinednessCheck

Combines two well-definedness checks having the same name, id, target, type, behaviour and are either both model fields or both not a model field.

Overrides:

combine in class WellDefinednessCheck

Parameters:

wdc - the well-definedness check to be combined with the current one

Returns:

the combined well-definedness contract

getGlobalDefs

public Term getGlobalDefs()

getAxiom

public Term getAxiom()

Description copied from class: WellDefinednessCheck

Only for contracts with model_behaviour, the result is different from null.

Specified by:

getAxiom in class WellDefinednessCheck

Returns:

the return value of a model method (null otherwise)

transactionApplicableContract

public boolean transactionApplicableContract()

setID

public MethodWellDefinedness setID(int newId)

Description copied from interface: Contract

Returns a contract which is identical this contract except that the id is set to the new id.

Parameters:

newId - the new id value

Returns:

an identical contract with the new id

setTarget

public MethodWellDefinedness setTarget(KeYJavaType newKJT,
                                       IObserverFunction newPM)

Description copied from interface: Contract

Returns a contract which is identical to this contract except that the KeYJavaType and IObserverFunction are set to the new values.

Parameters:

newKJT - the new KeYJavaType

newPM - the new observer function

Returns:

an identical contract with the new KJT and PM (see above)

getTypeName

public java.lang.String getTypeName()

Description copied from interface: Contract

Returns technical name for the contract type.

Returns:

the technical name

getVisibility

public VisibilityModifier getVisibility()

Description copied from interface: SpecificationElement

Returns the visibility of the invariant (null for default visibility)

getKJT

public KeYJavaType getKJT()

Description copied from interface: SpecificationElement

Returns the KeYJavaType representing the class/interface to which the specification element belongs.