public class WellDefinednessPO extends AbstractPO implements ContractPO
The proof obligation for well-definedness checks.
The generated Sequent
has the following form:
==>
WD(<generalAssumptions> && <preconditions>) &
(<generalAssumptions> & <preconditions>
-> WD(<otherClauses>) &
{anon^assignable}WD(<postconditions>)
Modifier and Type | Class and Description |
---|---|
static class |
WellDefinednessPO.Variables
A static data structure for storing and passing the variables used in the actual proof.
|
AbstractPO.Vertex
IPersistablePO.LoadedPOContainer
Modifier and Type | Field and Description |
---|---|
private WellDefinednessCheck |
check |
private Term |
mbyAtPre |
private InitConfig |
proofConfig |
private TermBuilder |
tb |
environmentConfig, environmentServices, heapLDT, javaInfo, name, poNames, poTerms, specRepos, taclets
PROPERTY_ADD_SYMBOLIC_EXECUTION_LABEL, PROPERTY_ADD_UNINTERPRETED_PREDICATE, PROPERTY_CLASS, PROPERTY_FILENAME, PROPERTY_NAME
Constructor and Description |
---|
WellDefinednessPO(InitConfig initConfig,
WellDefinednessCheck check)
Constructor
|
Modifier and Type | Method and Description |
---|---|
private static ImmutableList<ProgramVariable> |
addGhostParams(ImmutableList<ProgramVariable> paramVars,
ImmutableList<ProgramVariable> origParams)
Make sure ghost parameters appear in the list of parameter variables.
|
private static WellDefinednessPO.Variables |
buildVariables(WellDefinednessCheck check,
Services services)
This should only be executed once per proof.
|
private static Function |
createAnonHeap(LocationVariable heap,
Services services) |
private static java.util.Map<LocationVariable,ProgramVariable> |
createAtPres(LocationVariable heap,
TermServices services) |
private static ProgramVariable |
createException(IProgramMethod pm,
TermServices services) |
private static ImmutableList<ProgramVariable> |
createParams(IObserverFunction target,
ImmutableList<ProgramVariable> origParams,
TermServices services) |
private static ProgramVariable |
createResult(IProgramMethod pm,
TermServices services) |
private static LocationVariable |
createSelf(IProgramMethod pm,
KeYJavaType selfKJT,
TermServices services) |
void |
fillSaveProperties(java.util.Properties properties)
This method is called by a
ProofSaver to store the proof
specific settings in the given Properties . |
KeYJavaType |
getContainerType()
Returns the
KeYJavaType in which the proven element is contained in. |
WellDefinednessCheck |
getContract() |
protected InitConfig |
getCreatedInitConfigForSingleProof() |
KeYJavaType |
getKJT() |
Term |
getMbyAtPre() |
IObserverFunction |
getTarget() |
boolean |
implies(ProofOblInput po)
If true, then this PO implies the passed one.
|
static IPersistablePO.LoadedPOContainer |
loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
private Services |
postInit() |
void |
readProblem() |
private void |
register(WellDefinednessPO.Variables vars,
Services proofServices)
Registers the new variables
|
protected ImmutableSet<ClassAxiom> |
selectClassAxioms(KeYJavaType kjt) |
assignPOTerms, collectClassAxioms, createProof, createProofObject, generateSelfCreated, generateSelfExactType, generateSelfExactType, generateSelfNotNull, generateWdTaclets, getName, getPO, name, register, register, register
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getPO, name
private final WellDefinednessCheck check
private Term mbyAtPre
private InitConfig proofConfig
private TermBuilder tb
public WellDefinednessPO(InitConfig initConfig, WellDefinednessCheck check)
initConfig
- The initial Configurationcheck
- The Well-Definedness Checkprivate static Function createAnonHeap(LocationVariable heap, Services services)
private static LocationVariable createSelf(IProgramMethod pm, KeYJavaType selfKJT, TermServices services)
private static ProgramVariable createResult(IProgramMethod pm, TermServices services)
private static ProgramVariable createException(IProgramMethod pm, TermServices services)
private static java.util.Map<LocationVariable,ProgramVariable> createAtPres(LocationVariable heap, TermServices services)
private static ImmutableList<ProgramVariable> addGhostParams(ImmutableList<ProgramVariable> paramVars, ImmutableList<ProgramVariable> origParams)
private static ImmutableList<ProgramVariable> createParams(IObserverFunction target, ImmutableList<ProgramVariable> origParams, TermServices services)
private static WellDefinednessPO.Variables buildVariables(WellDefinednessCheck check, Services services)
check
- the underlying well-definedness checkservices
- private void register(WellDefinednessPO.Variables vars, Services proofServices)
vars
- variables to be used in the checkprotected ImmutableSet<ClassAxiom> selectClassAxioms(KeYJavaType kjt)
selectClassAxioms
in class AbstractPO
public IObserverFunction getTarget()
public KeYJavaType getKJT()
public void readProblem() throws ProofInputException
readProblem
in interface ProofOblInput
ProofInputException
private Services postInit()
public boolean implies(ProofOblInput po)
ProofOblInput
implies
in interface ProofOblInput
implies
in class AbstractPO
public WellDefinednessCheck getContract()
getContract
in interface ContractPO
public Term getMbyAtPre()
getMbyAtPre
in interface ContractPO
public void fillSaveProperties(java.util.Properties properties) throws java.io.IOException
ProofSaver
to store the proof
specific settings in the given Properties
. The stored settings
have to contain all information required to instantiate the proof
obligation again and this instance should create the same Sequent
(if code and specifications are unchanged).fillSaveProperties
in interface IPersistablePO
fillSaveProperties
in class AbstractPO
properties
- The Properties
to fill with the proof obligation specific settings.java.io.IOException
- Occurred Exception.public static IPersistablePO.LoadedPOContainer loadFrom(InitConfig initConfig, java.util.Properties properties) throws java.io.IOException
initConfig
- The already load InitConfig
.properties
- The settings of the proof obligation to instantiate.java.io.IOException
- Occurred Exception.protected InitConfig getCreatedInitConfigForSingleProof()
getCreatedInitConfigForSingleProof
in class AbstractPO
public KeYJavaType getContainerType()
KeYJavaType
in which the proven element is contained in.getContainerType
in interface ProofOblInput
getContainerType
in class AbstractPO
KeYJavaType
in which the proven element is contained in or null
if not available.