Java Doc for JMLEqualsToEqualsMap.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.JMLEqualsToEqualsRelation
      org.jmlspecs.models.JMLEqualsToEqualsMap

JMLEqualsToEqualsMap
public class JMLEqualsToEqualsMap extends JMLEqualsToEqualsRelation (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 JMLEqualsToEqualsRelation , and as such as can be treated as a binary relation or a set valued function also. See the documentation for JMLEqualsToEqualsRelation 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:   JMLEqualsToEqualsRelation
See Also:   JMLEqualsToEqualsRelationEnumerator
See Also:   JMLEqualsToEqualsRelationImageEnumerator
See Also:   JMLValueSet
See Also:   JMLObjectSet
See Also:   JMLObjectToObjectMap
See Also:   JMLValueToObjectMap
See Also:   JMLObjectToValueMap
See Also:   JMLValueToValueMap
See Also:   JMLEqualsToEqualsRelation.toFunction



Field Summary
final public static  JMLEqualsToEqualsMapEMPTY
     The empty JMLEqualsToEqualsMap.

Constructor Summary
public  JMLEqualsToEqualsMap()
     Initialize this map to be the empty mapping.
public  JMLEqualsToEqualsMap(Object dv, Object rv)
     Initialize this map to be a mapping that maps the given domain element to the given range element.
public  JMLEqualsToEqualsMap(JMLEqualsEqualsPair pair)
     Initialize this map to be a mapping that maps the key in the given pair to the value in that pair.
protected  JMLEqualsToEqualsMap(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  JMLEqualsToEqualsMapclashReplaceUnion(JMLEqualsToEqualsMap 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(JMLValueToEqualsMap othMap)
     Return a new map that is the composition of this and the given map.
public  JMLObjectToEqualsMapcompose(JMLObjectToEqualsMap othMap)
     Return a new map that is the composition of this and the given map.
public  JMLEqualsToEqualsMapdisjointUnion(JMLEqualsToEqualsMap othMap)
     Return a map that is the disjoint union of this and othMap.
public  JMLEqualsToEqualsMapextend(Object dv, Object rv)
     Return a new map that is like this but maps the given domain element to the given range element.
public  JMLEqualsToEqualsMapextendUnion(JMLEqualsToEqualsMap 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  JMLEqualsToEqualsMaprangeRestrictedTo(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  JMLEqualsToEqualsMapremoveDomainElement(Object dv)
     Return a new map that is like this but has no association for the given domain element.
public  JMLEqualsToEqualsMaprestrictedTo(JMLEqualsSet dom)
     Return a new map that only maps elements in the given domain to the corresponding range elements in this map.
public static  JMLEqualsToEqualsMapsingletonMap(Object dv, Object rv)
     Return the singleton map containing the given association.
public static  JMLEqualsToEqualsMapsingletonMap(JMLEqualsEqualsPair pair)
     Return the singleton map containing the association described by the given pair.

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




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



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



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



JMLEqualsToEqualsMap
protected JMLEqualsToEqualsMap(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:   JMLEqualsToEqualsRelation.isDefinedAt
See Also:   JMLEqualsToEqualsRelation.elementImage
See Also:   JMLEqualsToEqualsRelation.image



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



clone
public Object clone()(Code)



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



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



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



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



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



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



rangeRestrictedTo
public JMLEqualsToEqualsMap 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:   JMLEqualsToEqualsMap.restrictedTo
See Also:   JMLEqualsToEqualsRelation.restrictRangeTo



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



restrictedTo
public JMLEqualsToEqualsMap 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:   JMLEqualsToEqualsMap.rangeRestrictedTo
See Also:   JMLEqualsToEqualsRelation.restrictDomainTo



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



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



Fields inherited from org.jmlspecs.models.JMLEqualsToEqualsRelation
final public static JMLEqualsToEqualsRelation 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.JMLEqualsToEqualsRelation
public JMLEqualsToEqualsRelation add(Object dv, Object rv) throws NullPointerException, IllegalStateException(Code)(Java Doc)
public JMLEqualsToEqualsRelationEnumerator associations()(Code)(Java Doc)
public Object clone()(Code)(Java Doc)
public JMLValueToEqualsRelation compose(JMLValueToEqualsRelation othRel)(Code)(Java Doc)
public JMLObjectToEqualsRelation compose(JMLObjectToEqualsRelation othRel)(Code)(Java Doc)
public JMLEqualsToEqualsRelation difference(JMLEqualsToEqualsRelation othRel)(Code)(Java Doc)
public JMLEqualsSet domain()(Code)(Java Doc)
public JMLEqualsSetEnumerator domainElements()(Code)(Java Doc)
public JMLEqualsSet elementImage(Object dv)(Code)(Java Doc)
public JMLEqualsToEqualsRelationEnumerator 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(JMLEqualsEqualsPair pair)(Code)(Java Doc)
public boolean has(Object obj)(Code)(Java Doc)
public int hashCode()(Code)(Java Doc)
public JMLEqualsSet image(JMLEqualsSet dom)(Code)(Java Doc)
public JMLValueSet imagePairSet()(Code)(Java Doc)
public JMLEqualsToEqualsRelationImageEnumerator imagePairs()(Code)(Java Doc)
public JMLEqualsToEqualsRelation insert(JMLEqualsEqualsPair pair) throws IllegalStateException(Code)(Java Doc)
public int int_size()(Code)(Java Doc)
public JMLEqualsToEqualsRelation intersection(JMLEqualsToEqualsRelation othRel)(Code)(Java Doc)
public JMLEqualsToEqualsRelation inverse()(Code)(Java Doc)
public JMLEqualsSet inverseElementImage(Object rv)(Code)(Java Doc)
public JMLEqualsSet 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 JMLEqualsToEqualsRelation remove(Object dv, Object rv)(Code)(Java Doc)
public JMLEqualsToEqualsRelation remove(JMLEqualsEqualsPair pair)(Code)(Java Doc)
public JMLEqualsToEqualsRelation removeFromDomain(Object dv)(Code)(Java Doc)
public JMLEqualsToEqualsRelation restrictDomainTo(JMLEqualsSet dom)(Code)(Java Doc)
public JMLEqualsToEqualsRelation restrictRangeTo(JMLEqualsSet rng)(Code)(Java Doc)
public static JMLEqualsToEqualsRelation singleton(Object dv, Object rv)(Code)(Java Doc)
public static JMLEqualsToEqualsRelation singleton(JMLEqualsEqualsPair pair)(Code)(Java Doc)
public JMLValueBag toBag()(Code)(Java Doc)
public JMLEqualsToEqualsMap toFunction()(Code)(Java Doc)
public JMLValueSequence toSequence()(Code)(Java Doc)
public JMLValueSet toSet()(Code)(Java Doc)
public String toString()(Code)(Java Doc)
public JMLEqualsToEqualsRelation union(JMLEqualsToEqualsRelation 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.