de.uka.ilkd.key.speclang

Class BlockWellDefinedness

java.lang.Object

de.uka.ilkd.key.speclang.WellDefinednessCheck

de.uka.ilkd.key.speclang.StatementWellDefinedness

de.uka.ilkd.key.speclang.BlockWellDefinedness

All Implemented Interfaces:

Contract, SpecificationElement

public class BlockWellDefinedness
extends StatementWellDefinedness

A contract for checking the well-definedness of a jml block contract.

Author:

Michael Kirsten

Nested Class Summary

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

StatementWellDefinedness.SequentTerms

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 BlockContract	block The jml block contract.

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
	BlockWellDefinedness(BlockContract block, AuxiliaryContract.Variables variables, ImmutableSet<ProgramVariable> params, Services services) Creates a contract to check well-definedness of a block contract
private	BlockWellDefinedness(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, BlockContract block, TermBuilder tb)

Method Summary

Modifier and Type	Method and Description
BlockWellDefinedness	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.
(package private) SequentFormula	generateSequent(StatementWellDefinedness.SequentTerms seq, TermServices services) This formula creates the sequent formula for the well-definedness of a jml statement in the specific way, in which it is required for the specific jml statement.
KeYJavaType	getKJT() Returns the KeYJavaType representing the class/interface to which the specification element belongs.
BlockContract	getStatement()
java.lang.String	getTypeName() Returns technical name for the contract type.
VisibilityModifier	getVisibility() Returns the visibility of the invariant (null for default visibility)
Contract	setID(int newId) Returns a contract which is identical this contract except that the id is set to the new id.
Contract	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.StatementWellDefinedness

convertParams, createSeqTerms, generateMbyAtPreFunc, generateSequent, generateSequent, getAxiom, getBehaviour, getGlobalDefs, getRest, modelField

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

block

private final BlockContract block

The jml block contract.

Constructor Detail

BlockWellDefinedness

private BlockWellDefinedness(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,
                             BlockContract block,
                             TermBuilder tb)

BlockWellDefinedness

public BlockWellDefinedness(BlockContract block,
                            AuxiliaryContract.Variables variables,
                            ImmutableSet<ProgramVariable> params,
                            Services services)

Creates a contract to check well-definedness of a block contract

Parameters:

block - the block belonging to the block contract

variables - the variables of the block contract

params - the parameters of the block

services - the services instance

Method Detail

generateSequent

SequentFormula generateSequent(StatementWellDefinedness.SequentTerms seq,
                               TermServices services)

Description copied from class: StatementWellDefinedness

This formula creates the sequent formula for the well-definedness of a jml statement in the specific way, in which it is required for the specific jml statement.

Specified by:

generateSequent in class StatementWellDefinedness

Returns:

getStatement

public BlockContract getStatement()

Specified by:

getStatement in class StatementWellDefinedness

transactionApplicableContract

public boolean transactionApplicableContract()

setID

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

combine

public BlockWellDefinedness 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