de.uka.ilkd.key.proof.init

Class WellDefinednessPO.Variables

java.lang.Object

de.uka.ilkd.key.proof.init.WellDefinednessPO.Variables

Enclosing class:

WellDefinednessPO

public static class WellDefinednessPO.Variables
extends java.lang.Object

A static data structure for storing and passing the variables used in the actual proof. This includes a self variable, a result variable, an exception variable, a mapping of heaps to the according preconditions, a list of parameter variables, a base heap, a heap for the pre-state and an anonymous heap.

Author:

Michael Kirsten

Field Summary

Fields

Modifier and Type	Field and Description
Term	anonHeap
java.util.Map<LocationVariable,ProgramVariable>	atPres
ProgramVariable	exception
LocationVariable	heap
ProgramVariable	heapAtPre
ImmutableList<ProgramVariable>	params
ProgramVariable	result
ProgramVariable	self

Constructor Summary

Constructors

Modifier	Constructor and Description
private	Variables(ProgramVariable self, ProgramVariable result, ProgramVariable exception, java.util.Map<LocationVariable,ProgramVariable> atPres, ImmutableList<ProgramVariable> params, LocationVariable heap, Function anonHeap, TermServices services)
	Variables(ProgramVariable self, ProgramVariable result, ProgramVariable exception, java.util.Map<LocationVariable,ProgramVariable> atPres, ImmutableList<ProgramVariable> params, LocationVariable heap, Term anonHeap)

Method Summary

Methods inherited from class java.lang.Object

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

Field Detail

self

public final ProgramVariable self

result

public final ProgramVariable result

exception

public final ProgramVariable exception

atPres

public final java.util.Map<LocationVariable,ProgramVariable> atPres

params

public final ImmutableList<ProgramVariable> params

heap

public final LocationVariable heap

heapAtPre

public final ProgramVariable heapAtPre

anonHeap

public final Term anonHeap

Constructor Detail

Variables

public Variables(ProgramVariable self,
                 ProgramVariable result,
                 ProgramVariable exception,
                 java.util.Map<LocationVariable,ProgramVariable> atPres,
                 ImmutableList<ProgramVariable> params,
                 LocationVariable heap,
                 Term anonHeap)

Variables

private Variables(ProgramVariable self,
                  ProgramVariable result,
                  ProgramVariable exception,
                  java.util.Map<LocationVariable,ProgramVariable> atPres,
                  ImmutableList<ProgramVariable> params,
                  LocationVariable heap,
                  Function anonHeap,
                  TermServices services)