Java Doc for JMLObjectToEqualsMap.java in  » Testing » KeY » org » jmlspecs » models » Java Source Code / Java DocumentationJava Source Code and Java Documentation

Java Source Code / Java Documentation
1. 6.0 JDK Core
2. 6.0 JDK Modules
3. 6.0 JDK Modules com.sun
4. 6.0 JDK Modules com.sun.java
5. 6.0 JDK Modules sun
6. 6.0 JDK Platform
7. Ajax
8. Apache Harmony Java SE
9. Aspect oriented
10. Authentication Authorization
11. Blogger System
12. Build
13. Byte Code
14. Cache
15. Chart
16. Chat
17. Code Analyzer
18. Collaboration
19. Content Management System
20. Database Client
21. Database DBMS
22. Database JDBC Connection Pool
23. Database ORM
24. Development
25. EJB Server geronimo
26. EJB Server GlassFish
27. EJB Server JBoss 4.2.1
28. EJB Server resin 3.1.5
29. ERP CRM Financial
30. ESB
31. Forum
32. GIS
33. Graphic Library
34. Groupware
35. HTML Parser
36. IDE
37. IDE Eclipse
38. IDE Netbeans
39. Installer
40. Internationalization Localization
41. Inversion of Control
42. Issue Tracking
43. J2EE
44. JBoss
45. JMS
46. JMX
47. Library
48. Mail Clients
49. Net
50. Parser
51. PDF
52. Portal
53. Profiler
54. Project Management
55. Report
56. RSS RDF
57. Rule Engine
58. Science
59. Scripting
60. Search Engine
61. Security
62. Sevlet Container
63. Source Control
64. Swing Library
65. Template Engine
66. Test Coverage
67. Testing
68. UML
69. Web Crawler
70. Web Framework
71. Web Mail
72. Web Server
73. Web Services
74. Web Services apache cxf 2.0.1
75. Web Services AXIS2
76. Wiki Engine
77. Workflow Engines
78. XML
79. XML UI
Java
Java Tutorial
Java Open Source
Jar File Download
Java Articles
Java Products
Java by API
Photoshop Tutorials
Maya Tutorials
Flash Tutorials
3ds-Max Tutorials
Illustrator Tutorials
GIMP Tutorials
C# / C Sharp
C# / CSharp Tutorial
C# / CSharp Open Source
ASP.Net
ASP.NET Tutorial
JavaScript DHTML
JavaScript Tutorial
JavaScript Reference
HTML / CSS
HTML CSS Reference
C / ANSI-C
C Tutorial
C++
C++ Tutorial
Ruby
PHP
Python
Python Tutorial
Python Open Source
SQL Server / T-SQL
SQL Server / T-SQL Tutorial
Oracle PL / SQL
Oracle PL/SQL Tutorial
PostgreSQL
SQL / MySQL
MySQL Tutorial
VB.Net
VB.Net Tutorial
Flash / Flex / ActionScript
VBA / Excel / Access / Word
XML
XML Tutorial
Microsoft Office PowerPoint 2007 Tutorial
Microsoft Office Excel 2007 Tutorial
Microsoft Office Word 2007 Tutorial
Java Source Code / Java Documentation » Testing » KeY » org.jmlspecs.models 
Source Cross Reference  Class Diagram Java Document (Java Doc) 


java.lang.Object
   org.jmlspecs.models.JMLObjectToEqualsRelation
      org.jmlspecs.models.JMLObjectToEqualsMap

JMLObjectToEqualsMap
public class JMLObjectToEqualsMap extends JMLObjectToEqualsRelation (Code)
Maps (i.e., binary relations that are functional) from non-null elements of Object to non-null elements of Object . The first type, Object, is called the domain type of the map; the second type, Object, is called the range type of the map. A map can be seen as a set of pairs, of form (dv, rv), consisting of an element of the domain type, dv, and an element of the range type, rv. Alternatively, it can be seen as a function that maps each element of the domain to some of elements of the range type.

This type is a subtype of JMLObjectToEqualsRelation , and as such as can be treated as a binary relation or a set valued function also. See the documentation for JMLObjectToEqualsRelation and for the methods inherited from this supertype for more information.

This type considers elements val and dv of the domain type, to be distinct just when _val_not_equal_to_dv_. It considers elements of r and rv of the range type to be distinct just when _r_not_equal_to_rv_. Cloning takes place for the domain or range elements if the corresponding domain or range type is JMLType .
version:
   $Revision: 1.2 $
author:
   Gary T. Leavens
author:
   Clyde Ruby
