Java Doc for JMLEqualsToValueMap.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.JMLEqualsToValueRelation
      org.jmlspecs.models.JMLEqualsToValueMap

JMLEqualsToValueMap
public class JMLEqualsToValueMap extends JMLEqualsToValueRelation (Code)
Maps (i.e., binary relations that are functional) from non-null elements of Object to non-null elements of JMLType . The first type, Object, is called the domain type of the map; the second type, JMLType, 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 JMLEqualsToValueRelation , and as such as can be treated as a binary relation or a set valued function also. See the documentation for JMLEqualsToValueRelation 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:   JMLEqualsToValueRelation
See Also:   JMLEqualsToValueRelationEnumerator
See Also:   JMLEqualsToValueRelationImageEnumerator
See Also:   JMLValueSet
See Also:   JMLObjectSet
See Also:   JMLObjectToObjectMap
See Also:   JMLValueToObjectMap
See Also:   JMLObjectToValueMap
See Also:   JMLValueToValueMap
See Also:   JMLEqualsToValueRelation.toFunction



Field Summary
final public static  JMLEqualsToValueMapEMPTY
     The empty JMLEqualsToValueMap.

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

Method Summary
public  JMLTypeapply(Object dv)
     Return the range element corresponding to dv, if there is one.
public  JMLEqualsToValueMapclashReplaceUnion(JMLEqualsToValueMap othMap, JMLType 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  JMLValueToValueMapcompose(JMLValueToEqualsMap othMap)
     Return a new map that is the composition of this and the given map.
public  JMLObjectToValueMapcompose(JMLObjectToEqualsMap othMap)
     Return a new map that is the composition of this and the given map.
public  JMLEqualsToValueMapdisjointUnion(JMLEqualsToValueMap othMap)
     Return a map that is the disjoint union of this and othMap.
public  JMLEqualsToValueMapextend(Object dv, JMLType rv)
     Return a new map that is like this but maps the given domain element to the given range element.
public  JMLEqualsToValueMapextendUnion(JMLEqualsToValueMap 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  JMLEqualsToValueMaprangeRestrictedTo(JMLValueSet rng)
     Return a new map that is like this map but only contains associations that map to range elements in the given set.
public  JMLEqualsToValueMapremoveDomainElement(Object dv)
     Return a new map that is like this but has no association for the given domain element.
public  JMLEqualsToValueMaprestrictedTo(JMLEqualsSet dom)
     Return a new map that only maps elements in the given domain to the corresponding range elements in this map.
public static  JMLEqualsToValueMapsingletonMap(Object dv, JMLType rv)
     Return the singleton map containing the given association.
public static  JMLEqualsToValueMapsingletonMap(JMLEqualsValuePair pair)
     Return the singleton map containing the association described by the given pair.

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




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



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



JMLEqualsToValueMap
public JMLEqualsToValueMap(JMLEqualsValuePair 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:   JMLEqualsToValueMap.singletonMap(JMLEqualsValuePair)
See Also:   JMLEqualsToValueMap.JMLEqualsToValueMap(Object,JMLType)



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




Method Detail
apply
public JMLType 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:   JMLEqualsToValueRelation.isDefinedAt
See Also:   JMLEqualsToValueRelation.elementImage
See Also:   JMLEqualsToValueRelation.image



clashReplaceUnion
public JMLEqualsToValueMap clashReplaceUnion(JMLEqualsToValueMap othMap, JMLType 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:   JMLEqualsToValueMap.extendUnion
See Also:   JMLEqualsToValueMap.disjointUnion
See Also:   JMLEqualsToValueRelation.union



clone
public Object clone()(Code)



compose
public JMLValueToValueMap 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:   JMLEqualsToValueMap.compose(JMLObjectToEqualsMap)



compose
public JMLObjectToValueMap 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:   JMLEqualsToValueMap.compose(JMLValueToEqualsMap)



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



extend
public JMLEqualsToValueMap extend(Object dv, JMLType 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:   JMLEqualsToValueRelation.insert(ObjectJMLType)



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



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



rangeRestrictedTo
public JMLEqualsToValueMap rangeRestrictedTo(JMLValueSet 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:   JMLEqualsToValueMap.restrictedTo
See Also:   JMLEqualsToValueRelation.restrictRangeTo



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



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



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



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



Fields inherited from org.jmlspecs.models.JMLEqualsToValueRelation
final public static JMLEqualsToValueRelation 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.JMLEqualsToValueRelation
public JMLEqualsToValueRelation add(Object dv, JMLType rv) throws NullPointerException, IllegalStateException(Code)(Java Doc)
public JMLEqualsToValueRelationEnumerator associations()(Code)(Java Doc)
public Object clone()(Code)(Java Doc)
public JMLValueToValueRelation compose(JMLValueToEqualsRelation othRel)(Code)(Java Doc)
public JMLObjectToValueRelation compose(JMLObjectToEqualsRelation othRel)(Code)(Java Doc)
public JMLEqualsToValueRelation difference(JMLEqualsToValueRelation othRel)(Code)(Java Doc)
public JMLEqualsSet domain()(Code)(Java Doc)
public JMLEqualsSetEnumerator domainElements()(Code)(Java Doc)
public JMLValueSet elementImage(Object dv)(Code)(Java Doc)
public JMLEqualsToValueRelationEnumerator elements()(Code)(Java Doc)
public boolean equals(Object obj)(Code)(Java Doc)
public boolean has(Object dv, JMLType rv)(Code)(Java Doc)
public boolean has(JMLEqualsValuePair pair)(Code)(Java Doc)
public boolean has(Object obj)(Code)(Java Doc)
public int hashCode()(Code)(Java Doc)
public JMLValueSet image(JMLEqualsSet dom)(Code)(Java Doc)
public JMLValueSet imagePairSet()(Code)(Java Doc)
public JMLEqualsToValueRelationImageEnumerator imagePairs()(Code)(Java Doc)
public JMLEqualsToValueRelation insert(JMLEqualsValuePair pair) throws IllegalStateException(Code)(Java Doc)
public int int_size()(Code)(Java Doc)
public JMLEqualsToValueRelation intersection(JMLEqualsToValueRelation othRel)(Code)(Java Doc)
public JMLValueToEqualsRelation inverse()(Code)(Java Doc)
public JMLEqualsSet inverseElementImage(JMLType rv)(Code)(Java Doc)
public JMLEqualsSet inverseImage(JMLValueSet 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 JMLValueSet range()(Code)(Java Doc)
public JMLValueSetEnumerator rangeElements()(Code)(Java Doc)
public JMLEqualsToValueRelation remove(Object dv, JMLType rv)(Code)(Java Doc)
public JMLEqualsToValueRelation remove(JMLEqualsValuePair pair)(Code)(Java Doc)
public JMLEqualsToValueRelation removeFromDomain(Object dv)(Code)(Java Doc)
public JMLEqualsToValueRelation restrictDomainTo(JMLEqualsSet dom)(Code)(Java Doc)
public JMLEqualsToValueRelation restrictRangeTo(JMLValueSet rng)(Code)(Java Doc)
public static JMLEqualsToValueRelation singleton(Object dv, JMLType rv)(Code)(Java Doc)
public static JMLEqualsToValueRelation singleton(JMLEqualsValuePair pair)(Code)(Java Doc)
public JMLValueBag toBag()(Code)(Java Doc)
public JMLEqualsToValueMap toFunction()(Code)(Java Doc)
public JMLValueSequence toSequence()(Code)(Java Doc)
public JMLValueSet toSet()(Code)(Java Doc)
public String toString()(Code)(Java Doc)
public JMLEqualsToValueRelation union(JMLEqualsToValueRelation 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.