de.uka.ilkd.key.speclang

Class ClassWellDefinedness

java.lang.Object

de.uka.ilkd.key.speclang.WellDefinednessCheck

de.uka.ilkd.key.speclang.ClassWellDefinedness

All Implemented Interfaces:

Contract, SpecificationElement

public final class ClassWellDefinedness
extends WellDefinednessCheck

A contract for checking the well-definedness of a specification for a class invariant.

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 ClassInvariant	inv

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
	ClassWellDefinedness(ClassInvariant inv, IObserverFunction target, Term accessible, Term mby, Services services)
private	ClassWellDefinedness(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, ClassInvariant inv, TermBuilder tb)

Method Summary

Modifier and Type	Method and Description
void	addInv(Term inv)
ClassWellDefinedness	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.
static ImmutableSet<RewriteTaclet>	createInvTaclet(Services services) Creates a well-definedness taclet for an invariant reference.
(package private) Function	generateMbyAtPreFunc(Services services)
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()
ClassInvariant	getInvariant()
KeYJavaType	getKJT() Returns the KeYJavaType representing the class/interface to which the specification element belongs.
(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	modelField() Detects if the specification element is a true (i.e. not an invariant) model field
ClassWellDefinedness	setID(int newId) Returns a contract which is identical this contract except that the id is set to the new id.
ClassWellDefinedness	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

inv

private final ClassInvariant inv

Constructor Detail

ClassWellDefinedness

private ClassWellDefinedness(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,
                             ClassInvariant inv,
                             TermBuilder tb)

ClassWellDefinedness

public ClassWellDefinedness(ClassInvariant inv,
                            IObserverFunction target,
                            Term accessible,
                            Term mby,
                            Services services)

Method Detail

generateMbyAtPreFunc

Function generateMbyAtPreFunc(Services services)

Specified by:

generateMbyAtPreFunc in class WellDefinednessCheck

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

createInvTaclet

public static ImmutableSet<RewriteTaclet> createInvTaclet(Services services)

Creates a well-definedness taclet for an invariant reference. Actually we should be able to statically denote this taclet in the rule folder, but somehow the type java.lang.Object is not available there in the required manner.

Parameters:

services -

Returns:

the well-definedness taclet for an invariant reference

getInvariant

public ClassInvariant getInvariant()

addInv

public final void addInv(Term inv)

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

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 ClassWellDefinedness 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

transactionApplicableContract

public boolean transactionApplicableContract()

setID

public ClassWellDefinedness 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 ClassWellDefinedness 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.

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)