de.uka.ilkd.key.speclang

Class StatementWellDefinedness

java.lang.Object

de.uka.ilkd.key.speclang.WellDefinednessCheck

de.uka.ilkd.key.speclang.StatementWellDefinedness

All Implemented Interfaces:

Contract, SpecificationElement

Direct Known Subclasses:

BlockWellDefinedness, LoopWellDefinedness

public abstract class StatementWellDefinedness
extends WellDefinednessCheck

A contract for checking the well-definedness of a jml statement. Contrary to jml specifications for methods, model fields and class invariants, the well-definedness of jml statements is checked "on-the-fly", i.e. before/when it is applied, since the check needs the context it is placed in. Thus the technical difference to other well-definedness checks is the context update and that it is not a separate contract, but another branch of the specific rule of the overlying proof. The according proof sequent is built in #generateSequent(ProgramVariable, ProgramVariable, ProgramVariable, LocationVariable, ProgramVariable, Term, ImmutableSet, Term, Services) Nevertheless it is imaginable to make them separate contracts.

Author:

Michael Kirsten

Nested Class Summary

Nested Classes

Modifier and Type

Class and Description

(package private) class

StatementWellDefinedness.SequentTerms A data structure to pass the needed terms for the well-definedness sequent of a jml statement, including the context update, pre-condition for the statement, well-formedness condition for the anonymous heap, well-definedness term for the statement's assignable-clause, well-definedness term for other clauses in the statement and the well-definedness term for the statement's post-condition with the according updates (heap of pre-state becomes current heap and the current heap gets anonymised) applied to it.

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

Constructor and Description
StatementWellDefinedness(java.lang.String name, int id, IObserverFunction target, Contract.OriginalVariables origVars, WellDefinednessCheck.Type type, Services services)
StatementWellDefinedness(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, TermBuilder tb)

Method Summary

Modifier and Type	Method and Description
(package private) static ImmutableList<ProgramVariable>	convertParams(ImmutableSet<ProgramVariable> set) Converts a set of parameter variables into a list of parameter variables
(package private) StatementWellDefinedness.SequentTerms	createSeqTerms(WellDefinednessCheck.POTerms po, WellDefinednessPO.Variables vars, Term leadingUpdate, Term localAnon, Services services) Aggregates and preprocesses the proof obligation data into the according terms for the well-definedness sequent of the jml statement.
(package private) Function	generateMbyAtPreFunc(Services services)
SequentFormula	generateSequent(ProgramVariable self, LocationVariable heap, Term anonHeap, ImmutableSet<ProgramVariable> ps, Term leadingUpdate, Term localAnonUpdate, Services services) This is where the proof sequent is built, however with a smaller set of variables, due to the nature of the jml statement.
SequentFormula	generateSequent(ProgramVariable self, ProgramVariable exception, ProgramVariable result, LocationVariable heap, ProgramVariable heapAtPre, Term anonHeap, ImmutableSet<ProgramVariable> ps, Term leadingUpdate, Term localAnonUpdate, Services services) This is where the proof sequent is built.
(package private) abstract SequentFormula	generateSequent(StatementWellDefinedness.SequentTerms seqTerms, 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.
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()
(package private) ImmutableList<Term>	getRest() Collects all remaining (implicitly or explicity) specified clauses (except for pre-condition, post-condition and assignable-clause).
abstract SpecificationElement	getStatement()
boolean	modelField() Detects if the specification element is a true (i.e. not an invariant) model field

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

addEnsures, addEnsures, addRepresents, addRequires, addRequires, combine, 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

getTypeName, isAuxiliary, setID, setTarget, transactionApplicableContract

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

getKJT, getVisibility

Constructor Detail

StatementWellDefinedness

StatementWellDefinedness(java.lang.String name,
                         int id,
                         IObserverFunction target,
                         Contract.OriginalVariables origVars,
                         WellDefinednessCheck.Type type,
                         Services services)

StatementWellDefinedness

StatementWellDefinedness(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,
                         TermBuilder tb)

Method Detail

generateSequent

abstract SequentFormula generateSequent(StatementWellDefinedness.SequentTerms seqTerms,
                                        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.

Parameters:

seqTerms -

services -

Returns:

getStatement

public abstract SpecificationElement getStatement()

convertParams

static final ImmutableList<ProgramVariable> convertParams(ImmutableSet<ProgramVariable> set)

Converts a set of parameter variables into a list of parameter variables

Parameters:

set - a set of parameter variables

Returns:

a list of the parameter variables

generateMbyAtPreFunc

final Function generateMbyAtPreFunc(Services services)

Specified by:

generateMbyAtPreFunc in class WellDefinednessCheck

getRest

final 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

createSeqTerms

final StatementWellDefinedness.SequentTerms createSeqTerms(WellDefinednessCheck.POTerms po,
                                                           WellDefinednessPO.Variables vars,
                                                           Term leadingUpdate,
                                                           Term localAnon,
                                                           Services services)

Aggregates and preprocesses the proof obligation data into the according terms for the well-definedness sequent of the jml statement.

Parameters:

po - the proof obligation terms of the statement

vars - the new (current) variables

leadingUpdate - the context update of the program before the statement

localAnon - anonymize local variables

services -

Returns:

the actual terms used in the well-definedness sequent

generateSequent

public SequentFormula generateSequent(ProgramVariable self,
                                      ProgramVariable exception,
                                      ProgramVariable result,
                                      LocationVariable heap,
                                      ProgramVariable heapAtPre,
                                      Term anonHeap,
                                      ImmutableSet<ProgramVariable> ps,
                                      Term leadingUpdate,
                                      Term localAnonUpdate,
                                      Services services)

This is where the proof sequent is built.

Parameters:

self - The current self variable

exception - The current exception variable

result - The current result variable

heap - The current heap

heapAtPre - The current old heap

anonHeap - The anonymized heap

ps - The current parameter variables

leadingUpdate - The context update

localAnonUpdate - anonymization update of local variables

services - The current services reference

Returns:

The proof sequent for the well-definedness check

generateSequent

public SequentFormula generateSequent(ProgramVariable self,
                                      LocationVariable heap,
                                      Term anonHeap,
                                      ImmutableSet<ProgramVariable> ps,
                                      Term leadingUpdate,
                                      Term localAnonUpdate,
                                      Services services)

This is where the proof sequent is built, however with a smaller set of variables, due to the nature of the jml statement. This means no exception variable, no result variable and variable for the heap of the pre-state.

Parameters:

self - self variable

heap - heap variable

anonHeap - anonymised heap

ps - set of parameter variables

leadingUpdate - the context update

localAnonUpdate - anonymization update of local variables

services -

Returns:

The proof sequent for the well-definedness check

getBehaviour

public final java.lang.String getBehaviour()

Description copied from class: WellDefinednessCheck

Detects the specification element's behaviour

Specified by:

getBehaviour in class WellDefinednessCheck

Returns:

behaviour string

getGlobalDefs

public final Term getGlobalDefs()

getAxiom

public final 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)

modelField

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