Java Doc for JMLEqualsToObjectMap.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.JMLEqualsToObjectRelation
      org.jmlspecs.models.JMLEqualsToObjectMap

JMLEqualsToObjectMap
public class JMLEqualsToObjectMap extends JMLEqualsToObjectRelation (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 JMLEqualsToObjectRelation , and as such as can be treated as a binary relation or a set valued function also. See the documentation for JMLEqualsToObjectRelation 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.3 $
author:
   Gary T. Leavens
author:
   Clyde Ruby
See Also:   JMLCollection
See Also:   JMLType
See Also:   JMLEqualsToObjectRelation
See Also:   JMLEqualsToObjectRelationEnumerator
See Also:   JMLEqualsToObjectRelationImageEnumerator
See Also:   JMLValueSet
See Also:   JMLObjectSet
See Also:   JMLObjectToObjectMap
See Also:   JMLValueToObjectMap
See Also:   JMLObjectToValueMap
See Also:   JMLValueToValueMap
See Also:   JMLEqualsToObjectRelation.toFunction



Field Summary
final public static  JMLEqualsToObjectMapEMPTY
     The empty JMLEqualsToObjectMap.

Constructor Summary
public  JMLEqualsToObjectMap()
     Initialize this map to be the empty mapping.
public  JMLEqualsToObjectMap(Object dv, Object rv)
     Initialize this map to be a mapping that maps the given domain element to the given range element.
public  JMLEqualsToObjectMap(JMLEqualsObjectPair pair)
     Initialize this map to be a mapping that maps the key in the given pair to the value in that pair.
protected  JMLEqualsToObjectMap(JMLValueSet ipset, JMLEqualsSet 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  JMLEqualsToObjectMapclashReplaceUnion(JMLEqualsToObjectMap 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  JMLValueToObjectMapcompose(JMLValueToEqualsMap othMap)
     Return a new map that is the composition of this and the given map.
public  JMLObjectToObjectMapcompose(JMLObjectToEqualsMap othMap)
     Return a new map that is the composition of this and the given map.
public  JMLEqualsToObjectMapdisjointUnion(JMLEqualsToObjectMap othMap)
     Return a map that is the disjoint union of this and othMap.
public  JMLEqualsToObjectMapextend(Object dv, Object rv)
     Return a new map that is like this but maps the given domain element to the given range element.
public  JMLEqualsToObjectMapextendUnion(JMLEqualsToObjectMap 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  JMLEqualsToObjectMaprangeRestrictedTo(JMLObjectSet rng)
     Return a new map that is like this map but only contains associations that map to range elements in the given set.
public  JMLEqualsToObjectMapremoveDomainElement(Object dv)
     Return a new map that is like this but has no association for the given domain element.
public  JMLEqualsToObjectMaprestrictedTo(JMLEqualsSet dom)
     Return a new map that only maps elements in the given domain to the corresponding range elements in this map.
public static  JMLEqualsToObjectMapsingletonMap(Object dv, Object rv)
     Return the singleton map containing the given association.
public static  JMLEqualsToObjectMapsingletonMap(JMLEqualsObjectPair pair)
     Return the singleton map containing the association described by the given pair.

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




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



JMLEqualsToObjectMap
public JMLEqualsToObjectMap(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:   JMLEqualsToObjectMap.singletonMap(Object,Object)
See Also:   JMLEqualsToObjectMap.JMLEqualsToObjectMap(JMLEqualsObjectPair)



JMLEqualsToObjectMap
public JMLEqualsToObjectMap(JMLEqualsObjectPair 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:   JMLEqualsToObjectMap.singletonMap(JMLEqualsObjectPair)
See Also:   JMLEqualsToObjectMap.JMLEqualsToObjectMap(Object,Object)



JMLEqualsToObjectMap
protected JMLEqualsToObjectMap(JMLValueSet ipset, JMLEqualsSet 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:   JMLEqualsToObjectRelation.isDefinedAt
See Also:   JMLEqualsToObjectRelation.elementImage
See Also:   JMLEqualsToObjectRelation.image



clashReplaceUnion
public JMLEqualsToObjectMap clashReplaceUnion(JMLEqualsToObjectMap 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:   JMLEqualsToObjectMap.extendUnion
See Also:   JMLEqualsToObjectMap.disjointUnion
See Also:   JMLEqualsToObjectRelation.union



clone
public Object clone()(Code)



compose
public JMLValueToObjectMap compose(JMLValueToEqualsMap 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:   JMLEqualsToObjectMap.compose(JMLObjectToEqualsMap)



compose
public JMLObjectToObjectMap compose(JMLObjectToEqualsMap 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:   JMLEqualsToObjectMap.compose(JMLValueToEqualsMap)



disjointUnion
public JMLEqualsToObjectMap disjointUnion(JMLEqualsToObjectMap 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:   JMLEqualsToObjectMap.extendUnion
See Also:   JMLEqualsToObjectMap.clashReplaceUnion
See Also:   JMLEqualsToObjectRelation.union



extend
public JMLEqualsToObjectMap 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:   JMLEqualsToObjectRelation.insert(ObjectObject)



extendUnion
public JMLEqualsToObjectMap extendUnion(JMLEqualsToObjectMap 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:   JMLEqualsToObjectMap.clashReplaceUnion
See Also:   JMLEqualsToObjectMap.disjointUnion
See Also:   JMLEqualsToObjectRelation.union



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



rangeRestrictedTo
public JMLEqualsToObjectMap rangeRestrictedTo(JMLObjectSet 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:   JMLEqualsToObjectMap.restrictedTo
See Also:   JMLEqualsToObjectRelation.restrictRangeTo



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



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



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



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



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

Methods inherited from org.jmlspecs.models.JMLEqualsToObjectRelation
public JMLEqualsToObjectRelation add(Object dv, Object rv) throws NullPointerException, IllegalStateException(Code)(Java Doc)
public JMLEqualsToObjectRelationEnumerator associations()(Code)(Java Doc)
public Object clone()(Code)(Java Doc)
public JMLValueToObjectRelation compose(JMLValueToEqualsRelation othRel)(Code)(Java Doc)
public JMLObjectToObjectRelation compose(JMLObjectToEqualsRelation othRel)(Code)(Java Doc)
public JMLEqualsToObjectRelation difference(JMLEqualsToObjectRelation othRel)(Code)(Java Doc)
public JMLEqualsSet domain()(Code)(Java Doc)
public JMLEqualsSetEnumerator domainElements()(Code)(Java Doc)
public JMLObjectSet elementImage(Object dv)(Code)(Java Doc)
public JMLEqualsToObjectRelationEnumerator 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(JMLEqualsObjectPair pair)(Code)(Java Doc)
public boolean has(Object obj)(Code)(Java Doc)
public int hashCode()(Code)(Java Doc)
public JMLObjectSet image(JMLEqualsSet dom)(Code)(Java Doc)
public JMLValueSet imagePairSet()(Code)(Java Doc)
public JMLEqualsToObjectRelationImageEnumerator imagePairs()(Code)(Java Doc)
public JMLEqualsToObjectRelation insert(JMLEqualsObjectPair pair) throws IllegalStateException(Code)(Java Doc)
public int int_size()(Code)(Java Doc)
public JMLEqualsToObjectRelation intersection(JMLEqualsToObjectRelation othRel)(Code)(Java Doc)
public JMLObjectToEqualsRelation inverse()(Code)(Java Doc)
public JMLEqualsSet inverseElementImage(Object rv)(Code)(Java Doc)
public JMLEqualsSet inverseImage(JMLObjectSet 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 JMLObjectSet range()(Code)(Java Doc)
public JMLObjectSetEnumerator rangeElements()(Code)(Java Doc)
public JMLEqualsToObjectRelation remove(Object dv, Object rv)(Code)(Java Doc)
public JMLEqualsToObjectRelation remove(JMLEqualsObjectPair pair)(Code)(Java Doc)
public JMLEqualsToObjectRelation removeFromDomain(Object dv)(Code)(Java Doc)
public JMLEqualsToObjectRelation restrictDomainTo(JMLEqualsSet dom)(Code)(Java Doc)
public JMLEqualsToObjectRelation restrictRangeTo(JMLObjectSet rng)(Code)(Java Doc)
public static JMLEqualsToObjectRelation singleton(Object dv, Object rv)(Code)(Java Doc)
public static JMLEqualsToObjectRelation singleton(JMLEqualsObjectPair pair)(Code)(Java Doc)
public JMLValueBag toBag()(Code)(Java Doc)
public JMLEqualsToObjectMap toFunction()(Code)(Java Doc)
public JMLValueSequence toSequence()(Code)(Java Doc)
public JMLValueSet toSet()(Code)(Java Doc)
public String toString()(Code)(Java Doc)
public JMLEqualsToObjectRelation union(JMLEqualsToObjectRelation 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.