de.uka.ilkd.key.speclang.jml.translation

Class ProgramVariableCollection

java.lang.Object

de.uka.ilkd.key.speclang.jml.translation.ProgramVariableCollection

public class ProgramVariableCollection
extends java.lang.Object

A collection of all program variables needed to translate a textual JML specification case. Used in JMLSpecFactory.

Field Summary

Fields

Modifier and Type	Field and Description
java.util.Map<LocationVariable,Term>	atBefores A map from every variable var to \before(var) (if applicable).
java.util.Map<LocationVariable,LocationVariable>	atBeforeVars A map from every variable var to \before(var) (if applicable).
java.util.Map<LocationVariable,Term>	atPres A map from every variable var to \old(var).
java.util.Map<LocationVariable,LocationVariable>	atPreVars A map from every variable var to \old(var).
ProgramVariable	excVar exception
ImmutableList<ProgramVariable>	paramVars The list of method parameters if the textual specification case is a method contract.
ProgramVariable	resultVar result
ProgramVariable	selfVar self

Constructor Summary

Constructors

Constructor and Description
ProgramVariableCollection() Create an empty collection.
ProgramVariableCollection(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,LocationVariable> atPreVars, java.util.Map<LocationVariable,Term> atPres) Create a collection containing the specified variables.
ProgramVariableCollection(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,LocationVariable> atPreVars, java.util.Map<LocationVariable,Term> atPres, java.util.Map<LocationVariable,LocationVariable> atBeforeVars, java.util.Map<LocationVariable,Term> atBefores) Create a collection containing the specified variables.

Method Summary

Methods inherited from class java.lang.Object

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

Field Detail

selfVar

public ProgramVariable selfVar

self

paramVars

public ImmutableList<ProgramVariable> paramVars

The list of method parameters if the textual specification case is a method contract.

resultVar

public ProgramVariable resultVar

result

excVar

public ProgramVariable excVar

exception

atPreVars

public java.util.Map<LocationVariable,LocationVariable> atPreVars

A map from every variable var to \old(var).

atPres

public java.util.Map<LocationVariable,Term> atPres

A map from every variable var to \old(var).

atBeforeVars

public java.util.Map<LocationVariable,LocationVariable> atBeforeVars

A map from every variable var to \before(var) (if applicable).

atBefores

public java.util.Map<LocationVariable,Term> atBefores

A map from every variable var to \before(var) (if applicable).

Constructor Detail

ProgramVariableCollection

public ProgramVariableCollection(ProgramVariable selfVar,
                                 ImmutableList<ProgramVariable> paramVars,
                                 ProgramVariable resultVar,
                                 ProgramVariable excVar,
                                 java.util.Map<LocationVariable,LocationVariable> atPreVars,
                                 java.util.Map<LocationVariable,Term> atPres)

Create a collection containing the specified variables.

Parameters:

selfVar - self

paramVars - the list of method parameters if the textual specification case is a method contract.

resultVar - result

excVar - exception

atPreVars - a map from every variable var to \old(var).

atPres - a map from every variable var to \old(var).

ProgramVariableCollection

public ProgramVariableCollection(ProgramVariable selfVar,
                                 ImmutableList<ProgramVariable> paramVars,
                                 ProgramVariable resultVar,
                                 ProgramVariable excVar,
                                 java.util.Map<LocationVariable,LocationVariable> atPreVars,
                                 java.util.Map<LocationVariable,Term> atPres,
                                 java.util.Map<LocationVariable,LocationVariable> atBeforeVars,
                                 java.util.Map<LocationVariable,Term> atBefores)

Create a collection containing the specified variables.

Parameters:

selfVar - self

paramVars - the list of method parameters if the textual specification case is a method contract.

resultVar - result

excVar - exception

atPreVars - a map from every variable var to \old(var).

atPres - a map from every variable var to \old(var).

atBeforeVars - a map from every variable var to \before(var) (if applicable).

atBefores - a map from every variable var to \before(var) (if applicable).

ProgramVariableCollection

public ProgramVariableCollection()

Create an empty collection.