See Also:   JMLCollection
See Also:   JMLType
See Also:   JMLObjectToEqualsRelation
See Also:   JMLObjectToEqualsRelationEnumerator
See Also:   JMLObjectToEqualsRelationImageEnumerator
See Also:   JMLValueSet
See Also:   JMLObjectSet
See Also:   JMLObjectToObjectMap
See Also:   JMLValueToObjectMap
See Also:   JMLObjectToValueMap
See Also:   JMLValueToValueMap
See Also:   JMLObjectToEqualsRelation.toFunction



Field Summary
final public static  JMLObjectToEqualsMapEMPTY
     The empty JMLObjectToEqualsMap.

Constructor Summary
public  JMLObjectToEqualsMap()
     Initialize this map to be the empty mapping.
public  JMLObjectToEqualsMap(Object dv, Object rv)
     Initialize this map to be a mapping that maps the given domain element to the given range element.
public  JMLObjectToEqualsMap(JMLObjectEqualsPair pair)
     Initialize this map to be a mapping that maps the key in the given pair to the value in that pair.
protected  JMLObjectToEqualsMap(JMLValueSet ipset, JMLObjectSet dom, int sz)
     Initialize this map based on the representation values given.

Method Summary
public  Objectapply(Object dv)
     Return the range element corresponding to dv, if there is one.
public  JMLObjectToEqualsMapclashReplaceUnion(JMLObjectToEqualsMap othMap, Object errval)
     Return a new map that is like the union of the given map and this map, except that if both define a mapping for a given domain element, then each of these clashes is replaced by a mapping from the domain element in question to the given range element.
public  Objectclone()
    
public  JMLValueToEqualsMapcompose(JMLValueToObjectMap othMap)
     Return a new map that is the composition of this and the given map.
public  JMLObjectToEqualsMapcompose(JMLObjectToObjectMap othMap)
     Return a new map that is the composition of this and the given map.
public  JMLObjectToEqualsMapdisjointUnion(JMLObjectToEqualsMap othMap)
     Return a map that is the disjoint union of this and othMap.
public  JMLObjectToEqualsMapextend(Object dv, Object rv)
     Return a new map that is like this but maps the given domain element to the given range element.
public  JMLObjectToEqualsMapextendUnion(JMLObjectToEqualsMap othMap)
     Return a new map that is like the union of the given map and this map, except that if both define a mapping for a given domain element, then only the mapping in the given map is retained.
public  booleanisaFunction()
     Tells whether this relation is a function.
public  JMLObjectToEqualsMaprangeRestrictedTo(JMLEqualsSet rng)
     Return a new map that is like this map but only contains associations that map to range elements in the given set.
public  JMLObjectToEqualsMapremoveDomainElement(Object dv)
     Return a new map that is like this but has no association for the given domain element.
public  JMLObjectToEqualsMaprestrictedTo(JMLObjectSet dom)
     Return a new map that only maps elements in the given domain to the corresponding range elements in this map.
public static  JMLObjectToEqualsMapsingletonMap(Object dv, Object rv)
     Return the singleton map containing the given association.
public static  JMLObjectToEqualsMapsingletonMap(JMLObjectEqualsPair pair)
     Return the singleton map containing the association described by the given pair.

Field Detail
EMPTY
final public static JMLObjectToEqualsMap EMPTY(Code)
The empty JMLObjectToEqualsMap.
See Also:   JMLObjectToEqualsMap.JMLObjectToEqualsMap()




Constructor Detail
JMLObjectToEqualsMap
public JMLObjectToEqualsMap()(Code)
Initialize this map to be the empty mapping.
See Also:   JMLObjectToEqualsMap.EMPTY



JMLObjectToEqualsMap
public JMLObjectToEqualsMap(Object dv, Object rv)(Code)
Initialize this map to be a mapping that maps the given domain element to the given range element.
See Also:   JMLObjectToEqualsMap.singletonMap(Object,Object)
See Also:   JMLObjectToEqualsMap.JMLObjectToEqualsMap(JMLObjectEqualsPair)



JMLObjectToEqualsMap
public JMLObjectToEqualsMap(JMLObjectEqualsPair pair)(Code)
Initialize this map to be a mapping that maps the key in the given pair to the value in that pair.
See Also:   JMLObjectToEqualsMap.singletonMap(JMLObjectEqualsPair)
See Also:   JMLObjectToEqualsMap.JMLObjectToEqualsMap(Object,Object)



JMLObjectToEqualsMap
protected JMLObjectToEqualsMap(JMLValueSet ipset, JMLObjectSet dom, int sz)(Code)
Initialize this map based on the representation values given.




Method Detail
apply
public Object apply(Object dv) throws JMLNoSuchElementException(Code)
Return the range element corresponding to dv, if there is one.
Parameters:
  dv - the domain element for which an association issought (the key to the table).
exception:
  JMLNoSuchElementException - when dv is not associatedto any range element by this.
