JML

org.jmlspecs.checker
Class JmlAssignableFieldSet

java.lang.Object
  extended byorg.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
Constructor Detail

JmlAssignableFieldSet

public JmlAssignableFieldSet()

JmlAssignableFieldSet

public JmlAssignableFieldSet(CField field)

JmlAssignableFieldSet

private JmlAssignableFieldSet(JmlAssignableFieldSet other)
Method Detail

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

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.