Source Code Cross Referenced for JMLObjectToValueRelation.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 Referenced  Class Diagram Java Document (Java Doc) 


0001:        // @(#)$Id: JMLObjectToValueRelation.java 1.1.1.1 Mon, 09 May 2005 15:27:50 +0200 engelc $
0002:
0003:        // Copyright (C) 1998, 1999, 2002 Iowa State University
0004:
0005:        // This file is part of JML
0006:
0007:        // JML is free software; you can redistribute it and/or modify
0008:        // it under the terms of the GNU General Public License as published by
0009:        // the Free Software Foundation; either version 2, or (at your option)
0010:        // any later version.
0011:
0012:        // JML is distributed in the hope that it will be useful,
0013:        // but WITHOUT ANY WARRANTY; without even the implied warranty of
0014:        // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
0015:        // GNU General Public License for more details.
0016:
0017:        // You should have received a copy of the GNU General Public License
0018:        // along with JML; see the file COPYING.  If not, write to
0019:        // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
0020:
0021:        package org.jmlspecs.models;
0022:
0023:        import java.util.Enumeration;
0024:
0025:        /** Binary relations (or set-valued functions) from non-null elements
0026:         *  of {@link Object} to non-null elements of {@link
0027:         *  JMLType}.  The first type, <kbd>Object</kbd>, is called
0028:         *  the domain type of the relation; the second type,
0029:         *  <kbd>JMLType</kbd>, is called the range type of the relation.
0030:         *  A relation can be seen as a set of pairs, of form <em>(dv,
0031:         *  rv)</em>, consisting of an element of the domain type,
0032:         *  <em>dv</em>, and an element of the range type, <em>rv</em>.
0033:         *  Alternatively, it can be seen as a set-valued function that
0034:         *  relates each element of the domain type to some set of elements of
0035:         *  the range type (a {@link JMLValueSet}).
0036:         *
0037:         *  <p> This type considers elements <kbd>val</kbd> and <kbd>dv<kbd>
0038:         *  of the domain type, to be distinct just when
0039:         *  <kbd>val != dv</kbd>.  It considers elements of
0040:         *  <kbd>r</kbd> and <kbd>rv</kbd> of the range type to be distinct
0041:         *  just when <kbd>!r.equals(rv)</kbd>.  Cloning takes place for
0042:         *  the domain or range elements if the corresponding domain or range
0043:         *  type is {@link JMLType}.
0044:         *
0045:         * @version $Revision: 1.1.1.1 $
0046:         * @author Gary T. Leavens
0047:         * @author Clyde Ruby
0048:         * @see JMLCollection
0049:         * @see JMLType
0050:         * @see JMLObjectToValueMap
0051:         * @see JMLObjectToValueRelationEnumerator
0052:         * @see JMLObjectToValueRelationImageEnumerator
0053:         * @see JMLValueSet
0054:         * @see JMLObjectSet
0055:         * @see JMLObjectToObjectRelation
0056:         * @see JMLValueToObjectRelation
0057:         * @see JMLObjectToValueRelation
0058:         * @see JMLValueToValueRelation
0059:         */
0060:        //-@ immutable
0061:        public/*@ pure @*/class JMLObjectToValueRelation implements 
0062:                JMLCollection {
0063:
0064:            /** The set of pairs of keys and values conceptually contained in
0065:             * this object.
0066:             */
0067:            //@ public model JMLValueSet theRelation;
0068:            /*@ public invariant
0069:              @      (\forall Object obj; theRelation.has((JMLType)obj);
0070:              @            obj != null
0071:              @         && obj instanceof JMLObjectValuePair
0072:              @         && ((JMLObjectValuePair)obj).key != null
0073:              @         && ((JMLObjectValuePair)obj).value != null);
0074:              @ public invariant_redundantly
0075:              @      (* Every element of 'theRelation'is a JMLObjectValuePair
0076:              @         whose key and value are not null *);
0077:              @*/
0078:
0079:            //@ public invariant elementType == \type(JMLObjectValuePair);
0080:            //@ public invariant !containsNull;
0081:            /** The set of elements in the domain of this relation.
0082:             */
0083:            protected final/*@ non_null @*/JMLObjectSet domain_;
0084:            //@                                             in theRelation;
0085:
0086:            /** The set representing the image pairs in the relation.  The
0087:             * elements of this set are JMLObjectValuePairs, which are all
0088:             * non-null.  Each such pair has a key which is an element in
0089:             * domain_ and a value which is a JMLValueSet containing all of
0090:             * the elements that the key of the pair is related to.
0091:             */
0092:            protected final/*@ non_null @*/JMLValueSet imagePairSet_;
0093:            //@                                             in theRelation;
0094:
0095:            /** The size (number of pairs) of this relation.
0096:             */
0097:            protected final int size_;
0098:
0099:            //@                  in theRelation;
0100:
0101:            //@ protected represents theRelation <- toSet();
0102:
0103:            /*@ protected invariant
0104:              @     imagePairSet_.int_size() == domain_.int_size()
0105:              @    && (\forall Object dv; dv != null && domain_.has(dv);
0106:              @          imagePairSet_
0107:              @            .has(new JMLObjectValuePair(dv, elementImage(dv))));
0108:              @*/
0109:            //@ protected invariant_redundantly imagePairSet_ == imagePairSet();
0110:            //@ protected invariant size_ == theRelation.int_size();
0111:            //@ protected invariant size_ >= 0;
0112:            //@ public    invariant owner == null;
0113:            //************************* Constructors ********************************
0114:            /** Initialize this to be an empty relation. That is, the value is
0115:             * an empty set of pairs.
0116:             * @see #EMPTY
0117:             */
0118:            /*@  public normal_behavior
0119:              @    assignable theRelation, owner, elementType, containsNull;
0120:              @    ensures theRelation.equals(new JMLValueSet());
0121:              @    ensures_redundantly theRelation.isEmpty();
0122:              @*/
0123:            public JMLObjectToValueRelation() {
0124:                domain_ = new JMLObjectSet();
0125:                imagePairSet_ = new JMLValueSet();
0126:                size_ = 0;
0127:            }
0128:
0129:            /** Initialize this to be a relation containing a single association
0130:             * between the given domain and range elements.
0131:             * @see #singleton(Object, JMLType)
0132:             * @see #JMLObjectToValueRelation(JMLObjectValuePair)
0133:             */
0134:            /*@  public normal_behavior
0135:              @    requires dv != null && rv != null;
0136:              @    assignable theRelation, owner, elementType, containsNull;
0137:              @    ensures theRelation.int_size() == 1;
0138:              @    ensures elementImage(dv).has(rv);
0139:              @    ensures_redundantly isDefinedAt(dv);
0140:              @*/
0141:            public JMLObjectToValueRelation(/*@ non_null @*/Object dv,
0142:            /*@ non_null @*/JMLType rv) {
0143:                size_ = 1;
0144:                domain_ = new JMLObjectSet(dv);
0145:                JMLValueSet img = new JMLValueSet(rv);
0146:                imagePairSet_ = new JMLValueSet(new JMLObjectValuePair(dv, img));
0147:            }
0148:
0149:            /** Initialize this to be a relation containing a single association
0150:             *  given by the pair.
0151:             * @see #singleton(JMLObjectValuePair)
0152:             * @see #JMLObjectToValueRelation(Object, JMLType)
0153:             */
0154:            /*@  public normal_behavior
0155:              @    requires pair != null;
0156:              @    assignable theRelation, owner, elementType, containsNull;
0157:              @    ensures theRelation.int_size() == 1 && theRelation.has(pair);
0158:              @*/
0159:            public JMLObjectToValueRelation(/*@ non_null @*/
0160:            JMLObjectValuePair pair) {
0161:                this (pair.key, pair.value);
0162:            }
0163:
0164:            /** Initialize this using the given representation.
0165:             */
0166:            /*@  protected normal_behavior
0167:              @    requires ipset != null && dom != null && dom.int_size() <= sz;
0168:              @    assignable theRelation, owner, elementType, containsNull;
0169:              @    assignable_redundantly domain_, imagePairSet_, size_;
0170:              @    ensures imagePairSet_ == ipset && domain_ == dom && size_ == sz;
0171:              @
0172:              @ implies_that
0173:              @    requires ipset != null && dom != null && 0 <= sz;
0174:              @    ensures imagePairSet_ == ipset && domain_ == dom && size_ == sz;
0175:              @*/
0176:            protected JMLObjectToValueRelation(
0177:                    /*@ non_null @*/JMLValueSet ipset,
0178:                    /*@ non_null @*/JMLObjectSet dom, int sz) {
0179:                domain_ = dom;
0180:                imagePairSet_ = ipset;
0181:                size_ = sz;
0182:            }
0183:
0184:            //**************************** Static methods ****************************
0185:
0186:            /** The empty JMLObjectToValueRelation.
0187:             * @see #JMLObjectToValueRelation()
0188:             */
0189:            public static final/*@ non_null @*/JMLObjectToValueRelation EMPTY = new JMLObjectToValueRelation();
0190:
0191:            /** Return the singleton relation containing the given association.
0192:             * @see #singleton(JMLObjectValuePair)
0193:             * @see #JMLObjectToValueRelation(Object, JMLType)
0194:             */
0195:            /*@ public normal_behavior
0196:              @    requires dv != null && rv != null;
0197:              @    ensures \result != null
0198:              @         && \result.equals(new JMLObjectToValueRelation(dv, rv));
0199:              @*/
0200:            public static/*@ pure @*//*@ non_null @*/
0201:            JMLObjectToValueRelation singleton(/*@ non_null @*/Object dv,
0202:            /*@ non_null @*/JMLType rv) {
0203:                return new JMLObjectToValueRelation(dv, rv);
0204:            }
0205:
0206:            /** Return the singleton relation containing the association
0207:             * described by the given pair.
0208:             * @see #singleton(Object, JMLType)
0209:             * @see #JMLObjectToValueRelation(JMLObjectValuePair)
0210:             */
0211:            /*@ public normal_behavior
0212:              @    requires pair != null;
0213:              @    ensures \result != null
0214:              @         && \result.equals(singleton(pair.key, pair.value));
0215:              @*/
0216:            public static/*@ pure @*//*@ non_null @*/
0217:            JMLObjectToValueRelation singleton(
0218:                    /*@ non_null @*/JMLObjectValuePair pair) {
0219:                return singleton(pair.key, pair.value);
0220:            }
0221:
0222:            //**************************** Observers **********************************
0223:
0224:            /** Tells whether this relation is a function.
0225:             * @see JMLObjectToValueMap
0226:             */
0227:            /*@   public normal_behavior
0228:              @     ensures \result == (\forall Object dv; isDefinedAt(dv);
0229:              @                                  elementImage(dv).int_size() == 1);
0230:              @*/
0231:            public boolean isaFunction() {
0232:                return size_ == domain_.int_size();
0233:            }
0234:
0235:            /** Returns a set containing all the range elements that this
0236:             * relation relates to the given domain element.
0237:             * @see #image
0238:             * @see JMLObjectToValueMap#apply
0239:             */
0240:            /*@  public normal_behavior
0241:              @    ensures (\forall JMLObjectValuePair pair;
0242:              @                      theRelation.has(pair);
0243:              @                      pair.keyEquals(dv) ==> \result.has(pair.value));
0244:              @    ensures (\forall JMLType o; \result.has(o);
0245:              @                  (\exists JMLObjectValuePair pair;
0246:              @                      theRelation.has(pair);
0247:              @                      pair.keyEquals(dv) && pair.valueEquals(o)));
0248:              @    ensures_redundantly !isDefinedAt(dv) ==> \result.isEmpty();
0249:              @
0250:              @ implies_that
0251:              @    ensures \result != null && !\result.containsNull;
0252:              @*/
0253:            public/*@ non_null @*/
0254:            JMLValueSet elementImage(Object dv) {
0255:                JMLObjectToValueRelationImageEnumerator imagePairEnum = this 
0256:                        .imagePairs();
0257:                JMLObjectValuePair imagePair;
0258:                while (imagePairEnum.hasMoreElements()) {
0259:                    imagePair = imagePairEnum.nextImagePair();
0260:                    if (imagePair.keyEquals(dv)) {
0261:                        JMLValueSet res = (JMLValueSet) imagePair.value;
0262:                        return res;
0263:                    }
0264:                }
0265:                return new JMLValueSet();
0266:            }
0267:
0268:            /** Returns a set containing all the range elements that this
0269:             * relation relates to the elements of the given set of domain elements.
0270:             * @see #elementImage
0271:             * @see #inverseImage
0272:             * @see JMLObjectToValueMap#apply
0273:             */
0274:            /*@  public normal_behavior
0275:              @    requires dom != null;
0276:              @    ensures (\forall JMLType o; \result.has(o)
0277:              @              <==> (\exists JMLObjectValuePair pair;
0278:              @                      theRelation.has(pair);
0279:              @                      dom.has(pair.key) && pair.valueEquals(o)));
0280:              @    ensures_redundantly
0281:              @              (\forall JMLObjectValuePair pair;
0282:              @                      theRelation.has(pair);
0283:              @                      dom.has(pair.key) ==> \result.has(pair.value));
0284:              @
0285:              @ implies_that
0286:              @    ensures \result != null && !\result.containsNull;
0287:              @*/
0288:            public/*@ non_null @*/
0289:            JMLValueSet image(/*@ non_null @*/JMLObjectSet dom) {
0290:                JMLValueSet img = new JMLValueSet();
0291:                JMLObjectToValueRelationImageEnumerator imagePairEnum = this 
0292:                        .imagePairs();
0293:                JMLObjectValuePair imagePair;
0294:                //@ loop_invariant !img.containsNull;
0295:                while (imagePairEnum.hasMoreElements()) {
0296:                    imagePair = imagePairEnum.nextImagePair();
0297:                    if (dom.has(imagePair.key)) {
0298:                        JMLValueSet ipv = (JMLValueSet) imagePair.value;
0299:                        img = img.union(ipv);
0300:                    }
0301:                }
0302:                return img;
0303:            }
0304:
0305:            /** Returns the inverse of this relation.  The inverse is the
0306:             *  relation that relates each range element to the corresponding
0307:             *  domain element.
0308:             * @see #inverseImage
0309:             * @see #inverseElementImage
0310:             */
0311:            /*@  public normal_behavior
0312:              @    ensures (\forall JMLValueObjectPair pair; ;
0313:              @                 \result.theRelation.has(pair) 
0314:              @                    == elementImage(pair.value).has(pair.key));
0315:              @*/
0316:            public/*@ non_null @*/JMLValueToObjectRelation inverse() {
0317:                JMLValueToObjectRelation invRel = new JMLValueToObjectRelation();
0318:                JMLObjectToValueRelationEnumerator assocEnum = this 
0319:                        .associations();
0320:                JMLObjectValuePair pair;
0321:                while (assocEnum.hasMoreElements()) {
0322:                    pair = assocEnum.nextPair();
0323:                    invRel = invRel.add(pair.value, pair.key);
0324:                }
0325:                return invRel;
0326:            }
0327:
0328:            /** Return a set of all the domain elements that relate to the
0329:             * given range element.
0330:             * @see #inverseImage
0331:             * @see #inverse
0332:             * @see #elementImage
0333:             */
0334:            /*@  public normal_behavior
0335:              @    ensures \result.equals(inverse().elementImage(rv));
0336:              @
0337:              @ implies_that
0338:              @    ensures \result != null && !\result.containsNull;
0339:              @*/
0340:            public/*@ non_null @*/
0341:            JMLObjectSet inverseElementImage(JMLType rv) {
0342:                JMLObjectSet invImg = new JMLObjectSet();
0343:                JMLObjectToValueRelationImageEnumerator imagePairEnum = this 
0344:                        .imagePairs();
0345:                JMLObjectValuePair imagePair;
0346:                //@ loop_invariant !invImg.containsNull;
0347:                while (imagePairEnum.hasMoreElements()) {
0348:                    imagePair = imagePairEnum.nextImagePair();
0349:                    JMLValueSet img = (JMLValueSet) imagePair.value;
0350:                    if (img.has(rv)) {
0351:                        invImg = invImg.insert(imagePair.key);
0352:                    }
0353:                }
0354:                return invImg;
0355:            }
0356:
0357:            /** Return a set of all the domain elements that relate to some
0358:             * element in the given set of range elements.
0359:             * @see #inverseElementImage
0360:             * @see #inverse
0361:             * @see #image
0362:             */
0363:            /*@  public normal_behavior
0364:              @    requires rng != null;
0365:              @    ensures \result.equals(inverse().image(rng));
0366:              @
0367:              @ implies_that
0368:              @    ensures \result != null && !\result.containsNull;
0369:              @*/
0370:            public/*@ non_null @*/
0371:            JMLObjectSet inverseImage(/*@ non_null @*/JMLValueSet rng) {
0372:                JMLObjectSet invImg = new JMLObjectSet();
0373:                JMLObjectToValueRelationImageEnumerator imagePairEnum = this 
0374:                        .imagePairs();
0375:                JMLObjectValuePair imagePair;
0376:                while (imagePairEnum.hasMoreElements()) {
0377:                    imagePair = imagePairEnum.nextImagePair();
0378:                    JMLValueSet img = (JMLValueSet) imagePair.value;
0379:                    if (!img.intersection(rng).isEmpty()) {
0380:                        invImg = invImg.insert(imagePair.key);
0381:                    }
0382:                }
0383:                return invImg;
0384:            }
0385:
0386:            /** Tells whether this relation associates any range element to the
0387:             * given domain element.
0388:             * @see #domain()
0389:             */
0390:            /*@  public normal_behavior
0391:              @     ensures \result == (elementImage(dv).int_size() > 0);
0392:              @     ensures_redundantly dv == null ==> !\result;
0393:              @*/
0394:            public boolean isDefinedAt(Object dv) {
0395:                return domain_.has(dv);
0396:            }
0397:
0398:            /** Tells whether this associates the given key to the given value.
0399:             * @see #isDefinedAt
0400:             * @see #has(JMLObjectValuePair)
0401:             */
0402:            /*@  public normal_behavior
0403:              @     ensures \result <==> domain().has(dv) && elementImage(dv).has(rv);
0404:              @     ensures_redundantly dv == null || rv == null ==> !\result;
0405:              @*/
0406:            public/*@ pure @*/boolean has(Object dv, JMLType rv) {
0407:                return domain_.has(dv) && elementImage(dv).has(rv);
0408:            }
0409:
0410:            /** Tells whether this associates the given key to the given value.
0411:             * @see #isDefinedAt
0412:             * @see #has(Object, JMLType)
0413:             */
0414:            /*@  public normal_behavior
0415:              @     requires pair != null;
0416:              @     ensures \result <==> has(pair.key, pair.value);
0417:              @*/
0418:            public/*@ pure @*/boolean has(
0419:                    /*@ non_null @*/JMLObjectValuePair pair) {
0420:                return has(pair.key, pair.value);
0421:            }
0422:
0423:            /** Tells whether this associates the given key to the given value.
0424:             * @see #isDefinedAt
0425:             * @see #has(JMLObjectValuePair)
0426:             */
0427:            /*@ also
0428:              @    public normal_behavior
0429:              @      ensures \result <==>
0430:              @              obj != null
0431:              @           && obj instanceof JMLObjectValuePair
0432:              @           && has((JMLObjectValuePair) obj);
0433:              @*/
0434:            public/*@ pure @*/boolean has(Object obj) {
0435:                return obj != null && obj instanceof  JMLObjectValuePair
0436:                        && has((JMLObjectValuePair) obj);
0437:            }
0438:
0439:            /** Tells whether the relation is empty.
0440:             * @see #int_size()
0441:             */
0442:            /*@  public normal_behavior
0443:              @    ensures \result == (theRelation.int_size() == 0);
0444:              @*/
0445:            public boolean isEmpty() {
0446:                return size_ == 0;
0447:            }
0448:
0449:            /** Return a clone of this object.
0450:             */
0451:            /*@ also
0452:              @  public normal_behavior
0453:              @    ensures \result instanceof JMLObjectToValueRelation
0454:              @         && ((JMLObjectToValueRelation)\result)
0455:              @                    .theRelation.equals(this.theRelation);
0456:              @*/
0457:            public Object clone() {
0458:                return new JMLObjectToValueRelation(imagePairSet_, domain_,
0459:                        size_);
0460:            }
0461:
0462:            /** Test whether this object's value is equal to the given argument.
0463:             */
0464:            /*@ also
0465:              @  public normal_behavior
0466:              @    requires obj != null && obj instanceof JMLObjectToValueRelation;
0467:              @    ensures \result == 
0468:              @            this.theRelation.equals(
0469:              @                    ((JMLObjectToValueRelation)obj).theRelation);
0470:              @ also 
0471:              @  public normal_behavior
0472:              @    requires obj == null
0473:              @          || !(obj instanceof JMLObjectToValueRelation);
0474:              @    ensures !\result;
0475:              @*/
0476:            public boolean equals(Object obj) {
0477:                if (obj == null || !(obj instanceof  JMLObjectToValueRelation)) {
0478:                    return false;
0479:                }
0480:
0481:                JMLObjectToValueRelation rel = (JMLObjectToValueRelation) obj;
0482:
0483:                if (size_ != rel.int_size()) {
0484:                    return false;
0485:                }
0486:
0487:                JMLObjectToValueRelationImageEnumerator imagePairEnum = this 
0488:                        .imagePairs();
0489:                JMLObjectValuePair imagePair;
0490:                JMLValueSet img;
0491:                while (imagePairEnum.hasMoreElements()) {
0492:                    imagePair = imagePairEnum.nextImagePair();
0493:                    img = (JMLValueSet) imagePair.value;
0494:                    if (!img.equals(rel.elementImage(imagePair.key))) {
0495:                        return false;
0496:                    }
0497:                }
0498:                return true;
0499:            }
0500:
0501:            /** Return a hash code for this object.
0502:             */
0503:            public int hashCode() {
0504:                return imagePairSet_.hashCode();
0505:            }
0506:
0507:            /** Returns a set containing the domain of this relation.
0508:             * @see #domainElements()
0509:             * @see #associations()
0510:             * @see #isDefinedAt
0511:             * @see #image
0512:             * @see #range()
0513:             * @see #inverse()
0514:             */
0515:            /*@  public normal_behavior
0516:              @    ensures (\forall Object dv; ;
0517:              @                 \result.has(dv) == isDefinedAt(dv));
0518:              @*/
0519:            public/*@ non_null @*/JMLObjectSet domain() {
0520:                return domain_;
0521:            }
0522:
0523:            /** Returns a set containing the range of this relation.
0524:             * @see #rangeElements()
0525:             * @see #associations()
0526:             * @see #inverseElementImage
0527:             * @see #domain()
0528:             * @see #inverse()
0529:             */
0530:            /*@  public normal_behavior
0531:              @    ensures (\forall JMLType rv; ;
0532:              @                 \result.has(rv) 
0533:              @                    == (\exists Object dv; ;
0534:              @                            elementImage(dv).has(rv)) 
0535:              @                );
0536:              @*/
0537:            public/*@ non_null @*/JMLValueSet range() {
0538:                JMLValueSet rangeSet = new JMLValueSet();
0539:
0540:                JMLObjectToValueRelationImageEnumerator imagePairEnum = this 
0541:                        .imagePairs();
0542:                JMLObjectValuePair imagePair;
0543:                JMLValueSet img;
0544:                while (imagePairEnum.hasMoreElements()) {
0545:                    imagePair = imagePairEnum.nextImagePair();
0546:                    img = (JMLValueSet) imagePair.value;
0547:                    rangeSet = rangeSet.union(img);
0548:                }
0549:                return rangeSet;
0550:            }
0551:
0552:            private static final String TOO_BIG_TO_INSERT = "Cannot insert into a Relation with Integer.MAX_VALUE elements.";
0553:
0554:            /** Return a relation that is just like this relation, except that
0555:             *  it also associates the given domain element to the given range
0556:             *  element.
0557:             * @see #insert
0558:             */
0559:            /*@  public normal_behavior
0560:              @    requires dv != null && rv != null;
0561:              @    requires int_size() < Integer.MAX_VALUE || elementImage(dv).has(rv);
0562:              @    ensures \result.theRelation.equals(
0563:              @           this.theRelation.insert(new JMLObjectValuePair(dv, rv)));
0564:              @*/
0565:            public/*@ pure @*//*@ non_null @*/
0566:            JMLObjectToValueRelation add(/*@ non_null @*/Object dv,
0567:            /*@ non_null @*/JMLType rv) throws NullPointerException,
0568:                    IllegalStateException {
0569:                if (rv == null) {
0570:                    throw new NullPointerException();
0571:                }
0572:
0573:                JMLValueSet newImagePairSet;
0574:                JMLObjectSet newDom;
0575:                int newSize;
0576:                JMLValueSet img;
0577:
0578:                if (!domain_.has(dv)) {
0579:                    if (size_ == Integer.MAX_VALUE) {
0580:                        throw new IllegalStateException(TOO_BIG_TO_INSERT);
0581:                    }
0582:                    newDom = domain_.insert(dv);
0583:                    newSize = size_ + 1;
0584:                    img = new JMLValueSet(rv);
0585:                    newImagePairSet = imagePairSet_
0586:                            .insert(new JMLObjectValuePair(dv, img));
0587:                } else {
0588:                    newImagePairSet = new JMLValueSet();
0589:                    newDom = domain_;
0590:                    newSize = 0;
0591:
0592:                    JMLObjectToValueRelationImageEnumerator imagePairEnum = this 
0593:                            .imagePairs();
0594:                    JMLObjectValuePair imagePair;
0595:                    while (imagePairEnum.hasMoreElements()) {
0596:                        imagePair = imagePairEnum.nextImagePair();
0597:                        img = (JMLValueSet) imagePair.value;
0598:                        if (imagePair.keyEquals(dv)) {
0599:                            img = img.insert(rv);
0600:                        }
0601:                        int size_inc = img.int_size();
0602:                        if (newSize <= Integer.MAX_VALUE - size_inc) {
0603:                            newSize = newSize + size_inc;
0604:                        } else {
0605:                            throw new IllegalStateException(TOO_BIG_TO_INSERT);
0606:                        }
0607:                        newImagePairSet = newImagePairSet
0608:                                .insert(new JMLObjectValuePair(imagePair.key,
0609:                                        img));
0610:                    }
0611:                }
0612:                return new JMLObjectToValueRelation(newImagePairSet, newDom,
0613:                        newSize);
0614:            }
0615:
0616:            /** Return a relation that is just like this relation, except that
0617:             *  it also includes the association described by the given pair.
0618:             * @see #add
0619:             */
0620:            /*@  public normal_behavior
0621:              @    requires pair != null;
0622:              @    requires int_size() < Integer.MAX_VALUE
0623:              @             || elementImage(pair.key).has(pair.value);
0624:              @    ensures \result.theRelation.equals(this.theRelation.insert(pair));
0625:              @*/
0626:            public/*@ non_null @*/
0627:            JMLObjectToValueRelation insert(/*@ non_null @*/
0628:            JMLObjectValuePair pair) throws IllegalStateException {
0629:                return add(pair.key, pair.value);
0630:            }
0631:
0632:            /** Return a relation that is just like this relation, except that
0633:             *  it does not contain any association with the given domain element.
0634:             * @see #remove(JMLObjectValuePair)
0635:             * @see #removeFromDomain
0636:             */
0637:            /*@  public normal_behavior
0638:              @    ensures \result != null
0639:              @         && (\forall Object val; domain().has(val);
0640:              @             (\forall JMLType r; r != null;
0641:              @                   (elementImage(val).has(r)
0642:              @                      <==> \result.theRelation
0643:              @                            .has(new JMLObjectValuePair(val,r))
0644:              @                          && val != dv)));
0645:              @ implies_that
0646:              @   public normal_behavior
0647:              @    requires dv == null;
0648:              @    ensures \result != null && \result.equals(this);
0649:              @*/
0650:            public/*@ non_null @*/
0651:            JMLObjectToValueRelation removeFromDomain(Object dv) {
0652:                if (!domain_.has(dv)) {
0653:                    return (this );
0654:                }
0655:
0656:                JMLValueSet newImagePairSet = new JMLValueSet();
0657:                JMLObjectSet newDom = domain_.remove(dv);
0658:                int newSize = 0;
0659:
0660:                JMLObjectToValueRelationImageEnumerator imagePairEnum = this 
0661:                        .imagePairs();
0662:                JMLObjectValuePair imagePair;
0663:                while (imagePairEnum.hasMoreElements()) {
0664:                    imagePair = imagePairEnum.nextImagePair();
0665:                    if (!imagePair.keyEquals(dv)) {
0666:                        newImagePairSet = newImagePairSet.insert(imagePair);
0667:                        JMLValueSet img = (JMLValueSet) imagePair.value;
0668:                        newSize = newSize + img.int_size();
0669:                    }
0670:                }
0671:                return new JMLObjectToValueRelation(newImagePairSet, newDom,
0672:                        newSize);
0673:            }
0674:
0675:            /** Return a relation that is just like this relation, except that
0676:             *  it does not contain the association, if any, between the given
0677:             *  domain and range elements.
0678:             * @see #removeFromDomain
0679:             * @see #remove(Object, JMLType)
0680:             * @see #remove(JMLObjectValuePair)
0681:             */
0682:            /*@  public normal_behavior
0683:              @    requires dv != null && rv != null;
0684:              @    ensures \result.theRelation.equals(
0685:              @                theRelation.remove(new JMLObjectValuePair(dv, rv)));
0686:              @   also
0687:              @    requires dv == null || rv == null;
0688:              @    ensures \result != null && \result.equals(this);
0689:              @*/
0690:            public/*@ non_null @*/
0691:            JMLObjectToValueRelation remove(Object dv, JMLType rv) {
0692:                if (!domain_.has(dv)) {
0693:                    return (this );
0694:                }
0695:
0696:                JMLValueSet newImagePairSet = new JMLValueSet();
0697:                JMLObjectSet newDom = domain_;
0698:                int newSize = 0;
0699:
0700:                JMLObjectToValueRelationImageEnumerator imagePairEnum = this 
0701:                        .imagePairs();
0702:                JMLObjectValuePair imagePair;
0703:                JMLValueSet img;
0704:                while (imagePairEnum.hasMoreElements()) {
0705:                    imagePair = imagePairEnum.nextImagePair();
0706:                    img = (JMLValueSet) imagePair.value;
0707:                    int imgSize = img.int_size();
0708:                    if (imagePair.keyEquals(dv)) {
0709:                        img = img.remove(rv);
0710:                        imgSize = img.int_size();
0711:                        if (imgSize > 0) {
0712:                            newImagePairSet = newImagePairSet
0713:                                    .insert(new JMLObjectValuePair(dv, img));
0714:                            newSize = newSize + imgSize;
0715:                        } else {
0716:                            //@ assert imgSize == 0;
0717:                            newDom = newDom.remove(dv);
0718:                        }
0719:                    } else {
0720:                        newImagePairSet = newImagePairSet.insert(imagePair);
0721:                        newSize = newSize + imgSize;
0722:                    }
0723:                }
0724:                return new JMLObjectToValueRelation(newImagePairSet, newDom,
0725:                        newSize);
0726:            }
0727:
0728:            /** Return a relation that is just like this relation, except that
0729:             *  it does not contain association described by the given pair.
0730:             * @see #remove(Object, JMLType)
0731:             * @see #removeFromDomain
0732:             */
0733:            /*@  public normal_behavior
0734:              @    requires pair != null;
0735:              @    ensures \result.theRelation.equals(this.theRelation.remove(pair));
0736:              @*/
0737:            public/*@ non_null @*/
0738:            JMLObjectToValueRelation remove(/*@ non_null @*/
0739:            JMLObjectValuePair pair) {
0740:                return remove(pair.key, pair.value);
0741:            }
0742:
0743:            /** Return a relation that is the composition of the given
0744:             *  relation and this relation.  The composition is done in the
0745:             *  "usual" order, so that if the given relation relates x to y,
0746:             *  and this relation relates y to z, then the result relates x to
0747:             *  z.
0748:             *  @see #compose(JMLObjectToObjectRelation)
0749:             */
0750:            /*@  public normal_behavior
0751:              @    requires othRel != null;
0752:              @    ensures (\forall JMLValueValuePair pair; ;
0753:              @                 \result.theRelation.has(pair) 
0754:              @                    == (\exists Object val;
0755:              @                            othRel.elementImage(pair.key).has(val);
0756:              @                            this.elementImage(val).has(pair.value)
0757:              @                            )
0758:              @                );
0759:              @*/
0760:            public/*@ non_null @*/
0761:            JMLValueToValueRelation compose(
0762:                    /*@ non_null @*/JMLValueToObjectRelation othRel) {
0763:                JMLValueSet newImagePairSet = new JMLValueSet();
0764:                JMLValueSet newDom = new JMLValueSet();
0765:                int newSize = 0;
0766:
0767:                JMLValueToObjectRelationImageEnumerator imagePairEnum = othRel
0768:                        .imagePairs();
0769:                JMLValueValuePair imagePair;
0770:                JMLObjectSet img1;
0771:                JMLValueSet img2;
0772:                int imgSize;
0773:                while (imagePairEnum.hasMoreElements()) {
0774:                    imagePair = imagePairEnum.nextImagePair();
0775:                    img1 = (JMLObjectSet) imagePair.value;
0776:                    img2 = this .image(img1);
0777:                    imgSize = img2.int_size();
0778:                    if (imgSize > 0) {
0779:                        newImagePairSet = newImagePairSet
0780:                                .insert(new JMLValueValuePair(imagePair.key,
0781:                                        img2));
0782:                        newSize = newSize + imgSize;
0783:                        newDom = newDom.insert(imagePair.key);
0784:                    }
0785:                }
0786:                return new JMLValueToValueRelation(newImagePairSet, newDom,
0787:                        newSize);
0788:            }
0789:
0790:            /** Return a relation that is the composition of the given
0791:             *  relation and this relation.  The composition is done in the
0792:             *  "usual" order, so that if the given relation relates x to y,
0793:             *  and this relation relates y to z, then the result relates x to
0794:             *  z.
0795:             *  @see #compose(JMLValueToObjectRelation)
0796:             */
0797:            /*@  public normal_behavior
0798:              @    requires othRel != null;
0799:              @    ensures (\forall JMLValueValuePair pair; ;
0800:              @                 \result.theRelation.has(pair) 
0801:              @                    == (\exists Object val;
0802:              @                            othRel.elementImage(pair.key).has(val);
0803:              @                            this.elementImage(val).has(pair.value)
0804:              @                            )
0805:              @                );
0806:              @*/
0807:            public/*@ non_null @*/
0808:            JMLObjectToValueRelation compose(
0809:                    /*@ non_null @*/JMLObjectToObjectRelation othRel) {
0810:                JMLValueSet newImagePairSet = new JMLValueSet();
0811:                JMLObjectSet newDom = new JMLObjectSet();
0812:                int newSize = 0;
0813:
0814:                JMLObjectToObjectRelationImageEnumerator imagePairEnum = othRel
0815:                        .imagePairs();
0816:                JMLObjectValuePair imagePair;
0817:                JMLObjectSet img1;
0818:                JMLValueSet img2;
0819:                int imgSize;
0820:                while (imagePairEnum.hasMoreElements()) {
0821:                    imagePair = imagePairEnum.nextImagePair();
0822:                    img1 = (JMLObjectSet) imagePair.value;
0823:                    img2 = this .image(img1);
0824:                    imgSize = img2.int_size();
0825:                    if (imgSize > 0) {
0826:                        newImagePairSet = newImagePairSet
0827:                                .insert(new JMLObjectValuePair(imagePair.key,
0828:                                        img2));
0829:                        newSize = newSize + imgSize;
0830:                        newDom = newDom.insert(imagePair.key);
0831:                    }
0832:                }
0833:                return new JMLObjectToValueRelation(newImagePairSet, newDom,
0834:                        newSize);
0835:            }
0836:
0837:            /** Return a relation that union of the this and the given relation.
0838:             *  This is the union of the sets of associations.
0839:             *  @see #difference
0840:             *  @see #intersection
0841:             */
0842:            /*@  public normal_behavior
0843:              @    requires othRel != null;
0844:              @    requires int_size()
0845:              @             < Integer.MAX_VALUE - othRel.difference(this).int_size();
0846:              @    ensures \result.theRelation.equals(
0847:              @                    this.theRelation.union(othRel.theRelation));
0848:              @*/
0849:            public/*@ non_null @*/
0850:            JMLObjectToValueRelation union(
0851:                    /*@ non_null @*/JMLObjectToValueRelation othRel)
0852:                    throws IllegalStateException {
0853:                JMLValueSet newImagePairSet = new JMLValueSet();
0854:                JMLObjectSet newDom = domain_;
0855:                int newSize = 0;
0856:
0857:                JMLObjectToValueRelationImageEnumerator imagePairEnum = this 
0858:                        .imagePairs();
0859:                JMLObjectValuePair imagePair;
0860:                JMLValueSet img;
0861:                while (imagePairEnum.hasMoreElements()) {
0862:                    imagePair = imagePairEnum.nextImagePair();
0863:                    img = (JMLValueSet) imagePair.value;
0864:                    img = img.union(othRel.elementImage(imagePair.key));
0865:                    newImagePairSet = newImagePairSet
0866:                            .insert(new JMLObjectValuePair(imagePair.key, img));
0867:                    int size_inc = img.int_size();
0868:                    if (newSize <= Integer.MAX_VALUE - size_inc) {
0869:                        newSize = newSize + size_inc;
0870:                    } else {
0871:                        throw new IllegalStateException(TOO_BIG_TO_UNION);
0872:                    }
0873:                }
0874:                JMLObjectSet diffDom = othRel.domain().difference(this .domain_);
0875:                imagePairEnum = othRel.imagePairs();
0876:                while (imagePairEnum.hasMoreElements()) {
0877:                    imagePair = imagePairEnum.nextImagePair();
0878:                    if (diffDom.has(imagePair.key)) {
0879:                        newImagePairSet = newImagePairSet.insert(imagePair);
0880:                        newDom = newDom.insert(imagePair.key);
0881:                        img = (JMLValueSet) imagePair.value;
0882:                        int size_inc = img.int_size();
0883:                        if (newSize <= Integer.MAX_VALUE - size_inc) {
0884:                            newSize = newSize + size_inc;
0885:                        } else {
0886:                            throw new IllegalStateException(TOO_BIG_TO_UNION);
0887:                        }
0888:                    }
0889:                }
0890:                return new JMLObjectToValueRelation(newImagePairSet, newDom,
0891:                        newSize);
0892:            }
0893:
0894:            protected static final String TOO_BIG_TO_UNION = "Cannot make a union with more than Integer.MAX_VALUE elements.";
0895:
0896:            /** Return a relation that is the intersection of this and the
0897:             *  given relation.  This is the intersection of the sets of
0898:             *  associations.
0899:             *  @see #difference
0900:             *  @see #union
0901:             */
0902:            /*@  public normal_behavior
0903:              @    requires othRel != null;
0904:              @    ensures \result.theRelation.equals(
0905:              @                    this.theRelation.intersection(othRel.theRelation));
0906:              @*/
0907:            public/*@ non_null @*/
0908:            JMLObjectToValueRelation intersection(
0909:                    /*@ non_null @*/JMLObjectToValueRelation othRel) {
0910:                JMLValueSet newImagePairSet = new JMLValueSet();
0911:                JMLObjectSet newDom = new JMLObjectSet();
0912:                int newSize = 0;
0913:
0914:                JMLObjectToValueRelationImageEnumerator imagePairEnum = this 
0915:                        .imagePairs();
0916:                JMLObjectValuePair imagePair;
0917:                JMLValueSet img;
0918:                while (imagePairEnum.hasMoreElements()) {
0919:                    imagePair = imagePairEnum.nextImagePair();
0920:                    img = (JMLValueSet) imagePair.value;
0921:                    img = img.intersection(othRel.elementImage(imagePair.key));
0922:                    if (!img.isEmpty()) {
0923:                        newImagePairSet = newImagePairSet
0924:                                .insert(new JMLObjectValuePair(imagePair.key,
0925:                                        img));
0926:                        newDom = newDom.insert(imagePair.key);
0927:                        newSize = newSize + img.int_size();
0928:                    }
0929:                }
0930:                return new JMLObjectToValueRelation(newImagePairSet, newDom,
0931:                        newSize);
0932:            }
0933:
0934:            /** Return a relation that is the difference between this and the given
0935:             * relation.  This is the difference between the sets of
0936:             * associations.
0937:             *  @see #difference
0938:             *  @see #intersection
0939:             */
0940:            /*@  public normal_behavior
0941:              @    requires othRel != null;
0942:              @    ensures \result.theRelation.equals(
0943:              @                    this.theRelation.difference(othRel.theRelation));
0944:              @*/
0945:            public/*@ non_null @*/
0946:            JMLObjectToValueRelation difference(
0947:                    /*@ non_null @*/JMLObjectToValueRelation othRel) {
0948:                JMLValueSet newImagePairSet = new JMLValueSet();
0949:                JMLObjectSet newDom = new JMLObjectSet();
0950:                int newSize = 0;
0951:
0952:                JMLObjectToValueRelationImageEnumerator imagePairEnum = this 
0953:                        .imagePairs();
0954:                JMLObjectValuePair imagePair;
0955:                JMLValueSet img;
0956:                while (imagePairEnum.hasMoreElements()) {
0957:                    imagePair = imagePairEnum.nextImagePair();
0958:                    img = (JMLValueSet) imagePair.value;
0959:                    img = img.difference(othRel.elementImage(imagePair.key));
0960:                    if (!img.isEmpty()) {
0961:                        newImagePairSet = newImagePairSet
0962:                                .insert(new JMLObjectValuePair(imagePair.key,
0963:                                        img));
0964:                        newDom = newDom.insert(imagePair.key);
0965:                        newSize = newSize + img.int_size();
0966:                    }
0967:                }
0968:                return new JMLObjectToValueRelation(newImagePairSet, newDom,
0969:                        newSize);
0970:            }
0971:
0972:            /** Return a relation that is like this relation except that its
0973:             * domain is limited to just the elements of the given set.
0974:             *  @see #restrictRangeTo
0975:             */
0976:            /*@  public normal_behavior
0977:              @    requires dom != null;
0978:              @    ensures (\forall JMLObjectValuePair pair; pair != null;
0979:              @                      \result.theRelation.has(pair) == dom.has(pair.key)
0980:              @                    && elementImage(pair.key).has(pair.value)
0981:              @                );
0982:              @*/
0983:            public/*@ non_null @*/
0984:            JMLObjectToValueRelation restrictDomainTo(
0985:                    /*@ non_null @*/JMLObjectSet dom) {
0986:                JMLValueSet newImagePairSet = new JMLValueSet();
0987:                JMLObjectSet newDom = domain_.intersection(dom);
0988:                int newSize = 0;
0989:
0990:                JMLObjectToValueRelationImageEnumerator imagePairEnum = this 
0991:                        .imagePairs();
0992:                JMLObjectValuePair imagePair;
0993:                JMLValueSet img;
0994:                while (imagePairEnum.hasMoreElements()) {
0995:                    imagePair = imagePairEnum.nextImagePair();
0996:                    if (newDom.has(imagePair.key)) {
0997:                        newImagePairSet = newImagePairSet.insert(imagePair);
0998:                        img = (JMLValueSet) imagePair.value;
0999:                        newSize = newSize + img.int_size();
1000:                    }
1001:                }
1002:                return new JMLObjectToValueRelation(newImagePairSet, newDom,
1003:                        newSize);
1004:            }
1005:
1006:            /** Return a relation that is like this relation except that its
1007:             * range is limited to just the elements of the given set.
1008:             *  @see #restrictDomainTo
1009:             */
1010:            /*@  public normal_behavior
1011:              @    requires rng != null;
1012:              @    ensures (\forall JMLObjectValuePair pair; ;
1013:              @                       \result.theRelation.has(pair)
1014:              @                        == rng.has(pair.value) 
1015:              @                    && elementImage(pair.key).has(pair.value)
1016:              @                );
1017:              @*/
1018:            public/*@ non_null @*/
1019:            JMLObjectToValueRelation restrictRangeTo(
1020:                    /*@ non_null @*/JMLValueSet rng) {
1021:                JMLValueSet newImagePairSet = new JMLValueSet();
1022:                JMLObjectSet newDom = new JMLObjectSet();
1023:                int newSize = 0;
1024:
1025:                JMLObjectToValueRelationImageEnumerator imagePairEnum = this 
1026:                        .imagePairs();
1027:                JMLObjectValuePair imagePair;
1028:                JMLValueSet img;
1029:                while (imagePairEnum.hasMoreElements()) {
1030:                    imagePair = imagePairEnum.nextImagePair();
1031:                    img = ((JMLValueSet) imagePair.value).intersection(rng);
1032:                    if (!img.isEmpty()) {
1033:                        newImagePairSet = newImagePairSet
1034:                                .insert(new JMLObjectValuePair(imagePair.key,
1035:                                        img));
1036:                        newDom = newDom.insert(imagePair.key);
1037:                        newSize = newSize + img.int_size();
1038:                    }
1039:                }
1040:                return new JMLObjectToValueRelation(newImagePairSet, newDom,
1041:                        newSize);
1042:            }
1043:
1044:            /** Return a string representation of this object.
1045:             */
1046:            /*@ also
1047:              @  public normal_behavior
1048:              @    ensures \result.equals(theRelation.toString());
1049:              @*/
1050:            public String toString() {
1051:                return toSet().toString();
1052:            }
1053:
1054:            /** Return a enumerator for the set of associations that
1055:             * conceptually make up this relation.
1056:             *  @see #elements()
1057:             *  @see #iterator()
1058:             *  @see #toSet()
1059:             *  @see #imagePairs()
1060:             */
1061:            /*@  public normal_behavior
1062:              @    ensures \result != null &&
1063:              @      \result.equals(new JMLObjectToValueRelationEnumerator(this));
1064:              @*/
1065:            public/*@ non_null @*/
1066:            JMLObjectToValueRelationEnumerator associations() {
1067:                return new JMLObjectToValueRelationEnumerator(this );
1068:            }
1069:
1070:            /** Return a enumerator for the set of associations that
1071:             * conceptually make up this relation.  This is a synonym for associations.
1072:             *  @see #associations()
1073:             *  @see #iterator()
1074:             */
1075:            /*@  public normal_behavior
1076:              @    ensures \result != null &&
1077:              @      \result.equals(associations());
1078:              @*/
1079:            public/*@ non_null @*/
1080:            JMLObjectToValueRelationEnumerator elements() {
1081:                return associations();
1082:            }
1083:
1084:            /** Returns an Iterator over the set of pairs conceptually
1085:             *  contained in this relation..
1086:             *  @see #associations()
1087:             *  @see #elements()
1088:             */
1089:            /*@ also
1090:              @    public normal_behavior
1091:              @      ensures \fresh(\result)
1092:              @          && \result.equals(new JMLEnumerationToIterator(elements()));
1093:              @*/
1094:            public JMLIterator iterator() {
1095:                return new JMLEnumerationToIterator(elements());
1096:            }
1097:
1098:            /** Return the set of all associations in this relation.
1099:             *  @see #associations()
1100:             *  @see #toBag()
1101:             *  @see #toSequence()
1102:             */
1103:            /*@ public normal_behavior
1104:              @    ensures \result != null && \result.size == int_size()
1105:              @        && (\forall JMLType pv; \result.has(pv);
1106:              @                pv != null && pv instanceof JMLObjectValuePair
1107:              @             && this.isDefinedAt(((JMLObjectValuePair)pv).key)
1108:              @             && this.elementImage(((JMLObjectValuePair)pv).key)
1109:              @                    .has(((JMLObjectValuePair)pv).value));
1110:              @             
1111:              @*/
1112:            public/*@ non_null @*/JMLValueSet toSet() {
1113:                JMLObjectToValueRelationEnumerator pairEnum = this 
1114:                        .associations();
1115:                JMLValueSet ret = new JMLValueSet();
1116:                while (pairEnum.hasMoreElements()) {
1117:                    JMLObjectValuePair p = pairEnum.nextPair();
1118:                    ret = ret.insert(p);
1119:                }
1120:                return ret;
1121:            }
1122:
1123:            /** Return the bag of all associations in this relation.
1124:             *  @see #toSet()
1125:             *  @see #toSequence()
1126:             */
1127:            /*@ public normal_behavior
1128:              @    ensures \result != null && \result.equals(toSet().toBag());
1129:              @*/
1130:            public/*@ non_null @*/JMLValueBag toBag() {
1131:                JMLObjectToValueRelationEnumerator pairEnum = this 
1132:                        .associations();
1133:                JMLValueBag ret = new JMLValueBag();
1134:                while (pairEnum.hasMoreElements()) {
1135:                    JMLObjectValuePair p = pairEnum.nextPair();
1136:                    ret = ret.insert(p);
1137:                }
1138:                return ret;
1139:            }
1140:
1141:            /** Return a sequence containing all associations in this relation.
1142:             *  @see #toSet()
1143:             *  @see #toBag()
1144:             */
1145:            /*@ public normal_behavior
1146:              @    ensures \result != null
1147:              @         && (\forall JMLObjectValuePair p;; 
1148:              @                         \result.count(p) == 1 <==> this.has(p));
1149:              @*/
1150:            public/*@ non_null @*/JMLValueSequence toSequence() {
1151:                JMLObjectToValueRelationEnumerator pairEnum = this 
1152:                        .associations();
1153:                JMLValueSequence ret = new JMLValueSequence();
1154:                while (pairEnum.hasMoreElements()) {
1155:                    JMLObjectValuePair p = pairEnum.nextPair();
1156:                    ret = ret.insertFront(p);
1157:                }
1158:                return ret;
1159:            }
1160:
1161:            /** Return the set of image set pairs that make up this relation.
1162:             *  @see #imagePairs()
1163:             *  @see #toSet()
1164:             */
1165:            /*@ public normal_behavior
1166:              @    ensures \result != null && \result.int_size() == domain().int_size()
1167:              @        && (\forall Object dv; domain().has(dv);
1168:              @                \result.has(
1169:              @                    new JMLObjectValuePair(dv, elementImage(dv))));
1170:              @*/
1171:            public/*@ non_null @*/JMLValueSet imagePairSet() {
1172:                return imagePairSet_;
1173:            }
1174:
1175:            /** Return the set of domain image set pairs that make up this relation.
1176:             *  @see #imagePairSet()
1177:             *  @see #associations()
1178:             *  @see #toSet()
1179:             */
1180:            /*@ public normal_behavior
1181:              @    ensures \result != null
1182:              @        && \result.abstractValue().int_size() == domain().int_size()
1183:              @        && (\forall Object dv; domain().has(dv);
1184:              @                \result.abstractValue().has(
1185:              @                    new JMLObjectValuePair(dv, elementImage(dv))));
1186:              @*/
1187:            public/*@ non_null @*/
1188:            JMLObjectToValueRelationImageEnumerator imagePairs() {
1189:                return new JMLObjectToValueRelationImageEnumerator(this );
1190:            }
1191:
1192:            /** Return a enumerator for the set that is the domain of this
1193:             * relation.
1194:             * @see #domain()
1195:             * @see #rangeElements()
1196:             */
1197:            /*@  public normal_behavior
1198:              @    ensures \result.equals(domain().elements());
1199:              @*/
1200:            public/*@ non_null @*/JMLObjectSetEnumerator domainElements() {
1201:                return domain_.elements();
1202:            }
1203:
1204:            /** Return a enumerator for the set that is the range of this
1205:             * relation.  (This was formerly called "elements").
1206:             * @see #range()
1207:             * @see #domainElements()
1208:             */
1209:            /*@  public normal_behavior
1210:              @    ensures \result.equals(range().elements());
1211:              @*/
1212:            public/*@ non_null @*/JMLValueSetEnumerator rangeElements() {
1213:                return range().elements();
1214:            }
1215:
1216:            /** Return the number of associations in this relation.
1217:             */
1218:            /*@ also
1219:              @   public normal_behavior
1220:              @     ensures \result == theRelation.int_size();
1221:              @*/
1222:            public int int_size() {
1223:                return size_;
1224:            }
1225:
1226:            /** Return a map that is contained in this relation.  If this
1227:             * relation is a function, then this method can be seen as a type
1228:             * conversion which does not make a change to the abstract value.
1229:             * However, if this relation is not a function, then this method
1230:             * chooses a function contained in this relation from among the
1231:             * possibilities available.
1232:             * @see #isaFunction
1233:             * @see JMLObjectToValueMap
1234:             */
1235:            /*@  public normal_behavior
1236:              @    ensures (\forall Object dv; dv != null;
1237:              @             (this.isDefinedAt(dv) == \result.isDefinedAt(dv))
1238:              @             && \result.elementImage(dv).isSubset(this.elementImage(dv))
1239:              @             && \result.elementImage(dv).int_size() == 1);
1240:              @*/
1241:            public/*@ non_null @*/JMLObjectToValueMap toFunction() {
1242:                JMLObjectSet newDom = domain_;
1243:                int newSize = domain_.int_size();
1244:
1245:                JMLValueSet newImagePairSet = imagePairSet_;
1246:
1247:                if (newSize != size_) {
1248:                    // Have to restrict the result to be a function
1249:                    JMLObjectToValueRelationImageEnumerator imagePairEnum = this 
1250:                            .imagePairs();
1251:                    newImagePairSet = new JMLValueSet();
1252:                    JMLObjectValuePair imagePair;
1253:                    JMLValueSet img;
1254:                    while (imagePairEnum.hasMoreElements()) {
1255:                        imagePair = imagePairEnum.nextImagePair();
1256:                        img = (JMLValueSet) imagePair.value;
1257:                        Enumeration imgEnum = img.elements();
1258:                        Object o = imgEnum.nextElement();
1259:                        if (o == null) {
1260:                            img = new JMLValueSet(null);
1261:                        } else {
1262:                            JMLType rv = (JMLType) o;
1263:                            img = new JMLValueSet(rv);
1264:                        }
1265:                        newImagePairSet = newImagePairSet
1266:                                .insert(new JMLObjectValuePair(imagePair.key,
1267:                                        img));
1268:                    }
1269:                }
1270:                return new JMLObjectToValueMap(newImagePairSet, newDom, newSize);
1271:            }
1272:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.