org.jmlspecs.checker
Class JmlDataGroupMemberMap

java.lang.Object
  org.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

JmlDataGroupMemberMap

public JmlDataGroupMemberMap()

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