org.jmlspecs.checker
Class JmlAssignableFieldSet

java.lang.Object
  org.jmlspecs.checker.JmlAssignableFieldSet

public class JmlAssignableFieldSet

extends Object

This class acts as a set containing the assignable fields mentioned in an assignable clause. This class is also used to accumulate the members (fields) of a data group.

Field Summary
private  boolean	containsDynamicFields
private  boolean	containsEverything
private  boolean	containsPrivateFields
private  ArrayList	dataGroupList           A list containing only the fields that have an associated data group.
private  boolean	notSpecified
private  LinkedHashSet	theFieldSet           A set containing all the fields in this data group.

 

Constructor Summary
	JmlAssignableFieldSet()
private	JmlAssignableFieldSet(JmlAssignableFieldSet other)
	JmlAssignableFieldSet(CField field)

 

Method Summary
boolean	add(JmlStoreRef storeRef)
boolean	add(CField field)
boolean	addAll(JmlAssignableFieldSet otherSet)
void	clear()
Object	clone()
boolean	contains(CField field)
boolean	contains(CField field, JmlDataGroupMemberMap dgMap)
boolean	contains(JClassFieldExpression fieldExpr, JmlDataGroupMemberMap dgMap)
JmlAssignableFieldSet	intersect(JmlAssignableFieldSet otherSet, JmlDataGroupMemberMap dgMap)
boolean	isEmpty()
boolean	isNotSpecified()
boolean	isSubsetOf(JmlAssignableFieldSet otherSet, JmlDataGroupMemberMap dgMap)
boolean	isSupersetOf(JmlAssignableFieldSet otherSet, JmlDataGroupMemberMap dgMap)
boolean	isUniversalSet()
Iterator	iterator()
void	setNotSpecified()
int	size()
String	toString()

 

Methods inherited from class java.lang.Object

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

 

Field Detail

theFieldSet

private LinkedHashSet theFieldSet

A set containing all the fields in this data group. Also used to accumulate the assignable fields mentioned in an assignable clause.

 invariant theFieldSet != null;
 

dataGroupList

private ArrayList dataGroupList

A list containing only the fields that have an associated data group.

 invariant dataGroupList != null;
 

containsEverything

private boolean containsEverything

notSpecified

private boolean notSpecified

containsPrivateFields

private boolean containsPrivateFields

containsDynamicFields

private boolean containsDynamicFields

JmlAssignableFieldSet

public JmlAssignableFieldSet()

JmlAssignableFieldSet

public JmlAssignableFieldSet(CField field)

JmlAssignableFieldSet

private JmlAssignableFieldSet(JmlAssignableFieldSet other)

add

public boolean add(CField field)

add

public boolean add(JmlStoreRef storeRef)

clear

public void clear()

clone

public Object clone()

Overrides:

clone in class Object

contains

public boolean contains(CField field)

setNotSpecified

public void setNotSpecified()

contains

public boolean contains(CField field,
                        JmlDataGroupMemberMap dgMap)

contains

public boolean contains(JClassFieldExpression fieldExpr,
                        JmlDataGroupMemberMap dgMap)

size

public int size()

iterator

public Iterator iterator()

isEmpty

public boolean isEmpty()

isUniversalSet

public boolean isUniversalSet()

isNotSpecified

public boolean isNotSpecified()

addAll

public boolean addAll(JmlAssignableFieldSet otherSet)

isSubsetOf

public boolean isSubsetOf(JmlAssignableFieldSet otherSet,
                          JmlDataGroupMemberMap dgMap)

isSupersetOf

public boolean isSupersetOf(JmlAssignableFieldSet otherSet,
                            JmlDataGroupMemberMap dgMap)

intersect

public JmlAssignableFieldSet intersect(JmlAssignableFieldSet otherSet,
                                       JmlDataGroupMemberMap dgMap)

toString

public String toString()

Overrides:

toString in class Object