public class ProgramVariableCollection
extends java.lang.Object
JMLSpecFactory
.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 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.
|
public ProgramVariable selfVar
self
public ImmutableList<ProgramVariable> paramVars
public ProgramVariable resultVar
result
public ProgramVariable excVar
exception
public java.util.Map<LocationVariable,LocationVariable> atPreVars
var
to \old(var)
.public java.util.Map<LocationVariable,Term> atPres
var
to \old(var)
.public java.util.Map<LocationVariable,LocationVariable> atBeforeVars
var
to \before(var)
(if applicable).public java.util.Map<LocationVariable,Term> atBefores
var
to \before(var)
(if applicable).public ProgramVariableCollection(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,LocationVariable> atPreVars, java.util.Map<LocationVariable,Term> atPres)
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)
.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)
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).public ProgramVariableCollection()