de.uka.ilkd.key.speclang

Class Contract.OriginalVariables

java.lang.Object

de.uka.ilkd.key.speclang.Contract.OriginalVariables

Enclosing interface:

Contract

public static final class Contract.OriginalVariables
extends java.lang.Object

Class for storing the original variables without always distinguishing several different cases depending on which variables are present/needed in order to provide a general interface. At the moment only used for well-definedness checks (as those refer to already existing structures).

Author:

Michael Kirsten

Field Summary

Fields

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

Constructor Summary

Constructors

Constructor and Description
OriginalVariables(ProgramVariable selfVar, ProgramVariable resVar, ProgramVariable excVar, java.util.Map<? extends LocationVariable,? extends ProgramVariable> atPreVars, ImmutableList<? extends ProgramVariable> paramVars) Create new instance of original variables

Method Summary

Modifier and Type	Method and Description
Contract.OriginalVariables	add(ImmutableList<ProgramVariable> newParams) Adds a list of parameters and deletes the prior ones (if any).

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

Constructor Detail

OriginalVariables

public OriginalVariables(ProgramVariable selfVar,
                         ProgramVariable resVar,
                         ProgramVariable excVar,
                         java.util.Map<? extends LocationVariable,? extends ProgramVariable> atPreVars,
                         ImmutableList<? extends ProgramVariable> paramVars)

Create new instance of original variables

Parameters:

selfVar - the original self variable

resVar - the original result variable

excVar - the original exception variable

atPreVars - the original atPreVars

paramVars - the original parameter variables

Method Detail

add

public Contract.OriginalVariables add(ImmutableList<ProgramVariable> newParams)

Adds a list of parameters and deletes the prior ones (if any).

Parameters:

newParams -

Returns:

the changed original variables