See Also:   JMLObjectToEqualsRelation.isDefinedAt
See Also:   JMLObjectToEqualsRelation.elementImage
See Also:   JMLObjectToEqualsRelation.image



clashReplaceUnion
public JMLObjectToEqualsMap clashReplaceUnion(JMLObjectToEqualsMap othMap, Object errval) throws IllegalStateException(Code)
Return a new map that is like the union of the given map and this map, except that if both define a mapping for a given domain element, then each of these clashes is replaced by a mapping from the domain element in question to the given range element.
Parameters:
  othMap - the other map.
Parameters:
  errval - the range element to use when clashes occur.
See Also:   JMLObjectToEqualsMap.extendUnion
See Also:   JMLObjectToEqualsMap.disjointUnion
See Also:   JMLObjectToEqualsRelation.union



clone
public Object clone()(Code)



compose
public JMLValueToEqualsMap compose(JMLValueToObjectMap othMap)(Code)
Return a new map that is the composition of this and the given map. The composition is done in the usual order; that is, if the given map maps x to y and this maps y to z, then the result maps x to z.
See Also:   JMLObjectToEqualsMap.compose(JMLObjectToObjectMap)



compose
public JMLObjectToEqualsMap compose(JMLObjectToObjectMap othMap)(Code)
Return a new map that is the composition of this and the given map. The composition is done in the usual order; that is, if the given map maps x to y and this maps y to z, then the result maps x to z.
See Also:   JMLObjectToEqualsMap.compose(JMLValueToObjectMap)



disjointUnion
public JMLObjectToEqualsMap disjointUnion(JMLObjectToEqualsMap othMap) throws JMLMapException, IllegalStateException(Code)
Return a map that is the disjoint union of this and othMap.
Parameters:
  othMap - the other mapping
exception:
  JMLMapException - the ranges of this and othMap have elementsin common (i.e., when they interesect).
See Also:   JMLObjectToEqualsMap.extendUnion
See Also:   JMLObjectToEqualsMap.clashReplaceUnion
See Also:   JMLObjectToEqualsRelation.union



extend
public JMLObjectToEqualsMap extend(Object dv, Object rv)(Code)
Return a new map that is like this but maps the given domain element to the given range element. Any previously existing mapping for the domain element is removed first.
See Also:   JMLObjectToEqualsRelation.insert(ObjectObject)



extendUnion
public JMLObjectToEqualsMap extendUnion(JMLObjectToEqualsMap othMap) throws IllegalStateException(Code)
Return a new map that is like the union of the given map and this map, except that if both define a mapping for a given domain element, then only the mapping in the given map is retained.
See Also:   JMLObjectToEqualsMap.clashReplaceUnion
See Also:   JMLObjectToEqualsMap.disjointUnion
See Also:   JMLObjectToEqualsRelation.union



isaFunction
public boolean isaFunction()(Code)
Tells whether this relation is a function.



rangeRestrictedTo
public JMLObjectToEqualsMap rangeRestrictedTo(JMLEqualsSet rng)(Code)
Return a new map that is like this map but only contains associations that map to range elements in the given set.
See Also:   JMLObjectToEqualsMap.restrictedTo
See Also:   JMLObjectToEqualsRelation.restrictRangeTo



removeDomainElement
public JMLObjectToEqualsMap removeDomainElement(Object dv)(Code)
Return a new map that is like this but has no association for the given domain element.
See Also:   JMLObjectToEqualsRelation.removeFromDomain



restrictedTo
public JMLObjectToEqualsMap restrictedTo(JMLObjectSet dom)(Code)
Return a new map that only maps elements in the given domain to the corresponding range elements in this map.
See Also:   JMLObjectToEqualsMap.rangeRestrictedTo
See Also:   JMLObjectToEqualsRelation.restrictDomainTo



singletonMap
public static JMLObjectToEqualsMap singletonMap(Object dv, Object rv)(Code)
Return the singleton map containing the given association.
See Also:   JMLObjectToEqualsMap.JMLObjectToEqualsMap(Object,Object)
See Also:   JMLObjectToEqualsMap.singletonMap(JMLObjectEqualsPair)



singletonMap
public static JMLObjectToEqualsMap singletonMap(JMLObjectEqualsPair pair)(Code)
Return the singleton map containing the association described by the given pair.
See Also:   JMLObjectToEqualsMap.JMLObjectToEqualsMap(JMLObjectEqualsPair)
See Also:   JMLObjectToEqualsMap.singletonMap(Object,Object)



Fields inherited from org.jmlspecs.models.JMLObjectToEqualsRelation
final public static JMLObjectToEqualsRelation EMPTY(Code)(Java Doc)
final protected static String TOO_BIG_TO_UNION(Code)(Java Doc)
final protected JMLObjectSet domain_(Code)(Java Doc)
final protected JMLValueSet imagePairSet_(Code)(Java Doc)
final protected int size_(Code)(Java Doc)

