JML

org.jmlspecs.checker
Class JmlDataGroupMemberMap

java.lang.Object
  extended byorg.jmlspecs.checker.JmlDataGroupMemberMap

public class JmlDataGroupMemberMap
extends Object

This class acts as a


Field Summary
private  boolean inheritedMembersAdded
           
private  HashMap memberMap
          A mapping from JmlSourceField objects to JmlAssignableFieldsSet objects for handling members of data groups and checking assignable clauses.
 
Constructor Summary
JmlDataGroupMemberMap()
           
 
Method Summary
 void addGroup(JmlSourceField field)
          Add a mapping from field to the members of its data group.
 void addInheritedMembers(JmlDataGroupMemberMap parentMap)
          Add mappings for any groups in parentMap that are already in this map.
 void addMember(JmlSourceField group, CField member)
          Add member to the member set of group if group is already in this map.
 void addMembers(JmlSourceField group, JmlAssignableFieldSet members)
          Add a mapping for group if it is not already in this map.
 JmlAssignableFieldSet getMembers(JmlSourceField group)
          Returns the members of the given data group.
 Iterator keyGroupIterator()
           
 String toString()
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

memberMap

private HashMap memberMap
A mapping from JmlSourceField objects to JmlAssignableFieldsSet objects for handling members of data groups and checking assignable clauses.

 private invariant memberMap != null;
 


inheritedMembersAdded

private boolean inheritedMembersAdded
Constructor Detail

JmlDataGroupMemberMap

public JmlDataGroupMemberMap()
Method Detail

addGroup

public void addGroup(JmlSourceField field)
Add a mapping from field to the members of its data group. Initially the member set only has one member, i.e., field. This is only done if field is a data group, i.e., if it is a model field or has either a spec_public or spec_protected visibility modifier.


addMember

public void addMember(JmlSourceField group,
                      CField member)
Add member to the member set of group if group is already in this map. Otherwise, create a new group and add member to the member set for group.

 requires group != null &&  member != null && group.isDataGroup();
 


addMembers

public void addMembers(JmlSourceField group,
                       JmlAssignableFieldSet members)
Add a mapping for group if it is not already in this map. Otherwise, merge (union) member with sets for any groups that are in both maps.

 requires group != null &&  members != null && group.isDataGroup();
 


keyGroupIterator

public Iterator keyGroupIterator()

addInheritedMembers

public void addInheritedMembers(JmlDataGroupMemberMap parentMap)
Add mappings for any groups in parentMap that are already in this map. Also, merge (union) the member sets for any groups that are in both maps.

 requires parentMap != null && inheritedMembersAdded == false;
 


getMembers

public JmlAssignableFieldSet getMembers(JmlSourceField group)
Returns the members of the given data group. If group is not in the domain of this map, then null is returned.

 requires group != null;
 


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.