org.jmlspecs.checker
Class JmlDataGroupAccumulator

java.lang.Object
  org.jmlspecs.checker.JmlDataGroupAccumulator

public class JmlDataGroupAccumulator

extends Object

This class represents a set of jml-data-group-assertion's in JML ASTs.

Version:

$Revision: 1.5 $

Author:

Clyde Ruby

Field Summary
protected  ArrayList	inGroupList
protected  JmlInGroupClause[]	inGroups
protected  ArrayList	mapsIntoList

 

Constructor Summary

JmlDataGroupAccumulator()

 

Method Summary
void	addInGroup(JmlInGroupClause fieldAssertion)
void	addMapsInto(JmlMapsIntoClause fieldAssertion)
JmlMapsIntoClause[]	getMapsIntoClausesFor(String fieldId)
JmlInGroupClause[]	inGroupClauses()
ArrayList	mapsIntoClauses()

 

Methods inherited from class java.lang.Object

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

 

Field Detail

inGroupList

protected ArrayList inGroupList

mapsIntoList

protected ArrayList mapsIntoList

inGroups

protected JmlInGroupClause[] inGroups

JmlDataGroupAccumulator

public JmlDataGroupAccumulator()

addInGroup

public void addInGroup(JmlInGroupClause fieldAssertion)

inGroupClauses

public JmlInGroupClause[] inGroupClauses()

addMapsInto

public void addMapsInto(JmlMapsIntoClause fieldAssertion)

mapsIntoClauses

public ArrayList mapsIntoClauses()

getMapsIntoClausesFor

public JmlMapsIntoClause[] getMapsIntoClausesFor(String fieldId)