de.uka.ilkd.key.speclang

Class AuxiliaryContract.Terms

java.lang.Object

de.uka.ilkd.key.speclang.AuxiliaryContract.Terms

Enclosing interface:

AuxiliaryContract

public static class AuxiliaryContract.Terms
extends java.lang.Object

See Also:

AuxiliaryContract.Variables.termify(Term)

Field Summary

Fields

Modifier and Type	Field and Description
java.util.Map<Label,Term>	breakFlags
java.util.Map<Label,Term>	continueFlags
Term	exception
java.util.Map<LocationVariable,Term>	outerRemembranceHeaps
java.util.Map<LocationVariable,Term>	outerRemembranceVariables
java.util.Map<LocationVariable,Term>	remembranceHeaps
java.util.Map<LocationVariable,Term>	remembranceLocalVariables
Term	result
Term	returnFlag
Term	self

Constructor Summary

Constructors

Constructor and Description
Terms(AuxiliaryContract.Variables variables, TermBuilder tb)
Terms(Term self, java.util.Map<Label,Term> breakFlags, java.util.Map<Label,Term> continueFlags, Term returnFlag, Term result, Term exception, java.util.Map<LocationVariable,Term> remembranceHeaps, java.util.Map<LocationVariable,Term> remembranceLocalVariables, java.util.Map<LocationVariable,Term> outerRemembranceHeaps, java.util.Map<LocationVariable,Term> outerRemembranceVariables) Creates a new instance.

Method Summary

Modifier and Type	Method and Description
private static java.util.Map<Label,Term>	convertFlagMap(java.util.Map<Label,ProgramVariable> map, TermBuilder tb)
private static java.util.Map<LocationVariable,Term>	convertHeapMap(java.util.Map<LocationVariable,LocationVariable> map, TermBuilder tb)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

self

public final Term self

See Also:

AuxiliaryContract.Variables.self

breakFlags

public final java.util.Map<Label,Term> breakFlags

See Also:

AuxiliaryContract.Variables.breakFlags

continueFlags

public final java.util.Map<Label,Term> continueFlags

See Also:

AuxiliaryContract.Variables.continueFlags

returnFlag

public final Term returnFlag

See Also:

AuxiliaryContract.Variables.returnFlag

result

public final Term result

See Also:

AuxiliaryContract.Variables.result

exception

public final Term exception

See Also:

AuxiliaryContract.Variables.exception

remembranceHeaps

public final java.util.Map<LocationVariable,Term> remembranceHeaps

See Also:

AuxiliaryContract.Variables.remembranceHeaps

remembranceLocalVariables

public final java.util.Map<LocationVariable,Term> remembranceLocalVariables

See Also:

AuxiliaryContract.Variables.remembranceLocalVariables

outerRemembranceHeaps

public final java.util.Map<LocationVariable,Term> outerRemembranceHeaps

See Also:

AuxiliaryContract.Variables.outerRemembranceHeaps

outerRemembranceVariables

public final java.util.Map<LocationVariable,Term> outerRemembranceVariables

See Also:

AuxiliaryContract.Variables.outerRemembranceVariables

Constructor Detail

Terms

public Terms(Term self,
             java.util.Map<Label,Term> breakFlags,
             java.util.Map<Label,Term> continueFlags,
             Term returnFlag,
             Term result,
             Term exception,
             java.util.Map<LocationVariable,Term> remembranceHeaps,
             java.util.Map<LocationVariable,Term> remembranceLocalVariables,
             java.util.Map<LocationVariable,Term> outerRemembranceHeaps,
             java.util.Map<LocationVariable,Term> outerRemembranceVariables)

Creates a new instance. In most cases, AuxiliaryContract.Variables.termify(Term) or Terms#Terms(Variables, TermBuilder) should be used instead of this.

Parameters:

self - self

breakFlags - boolean flags that are set to true when the block terminates by a break label; statement with the specified label.

continueFlags - boolean flags that are set to true when the block terminates by a continue label; statement with the specified label.

returnFlag - boolean flag that is set to true when the block terminates by a return statement.

result - result variable to set when the block terminates by a return statement.

exception - exception variable to set when the block terminates by an uncaught throw statement.

remembranceHeaps - a map from every heap heap to heap_Before_BLOCK.

remembranceLocalVariables - a map from every variable var that is assignable inside the block to var_Before_BLOCK.

outerRemembranceHeaps - a map from every heap heap that is accessible inside the block to heap_Before_METHOD.

outerRemembranceVariables - a map from every variable var that is accessible inside the block to var_Before_METHOD.

Terms

public Terms(AuxiliaryContract.Variables variables,
             TermBuilder tb)

Parameters:

variables - the variables to termify.

tb - the term builder to use.

Method Detail

convertHeapMap

private static java.util.Map<LocationVariable,Term> convertHeapMap(java.util.Map<LocationVariable,LocationVariable> map,
                                                                   TermBuilder tb)

Parameters:

map - a map containing heaps as values.

tb - a term builder.

Returns:

a map with all values termified.

convertFlagMap

private static java.util.Map<Label,Term> convertFlagMap(java.util.Map<Label,ProgramVariable> map,
                                                        TermBuilder tb)

Parameters:

map - a map containing boolean variables as values.

tb - a term builder.

Returns:

a map with all values termified.