Methods inherited from org.jmlspecs.models.JMLObjectToEqualsRelation
public JMLObjectToEqualsRelation add(Object dv, Object rv) throws NullPointerException, IllegalStateException(Code)(Java Doc)
public JMLObjectToEqualsRelationEnumerator associations()(Code)(Java Doc)
public Object clone()(Code)(Java Doc)
public JMLValueToEqualsRelation compose(JMLValueToObjectRelation othRel)(Code)(Java Doc)
public JMLObjectToEqualsRelation compose(JMLObjectToObjectRelation othRel)(Code)(Java Doc)
public JMLObjectToEqualsRelation difference(JMLObjectToEqualsRelation othRel)(Code)(Java Doc)
public JMLObjectSet domain()(Code)(Java Doc)
public JMLObjectSetEnumerator domainElements()(Code)(Java Doc)
public JMLEqualsSet elementImage(Object dv)(Code)(Java Doc)
public JMLObjectToEqualsRelationEnumerator elements()(Code)(Java Doc)
public boolean equals(Object obj)(Code)(Java Doc)
public boolean has(Object dv, Object rv)(Code)(Java Doc)
public boolean has(JMLObjectEqualsPair pair)(Code)(Java Doc)
public boolean has(Object obj)(Code)(Java Doc)
public int hashCode()(Code)(Java Doc)
public JMLEqualsSet image(JMLObjectSet dom)(Code)(Java Doc)
public JMLValueSet imagePairSet()(Code)(Java Doc)
public JMLObjectToEqualsRelationImageEnumerator imagePairs()(Code)(Java Doc)
public JMLObjectToEqualsRelation insert(JMLObjectEqualsPair pair) throws IllegalStateException(Code)(Java Doc)
public int int_size()(Code)(Java Doc)
public JMLObjectToEqualsRelation intersection(JMLObjectToEqualsRelation othRel)(Code)(Java Doc)
public JMLEqualsToObjectRelation inverse()(Code)(Java Doc)
public JMLObjectSet inverseElementImage(Object rv)(Code)(Java Doc)
public JMLObjectSet inverseImage(JMLEqualsSet rng)(Code)(Java Doc)
public boolean isDefinedAt(Object dv)(Code)(Java Doc)
public boolean isEmpty()(Code)(Java Doc)
public boolean isaFunction()(Code)(Java Doc)
public JMLIterator iterator()(Code)(Java Doc)
public JMLEqualsSet range()(Code)(Java Doc)
public JMLEqualsSetEnumerator rangeElements()(Code)(Java Doc)
public JMLObjectToEqualsRelation remove(Object dv, Object rv)(Code)(Java Doc)
public JMLObjectToEqualsRelation remove(JMLObjectEqualsPair pair)(Code)(Java Doc)
public JMLObjectToEqualsRelation removeFromDomain(Object dv)(Code)(Java Doc)
public JMLObjectToEqualsRelation restrictDomainTo(JMLObjectSet dom)(Code)(Java Doc)
public JMLObjectToEqualsRelation restrictRangeTo(JMLEqualsSet rng)(Code)(Java Doc)
public static JMLObjectToEqualsRelation singleton(Object dv, Object rv)(Code)(Java Doc)
public static JMLObjectToEqualsRelation singleton(JMLObjectEqualsPair pair)(Code)(Java Doc)
public JMLValueBag toBag()(Code)(Java Doc)
public JMLObjectToEqualsMap toFunction()(Code)(Java Doc)
public JMLValueSequence toSequence()(Code)(Java Doc)
public JMLValueSet toSet()(Code)(Java Doc)
public String toString()(Code)(Java Doc)
public JMLObjectToEqualsRelation union(JMLObjectToEqualsRelation othRel) throws IllegalStateException(Code)(Java Doc)

Methods inherited from java.lang.Object
protected Object clone() throws CloneNotSupportedException(Code)(Java Doc)
public boolean equals(Object o)(Code)(Java Doc)
protected void finalize() throws Throwable(Code)(Java Doc)
final native public Class getClass()(Code)(Java Doc)
public int hashCode()(Code)(Java Doc)
final public void notify() throws IllegalMonitorStateException(Code)(Java Doc)
final public void notifyAll() throws IllegalMonitorStateException(Code)(Java Doc)
public String toString()(Code)(Java Doc)
final public void wait() throws IllegalMonitorStateException, InterruptedException(Code)(Java Doc)
final public void wait(long ms) throws IllegalMonitorStateException, InterruptedException(Code)(Java Doc)
final public void wait(long ms, int ns) throws IllegalMonitorStateException, InterruptedException(Code)(Java Doc)

www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.