Source Code Cross Referenced for JMLValueToValueRelation.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: JMLValueToValueRelation.java 1.2 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 JMLType} to non-null elements of {@link
0027:         *  JMLType}.  The first type, <kbd>JMLType</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.equals(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.2 $
0046:         * @author Gary T. Leavens
0047:         * @author Clyde Ruby
0048:         * @see JMLCollection
0049:         * @see JMLType
0050:         * @see JMLValueToValueMap
0051:         * @see JMLValueToValueRelationEnumerator
0052:         * @see JMLValueToValueRelationImageEnumerator
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 JMLValueToValueRelation 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 JMLValueValuePair
0072:              @         && ((JMLValueValuePair)obj).key != null
0073:              @         && ((JMLValueValuePair)obj).value != null);
0074:              @ public invariant_redundantly
0075:              @      (* Every element of 'theRelation'is a JMLValueValuePair
0076:              @         whose key and value are not null *);
0077:              @*/
0078:
0079:            //@ public invariant elementType == \type(JMLValueValuePair);
0080:            //@ public invariant !containsNull;
0081:            /** The set of elements in the domain of this relation.
0082:             */
0083:            protected final/*@ non_null @*/JMLValueSet domain_;
0084:            //@                                             in theRelation;
0085:
0086:            /** The set representing the image pairs in the relation.  The
0087:             * elements of this set are JMLValueValuePairs, 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 JMLType dv; dv != null && domain_.has(dv);
0106:              @          imagePairSet_
0107:              @            .has(new JMLValueValuePair(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 JMLValueToValueRelation() {
0124:                domain_ = new JMLValueSet();
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(JMLType, JMLType)
0132:             * @see #JMLValueToValueRelation(JMLValueValuePair)
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 JMLValueToValueRelation(/*@ non_null @*/JMLType dv,
0142:            /*@ non_null @*/JMLType rv) {
0143:                size_ = 1;
0144:                domain_ = new JMLValueSet(dv);
0145:                JMLValueSet img = new JMLValueSet(rv);
0146:                imagePairSet_ = new JMLValueSet(new JMLValueValuePair(dv, img));
0147:            }
0148:
0149:            /** Initialize this to be a relation containing a single association
0150:             *  given by the pair.
0151:             * @see #singleton(JMLValueValuePair)
0152:             * @see #JMLValueToValueRelation(JMLType, 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 JMLValueToValueRelation(/*@ non_null @*/
0160:            JMLValueValuePair 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 JMLValueToValueRelation(
0177:                    /*@ non_null @*/JMLValueSet ipset,
0178:                    /*@ non_null @*/JMLValueSet dom, int sz) {
0179:                domain_ = dom;
0180:                imagePairSet_ = ipset;
0181:                size_ = sz;
0182:            }
0183:
0184:            //**************************** Static methods ****************************
0185:
0186:            /** The empty JMLValueToValueRelation.
0187:             * @see #JMLValueToValueRelation()
0188:             */
0189:            public static final/*@ non_null @*/JMLValueToValueRelation EMPTY = new JMLValueToValueRelation();
0190:
0191:            /** Return the singleton relation containing the given association.
0192:             * @see #singleton(JMLValueValuePair)
0193:             * @see #JMLValueToValueRelation(JMLType, JMLType)
0194:             */
0195:            /*@ public normal_behavior
0196:              @    requires dv != null && rv != null;
0197:              @    ensures \result != null
0198:              @         && \result.equals(new JMLValueToValueRelation(dv, rv));
0199:              @*/
0200:            public static/*@ pure @*//*@ non_null @*/
0201:            JMLValueToValueRelation singleton(/*@ non_null @*/JMLType dv,
0202:            /*@ non_null @*/JMLType rv) {
0203:                return new JMLValueToValueRelation(dv, rv);
0204:            }
0205:
0206:            /** Return the singleton relation containing the association
0207:             * described by the given pair.
0208:             * @see #singleton(JMLType, JMLType)
0209:             * @see #JMLValueToValueRelation(JMLValueValuePair)
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:            JMLValueToValueRelation singleton(
0218:                    /*@ non_null @*/JMLValueValuePair pair) {
0219:                return singleton(pair.key, pair.value);
0220:            }
0221:
0222:            //**************************** Observers **********************************
0223:
0224:            /** Tells whether this relation is a function.
0225:             * @see JMLValueToValueMap
0226:             */
0227:            /*@   public normal_behavior
0228:              @     ensures \result == (\forall JMLType 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 JMLValueToValueMap#apply
0239:             */
0240:            /*@  public normal_behavior
0241:              @    ensures (\forall JMLValueValuePair pair;
0242:              @                      theRelation.has(pair);
0243:              @                      pair.keyEquals(dv) ==> \result.has(pair.value));
0244:              @    ensures (\forall JMLType o; \result.has(o);
0245:              @                  (\exists JMLValueValuePair 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(JMLType dv) {
0255:                JMLValueToValueRelationImageEnumerator imagePairEnum = this 
0256:                        .imagePairs();
0257:                JMLValueValuePair 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 JMLValueToValueMap#apply
0273:             */
0274:            /*@  public normal_behavior
0275:              @    requires dom != null;
0276:              @    ensures (\forall JMLType o; \result.has(o)
0277:              @              <==> (\exists JMLValueValuePair pair;
0278:              @                      theRelation.has(pair);
0279:              @                      dom.has(pair.key) && pair.valueEquals(o)));
0280:              @    ensures_redundantly
0281:              @              (\forall JMLValueValuePair 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 @*/JMLValueSet dom) {
0290:                JMLValueSet img = new JMLValueSet();
0291:                JMLValueToValueRelationImageEnumerator imagePairEnum = this 
0292:                        .imagePairs();
0293:                JMLValueValuePair 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 JMLValueValuePair pair; ;
0313:              @                 \result.theRelation.has(pair) 
0314:              @                    == elementImage(pair.value).has(pair.key));
0315:              @*/
0316:            public/*@ non_null @*/JMLValueToValueRelation inverse() {
0317:                JMLValueToValueRelation invRel = new JMLValueToValueRelation();
0318:                JMLValueToValueRelationEnumerator assocEnum = this 
0319:                        .associations();
0320:                JMLValueValuePair 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:            JMLValueSet inverseElementImage(JMLType rv) {
0342:                JMLValueSet invImg = new JMLValueSet();
0343:                JMLValueToValueRelationImageEnumerator imagePairEnum = this 
0344:                        .imagePairs();
0345:                JMLValueValuePair 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:            JMLValueSet inverseImage(/*@ non_null @*/JMLValueSet rng) {
0372:                JMLValueSet invImg = new JMLValueSet();
0373:                JMLValueToValueRelationImageEnumerator imagePairEnum = this 
0374:                        .imagePairs();
0375:                JMLValueValuePair imagePair;
0376:                //@ loop_invariant !invImg.containsNull;
0377:                while (imagePairEnum.hasMoreElements()) {
0378:                    imagePair = imagePairEnum.nextImagePair();
0379:                    JMLValueSet img = (JMLValueSet) imagePair.value;
0380:                    if (!img.intersection(rng).isEmpty()) {
0381:                        invImg = invImg.insert(imagePair.key);
0382:                    }
0383:                }
0384:                return invImg;
0385:            }
0386:
0387:            /** Tells whether this relation associates any range element to the
0388:             * given domain element.
0389:             * @see #domain()
0390:             */
0391:            /*@  public normal_behavior
0392:              @     ensures \result == (elementImage(dv).int_size() > 0);
0393:              @     ensures_redundantly dv == null ==> !\result;
0394:              @*/
0395:            public boolean isDefinedAt(JMLType dv) {
0396:                return domain_.has(dv);
0397:            }
0398:
0399:            /** Tells whether this associates the given key to the given value.
0400:             * @see #isDefinedAt
0401:             * @see #has(JMLValueValuePair)
0402:             */
0403:            /*@  public normal_behavior
0404:              @     ensures \result <==> domain().has(dv) && elementImage(dv).has(rv);
0405:              @     ensures_redundantly dv == null || rv == null ==> !\result;
0406:              @*/
0407:            public/*@ pure @*/boolean has(JMLType dv, JMLType rv) {
0408:                return domain_.has(dv) && elementImage(dv).has(rv);
0409:            }
0410:
0411:            /** Tells whether this associates the given key to the given value.
0412:             * @see #isDefinedAt
0413:             * @see #has(JMLType, JMLType)
0414:             */
0415:            /*@  public normal_behavior
0416:              @     requires pair != null;
0417:              @     ensures \result <==> has(pair.key, pair.value);
0418:              @*/
0419:            public/*@ pure @*/boolean has(
0420:                    /*@ non_null @*/JMLValueValuePair pair) {
0421:                return has(pair.key, pair.value);
0422:            }
0423:
0424:            /** Tells whether this associates the given key to the given value.
0425:             * @see #isDefinedAt
0426:             * @see #has(JMLValueValuePair)
0427:             */
0428:            /*@ also
0429:              @    public normal_behavior
0430:              @      ensures \result <==>
0431:              @              obj != null
0432:              @           && obj instanceof JMLValueValuePair
0433:              @           && has((JMLValueValuePair) obj);
0434:              @*/
0435:            public/*@ pure @*/boolean has(Object obj) {
0436:                return obj != null && obj instanceof  JMLValueValuePair
0437:                        && has((JMLValueValuePair) obj);
0438:            }
0439:
0440:            /** Tells whether the relation is empty.
0441:             * @see #int_size()
0442:             */
0443:            /*@  public normal_behavior
0444:              @    ensures \result == (theRelation.int_size() == 0);
0445:              @*/
0446:            public boolean isEmpty() {
0447:                return size_ == 0;
0448:            }
0449:
0450:            /** Return a clone of this object.
0451:             */
0452:            /*@ also
0453:              @  public normal_behavior
0454:              @    ensures \result instanceof JMLValueToValueRelation
0455:              @         && ((JMLValueToValueRelation)\result)
0456:              @                    .theRelation.equals(this.theRelation);
0457:              @*/
0458:            public Object clone() {
0459:                return new JMLValueToValueRelation(imagePairSet_, domain_,
0460:                        size_);
0461:            }
0462:
0463:            /** Test whether this object's value is equal to the given argument.
0464:             */
0465:            /*@ also
0466:              @  public normal_behavior
0467:              @    requires obj != null && obj instanceof JMLValueToValueRelation;
0468:              @    ensures \result == 
0469:              @            this.theRelation.equals(
0470:              @                    ((JMLValueToValueRelation)obj).theRelation);
0471:              @ also 
0472:              @  public normal_behavior
0473:              @    requires obj == null
0474:              @          || !(obj instanceof JMLValueToValueRelation);
0475:              @    ensures !\result;
0476:              @*/
0477:            public boolean equals(Object obj) {
0478:                if (obj == null || !(obj instanceof  JMLValueToValueRelation)) {
0479:                    return false;
0480:                }
0481:
0482:                JMLValueToValueRelation rel = (JMLValueToValueRelation) obj;
0483:
0484:                if (size_ != rel.int_size()) {
0485:                    return false;
0486:                }
0487:
0488:                JMLValueToValueRelationImageEnumerator imagePairEnum = this 
0489:                        .imagePairs();
0490:                JMLValueValuePair imagePair;
0491:                JMLValueSet img;
0492:                while (imagePairEnum.hasMoreElements()) {
0493:                    imagePair = imagePairEnum.nextImagePair();
0494:                    img = (JMLValueSet) imagePair.value;
0495:                    if (!img.equals(rel.elementImage(imagePair.key))) {
0496:                        return false;
0497:                    }
0498:                }
0499:                return true;
0500:            }
0501:
0502:            /** Return a hash code for this object.
0503:             */
0504:            public int hashCode() {
0505:                return imagePairSet_.hashCode();
0506:            }
0507:
0508:            /** Returns a set containing the domain of this relation.
0509:             * @see #domainElements()
0510:             * @see #associations()
0511:             * @see #isDefinedAt
0512:             * @see #image
0513:             * @see #range()
0514:             * @see #inverse()
0515:             */
0516:            /*@  public normal_behavior
0517:              @    ensures (\forall JMLType dv; ;
0518:              @                 \result.has(dv) == isDefinedAt(dv));
0519:              @*/
0520:            public/*@ non_null @*/JMLValueSet domain() {
0521:                return domain_;
0522:            }
0523:
0524:            /** Returns a set containing the range of this relation.
0525:             * @see #rangeElements()
0526:             * @see #associations()
0527:             * @see #inverseElementImage
0528:             * @see #domain()
0529:             * @see #inverse()
0530:             */
0531:            /*@  public normal_behavior
0532:              @    ensures (\forall JMLType rv; ;
0533:              @                 \result.has(rv) 
0534:              @                    == (\exists JMLType dv; ;
0535:              @                            elementImage(dv).has(rv)) 
0536:              @                );
0537:              @*/
0538:            public/*@ non_null @*/JMLValueSet range() {
0539:                JMLValueSet rangeSet = new JMLValueSet();
0540:
0541:                JMLValueToValueRelationImageEnumerator imagePairEnum = this 
0542:                        .imagePairs();
0543:                JMLValueValuePair imagePair;
0544:                JMLValueSet img;
0545:                while (imagePairEnum.hasMoreElements()) {
0546:                    imagePair = imagePairEnum.nextImagePair();
0547:                    img = (JMLValueSet) imagePair.value;
0548:                    rangeSet = rangeSet.union(img);
0549:                }
0550:                return rangeSet;
0551:            }
0552:
0553:            private static final String TOO_BIG_TO_INSERT = "Cannot insert into a Relation with Integer.MAX_VALUE elements.";
0554:
0555:            /** Return a relation that is just like this relation, except that
0556:             *  it also associates the given domain element to the given range
0557:             *  element.
0558:             * @see #insert
0559:             */
0560:            /*@  public normal_behavior
0561:              @    requires dv != null && rv != null;
0562:              @    requires int_size() < Integer.MAX_VALUE || elementImage(dv).has(rv);
0563:              @    ensures \result.theRelation.equals(
0564:              @           this.theRelation.insert(new JMLValueValuePair(dv, rv)));
0565:              @*/
0566:            public/*@ pure @*//*@ non_null @*/
0567:            JMLValueToValueRelation add(/*@ non_null @*/JMLType dv,
0568:            /*@ non_null @*/JMLType rv) throws NullPointerException,
0569:                    IllegalStateException {
0570:                if (rv == null) {
0571:                    throw new NullPointerException();
0572:                }
0573:
0574:                JMLValueSet newImagePairSet;
0575:                JMLValueSet newDom;
0576:                int newSize;
0577:                JMLValueSet img;
0578:
0579:                if (!domain_.has(dv)) {
0580:                    if (size_ == Integer.MAX_VALUE) {
0581:                        throw new IllegalStateException(TOO_BIG_TO_INSERT);
0582:                    }
0583:                    newDom = domain_.insert(dv);
0584:                    newSize = size_ + 1;
0585:                    img = new JMLValueSet(rv);
0586:                    newImagePairSet = imagePairSet_
0587:                            .insert(new JMLValueValuePair(dv, img));
0588:                } else {
0589:                    newImagePairSet = new JMLValueSet();
0590:                    newDom = domain_;
0591:                    newSize = 0;
0592:
0593:                    JMLValueToValueRelationImageEnumerator imagePairEnum = this 
0594:                            .imagePairs();
0595:                    JMLValueValuePair imagePair;
0596:                    while (imagePairEnum.hasMoreElements()) {
0597:                        imagePair = imagePairEnum.nextImagePair();
0598:                        img = (JMLValueSet) imagePair.value;
0599:                        if (imagePair.keyEquals(dv)) {
0600:                            img = img.insert(rv);
0601:                        }
0602:                        int size_inc = img.int_size();
0603:                        if (newSize <= Integer.MAX_VALUE - size_inc) {
0604:                            newSize = newSize + size_inc;
0605:                        } else {
0606:                            throw new IllegalStateException(TOO_BIG_TO_INSERT);
0607:                        }
0608:                        newImagePairSet = newImagePairSet
0609:                                .insert(new JMLValueValuePair(imagePair.key,
0610:                                        img));
0611:                    }
0612:                }
0613:                return new JMLValueToValueRelation(newImagePairSet, newDom,
0614:                        newSize);
0615:            }
0616:
0617:            /** Return a relation that is just like this relation, except that
0618:             *  it also includes the association described by the given pair.
0619:             * @see #add
0620:             */
0621:            /*@  public normal_behavior
0622:              @    requires pair != null;
0623:              @    requires int_size() < Integer.MAX_VALUE
0624:              @             || elementImage(pair.key).has(pair.value);
0625:              @    ensures \result.theRelation.equals(this.theRelation.insert(pair));
0626:              @*/
0627:            public/*@ non_null @*/
0628:            JMLValueToValueRelation insert(/*@ non_null @*/
0629:            JMLValueValuePair pair) throws IllegalStateException {
0630:                return add(pair.key, pair.value);
0631:            }
0632:
0633:            /** Return a relation that is just like this relation, except that
0634:             *  it does not contain any association with the given domain element.
0635:             * @see #remove(JMLValueValuePair)
0636:             * @see #removeFromDomain
0637:             */
0638:            /*@  public normal_behavior
0639:              @    ensures \result != null
0640:              @         && (\forall JMLType val; domain().has(val);
0641:              @             (\forall JMLType r; r != null;
0642:              @                   (elementImage(val).has(r)
0643:              @                      <==> \result.theRelation
0644:              @                            .has(new JMLValueValuePair(val,r))
0645:              @                          && !val.equals(dv))));
0646:              @ implies_that
0647:              @   public normal_behavior
0648:              @    requires dv == null;
0649:              @    ensures \result != null && \result.equals(this);
0650:              @*/
0651:            public/*@ non_null @*/
0652:            JMLValueToValueRelation removeFromDomain(JMLType dv) {
0653:                if (!domain_.has(dv)) {
0654:                    return (this );
0655:                }
0656:
0657:                JMLValueSet newImagePairSet = new JMLValueSet();
0658:                JMLValueSet newDom = domain_.remove(dv);
0659:                int newSize = 0;
0660:
0661:                JMLValueToValueRelationImageEnumerator imagePairEnum = this 
0662:                        .imagePairs();
0663:                JMLValueValuePair imagePair;
0664:                while (imagePairEnum.hasMoreElements()) {
0665:                    imagePair = imagePairEnum.nextImagePair();
0666:                    if (!imagePair.keyEquals(dv)) {
0667:                        newImagePairSet = newImagePairSet.insert(imagePair);
0668:                        JMLValueSet img = (JMLValueSet) imagePair.value;
0669:                        newSize = newSize + img.int_size();
0670:                    }
0671:                }
0672:                return new JMLValueToValueRelation(newImagePairSet, newDom,
0673:                        newSize);
0674:            }
0675:
0676:            /** Return a relation that is just like this relation, except that
0677:             *  it does not contain the association, if any, between the given
0678:             *  domain and range elements.
0679:             * @see #removeFromDomain
0680:             * @see #remove(JMLType, JMLType)
0681:             * @see #remove(JMLValueValuePair)
0682:             */
0683:            /*@  public normal_behavior
0684:              @    requires dv != null && rv != null;
0685:              @    ensures \result.theRelation.equals(
0686:              @                theRelation.remove(new JMLValueValuePair(dv, rv)));
0687:              @   also
0688:              @    requires dv == null || rv == null;
0689:              @    ensures \result != null && \result.equals(this);
0690:              @*/
0691:            public/*@ non_null @*/
0692:            JMLValueToValueRelation remove(JMLType dv, JMLType rv) {
0693:                if (!domain_.has(dv)) {
0694:                    return (this );
0695:                }
0696:
0697:                JMLValueSet newImagePairSet = new JMLValueSet();
0698:                JMLValueSet newDom = domain_;
0699:                int newSize = 0;
0700:
0701:                JMLValueToValueRelationImageEnumerator imagePairEnum = this 
0702:                        .imagePairs();
0703:                JMLValueValuePair imagePair;
0704:                JMLValueSet img;
0705:                while (imagePairEnum.hasMoreElements()) {
0706:                    imagePair = imagePairEnum.nextImagePair();
0707:                    img = (JMLValueSet) imagePair.value;
0708:                    int imgSize = img.int_size();
0709:                    if (imagePair.keyEquals(dv)) {
0710:                        img = img.remove(rv);
0711:                        imgSize = img.int_size();
0712:                        if (imgSize > 0) {
0713:                            newImagePairSet = newImagePairSet
0714:                                    .insert(new JMLValueValuePair(dv, img));
0715:                            newSize = newSize + imgSize;
0716:                        } else {
0717:                            //@ assert imgSize == 0;
0718:                            newDom = newDom.remove(dv);
0719:                        }
0720:                    } else {
0721:                        newImagePairSet = newImagePairSet.insert(imagePair);
0722:                        newSize = newSize + imgSize;
0723:                    }
0724:                }
0725:                return new JMLValueToValueRelation(newImagePairSet, newDom,
0726:                        newSize);
0727:            }
0728:
0729:            /** Return a relation that is just like this relation, except that
0730:             *  it does not contain association described by the given pair.
0731:             * @see #remove(JMLType, JMLType)
0732:             * @see #removeFromDomain
0733:             */
0734:            /*@  public normal_behavior
0735:              @    requires pair != null;
0736:              @    ensures \result.theRelation.equals(this.theRelation.remove(pair));
0737:              @*/
0738:            public/*@ non_null @*/
0739:            JMLValueToValueRelation remove(/*@ non_null @*/
0740:            JMLValueValuePair pair) {
0741:                return remove(pair.key, pair.value);
0742:            }
0743:
0744:            /** Return a relation that is the composition of the given
0745:             *  relation and this relation.  The composition is done in the
0746:             *  "usual" order, so that if the given relation relates x to y,
0747:             *  and this relation relates y to z, then the result relates x to
0748:             *  z.
0749:             *  @see #compose(JMLObjectToValueRelation)
0750:             */
0751:            /*@  public normal_behavior
0752:              @    requires othRel != null;
0753:              @    ensures (\forall JMLValueValuePair pair; ;
0754:              @                 \result.theRelation.has(pair) 
0755:              @                    == (\exists JMLType val;
0756:              @                            othRel.elementImage(pair.key).has(val);
0757:              @                            this.elementImage(val).has(pair.value)
0758:              @                            )
0759:              @                );
0760:              @*/
0761:            public/*@ non_null @*/
0762:            JMLValueToValueRelation compose(
0763:                    /*@ non_null @*/JMLValueToValueRelation othRel) {
0764:                JMLValueSet newImagePairSet = new JMLValueSet();
0765:                JMLValueSet newDom = new JMLValueSet();
0766:                int newSize = 0;
0767:
0768:                JMLValueToValueRelationImageEnumerator imagePairEnum = othRel
0769:                        .imagePairs();
0770:                JMLValueValuePair imagePair;
0771:                JMLValueSet img1;
0772:                JMLValueSet img2;
0773:                int imgSize;
0774:                while (imagePairEnum.hasMoreElements()) {
0775:                    imagePair = imagePairEnum.nextImagePair();
0776:                    img1 = (JMLValueSet) imagePair.value;
0777:                    img2 = this .image(img1);
0778:                    imgSize = img2.int_size();
0779:                    if (imgSize > 0) {
0780:                        newImagePairSet = newImagePairSet
0781:                                .insert(new JMLValueValuePair(imagePair.key,
0782:                                        img2));
0783:                        newSize = newSize + imgSize;
0784:                        newDom = newDom.insert(imagePair.key);
0785:                    }
0786:                }
0787:                return new JMLValueToValueRelation(newImagePairSet, newDom,
0788:                        newSize);
0789:            }
0790:
0791:            /** Return a relation that is the composition of the given
0792:             *  relation and this relation.  The composition is done in the
0793:             *  "usual" order, so that if the given relation relates x to y,
0794:             *  and this relation relates y to z, then the result relates x to
0795:             *  z.
0796:             *  @see #compose(JMLValueToValueRelation)
0797:             */
0798:            /*@  public normal_behavior
0799:              @    requires othRel != null;
0800:              @    ensures (\forall JMLValueValuePair pair; ;
0801:              @                 \result.theRelation.has(pair) 
0802:              @                    == (\exists JMLType val;
0803:              @                            othRel.elementImage(pair.key).has(val);
0804:              @                            this.elementImage(val).has(pair.value)
0805:              @                            )
0806:              @                );
0807:              @*/
0808:            public/*@ non_null @*/
0809:            JMLObjectToValueRelation compose(
0810:                    /*@ non_null @*/JMLObjectToValueRelation othRel) {
0811:                JMLValueSet newImagePairSet = new JMLValueSet();
0812:                JMLObjectSet newDom = new JMLObjectSet();
0813:                int newSize = 0;
0814:
0815:                JMLObjectToValueRelationImageEnumerator imagePairEnum = othRel
0816:                        .imagePairs();
0817:                JMLObjectValuePair imagePair;
0818:                JMLValueSet img1;
0819:                JMLValueSet img2;
0820:                int imgSize;
0821:                while (imagePairEnum.hasMoreElements()) {
0822:                    imagePair = imagePairEnum.nextImagePair();
0823:                    img1 = (JMLValueSet) imagePair.value;
0824:                    img2 = this .image(img1);
0825:                    imgSize = img2.int_size();
0826:                    if (imgSize > 0) {
0827:                        newImagePairSet = newImagePairSet
0828:                                .insert(new JMLObjectValuePair(imagePair.key,
0829:                                        img2));
0830:                        newSize = newSize + imgSize;
0831:                        newDom = newDom.insert(imagePair.key);
0832:                    }
0833:                }
0834:                return new JMLObjectToValueRelation(newImagePairSet, newDom,
0835:                        newSize);
0836:            }
0837:
0838:            /** Return a relation that union of the this and the given relation.
0839:             *  This is the union of the sets of associations.
0840:             *  @see #difference
0841:             *  @see #intersection
0842:             */
0843:            /*@  public normal_behavior
0844:              @    requires othRel != null;
0845:              @    requires int_size()
0846:              @             < Integer.MAX_VALUE - othRel.difference(this).int_size();
0847:              @    ensures \result.theRelation.equals(
0848:              @                    this.theRelation.union(othRel.theRelation));
0849:              @*/
0850:            public/*@ non_null @*/
0851:            JMLValueToValueRelation union(
0852:                    /*@ non_null @*/JMLValueToValueRelation othRel)
0853:                    throws IllegalStateException {
0854:                JMLValueSet newImagePairSet = new JMLValueSet();
0855:                JMLValueSet newDom = domain_;
0856:                int newSize = 0;
0857:
0858:                JMLValueToValueRelationImageEnumerator imagePairEnum = this 
0859:                        .imagePairs();
0860:                JMLValueValuePair imagePair;
0861:                JMLValueSet img;
0862:                while (imagePairEnum.hasMoreElements()) {
0863:                    imagePair = imagePairEnum.nextImagePair();
0864:                    img = (JMLValueSet) imagePair.value;
0865:                    img = img.union(othRel.elementImage(imagePair.key));
0866:                    newImagePairSet = newImagePairSet
0867:                            .insert(new JMLValueValuePair(imagePair.key, img));
0868:                    int size_inc = img.int_size();
0869:                    if (newSize <= Integer.MAX_VALUE - size_inc) {
0870:                        newSize = newSize + size_inc;
0871:                    } else {
0872:                        throw new IllegalStateException(TOO_BIG_TO_UNION);
0873:                    }
0874:                }
0875:                JMLValueSet diffDom = othRel.domain().difference(this .domain_);
0876:                imagePairEnum = othRel.imagePairs();
0877:                while (imagePairEnum.hasMoreElements()) {
0878:                    imagePair = imagePairEnum.nextImagePair();
0879:                    if (diffDom.has(imagePair.key)) {
0880:                        newImagePairSet = newImagePairSet.insert(imagePair);
0881:                        newDom = newDom.insert(imagePair.key);
0882:                        img = (JMLValueSet) imagePair.value;
0883:                        int size_inc = img.int_size();
0884:                        if (newSize <= Integer.MAX_VALUE - size_inc) {
0885:                            newSize = newSize + size_inc;
0886:                        } else {
0887:                            throw new IllegalStateException(TOO_BIG_TO_UNION);
0888:                        }
0889:                    }
0890:                }
0891:                return new JMLValueToValueRelation(newImagePairSet, newDom,
0892:                        newSize);
0893:            }
0894:
0895:            protected static final String TOO_BIG_TO_UNION = "Cannot make a union with more than Integer.MAX_VALUE elements.";
0896:
0897:            /** Return a relation that is the intersection of this and the
0898:             *  given relation.  This is the intersection of the sets of
0899:             *  associations.
0900:             *  @see #difference
0901:             *  @see #union
0902:             */
0903:            /*@  public normal_behavior
0904:              @    requires othRel != null;
0905:              @    ensures \result.theRelation.equals(
0906:              @                    this.theRelation.intersection(othRel.theRelation));
0907:              @*/
0908:            public/*@ non_null @*/
0909:            JMLValueToValueRelation intersection(
0910:                    /*@ non_null @*/JMLValueToValueRelation othRel) {
0911:                JMLValueSet newImagePairSet = new JMLValueSet();
0912:                JMLValueSet newDom = new JMLValueSet();
0913:                int newSize = 0;
0914:
0915:                JMLValueToValueRelationImageEnumerator imagePairEnum = this 
0916:                        .imagePairs();
0917:                JMLValueValuePair imagePair;
0918:                JMLValueSet img;
0919:                while (imagePairEnum.hasMoreElements()) {
0920:                    imagePair = imagePairEnum.nextImagePair();
0921:                    img = (JMLValueSet) imagePair.value;
0922:                    img = img.intersection(othRel.elementImage(imagePair.key));
0923:                    if (!img.isEmpty()) {
0924:                        newImagePairSet = newImagePairSet
0925:                                .insert(new JMLValueValuePair(imagePair.key,
0926:                                        img));
0927:                        newDom = newDom.insert(imagePair.key);
0928:                        newSize = newSize + img.int_size();
0929:                    }
0930:                }
0931:                return new JMLValueToValueRelation(newImagePairSet, newDom,
0932:                        newSize);
0933:            }
0934:
0935:            /** Return a relation that is the difference between this and the given
0936:             * relation.  This is the difference between the sets of
0937:             * associations.
0938:             *  @see #difference
0939:             *  @see #intersection
0940:             */
0941:            /*@  public normal_behavior
0942:              @    requires othRel != null;
0943:              @    ensures \result.theRelation.equals(
0944:              @                    this.theRelation.difference(othRel.theRelation));
0945:              @*/
0946:            public/*@ non_null @*/
0947:            JMLValueToValueRelation difference(
0948:                    /*@ non_null @*/JMLValueToValueRelation othRel) {
0949:                JMLValueSet newImagePairSet = new JMLValueSet();
0950:                JMLValueSet newDom = new JMLValueSet();
0951:                int newSize = 0;
0952:
0953:                JMLValueToValueRelationImageEnumerator imagePairEnum = this 
0954:                        .imagePairs();
0955:                JMLValueValuePair imagePair;
0956:                JMLValueSet img;
0957:                while (imagePairEnum.hasMoreElements()) {
0958:                    imagePair = imagePairEnum.nextImagePair();
0959:                    img = (JMLValueSet) imagePair.value;
0960:                    img = img.difference(othRel.elementImage(imagePair.key));
0961:                    if (!img.isEmpty()) {
0962:                        newImagePairSet = newImagePairSet
0963:                                .insert(new JMLValueValuePair(imagePair.key,
0964:                                        img));
0965:                        newDom = newDom.insert(imagePair.key);
0966:                        newSize = newSize + img.int_size();
0967:                    }
0968:                }
0969:                return new JMLValueToValueRelation(newImagePairSet, newDom,
0970:                        newSize);
0971:            }
0972:
0973:            /** Return a relation that is like this relation except that its
0974:             * domain is limited to just the elements of the given set.
0975:             *  @see #restrictRangeTo
0976:             */
0977:            /*@  public normal_behavior
0978:              @    requires dom != null;
0979:              @    ensures (\forall JMLValueValuePair pair; pair != null;
0980:              @                      \result.theRelation.has(pair) == dom.has(pair.key)
0981:              @                    && elementImage(pair.key).has(pair.value)
0982:              @                );
0983:              @*/
0984:            public/*@ non_null @*/
0985:            JMLValueToValueRelation restrictDomainTo(
0986:                    /*@ non_null @*/JMLValueSet dom) {
0987:                JMLValueSet newImagePairSet = new JMLValueSet();
0988:                JMLValueSet newDom = domain_.intersection(dom);
0989:                int newSize = 0;
0990:
0991:                JMLValueToValueRelationImageEnumerator imagePairEnum = this 
0992:                        .imagePairs();
0993:                JMLValueValuePair imagePair;
0994:                JMLValueSet img;
0995:                while (imagePairEnum.hasMoreElements()) {
0996:                    imagePair = imagePairEnum.nextImagePair();
0997:                    if (newDom.has(imagePair.key)) {
0998:                        newImagePairSet = newImagePairSet.insert(imagePair);
0999:                        img = (JMLValueSet) imagePair.value;
1000:                        newSize = newSize + img.int_size();
1001:                    }
1002:                }
1003:                return new JMLValueToValueRelation(newImagePairSet, newDom,
1004:                        newSize);
1005:            }
1006:
1007:            /** Return a relation that is like this relation except that its
1008:             * range is limited to just the elements of the given set.
1009:             *  @see #restrictDomainTo
1010:             */
1011:            /*@  public normal_behavior
1012:              @    requires rng != null;
1013:              @    ensures (\forall JMLValueValuePair pair; ;
1014:              @                       \result.theRelation.has(pair)
1015:              @                        == rng.has(pair.value) 
1016:              @                    && elementImage(pair.key).has(pair.value)
1017:              @                );
1018:              @*/
1019:            public/*@ non_null @*/
1020:            JMLValueToValueRelation restrictRangeTo(
1021:                    /*@ non_null @*/JMLValueSet rng) {
1022:                JMLValueSet newImagePairSet = new JMLValueSet();
1023:                JMLValueSet newDom = new JMLValueSet();
1024:                int newSize = 0;
1025:
1026:                JMLValueToValueRelationImageEnumerator imagePairEnum = this 
1027:                        .imagePairs();
1028:                JMLValueValuePair imagePair;
1029:                JMLValueSet img;
1030:                while (imagePairEnum.hasMoreElements()) {
1031:                    imagePair = imagePairEnum.nextImagePair();
1032:                    img = ((JMLValueSet) imagePair.value).intersection(rng);
1033:                    if (!img.isEmpty()) {
1034:                        newImagePairSet = newImagePairSet
1035:                                .insert(new JMLValueValuePair(imagePair.key,
1036:                                        img));
1037:                        newDom = newDom.insert(imagePair.key);
1038:                        newSize = newSize + img.int_size();
1039:                    }
1040:                }
1041:                return new JMLValueToValueRelation(newImagePairSet, newDom,
1042:                        newSize);
1043:            }
1044:
1045:            /** Return a string representation of this object.
1046:             */
1047:            /*@ also
1048:              @  public normal_behavior
1049:              @    ensures \result.equals(theRelation.toString());
1050:              @*/
1051:            public String toString() {
1052:                return toSet().toString();
1053:            }
1054:
1055:            /** Return a enumerator for the set of associations that
1056:             * conceptually make up this relation.
1057:             *  @see #elements()
1058:             *  @see #iterator()
1059:             *  @see #toSet()
1060:             *  @see #imagePairs()
1061:             */
1062:            /*@  public normal_behavior
1063:              @    ensures \result != null &&
1064:              @      \result.equals(new JMLValueToValueRelationEnumerator(this));
1065:              @*/
1066:            public/*@ non_null @*/
1067:            JMLValueToValueRelationEnumerator associations() {
1068:                return new JMLValueToValueRelationEnumerator(this );
1069:            }
1070:
1071:            /** Return a enumerator for the set of associations that
1072:             * conceptually make up this relation.  This is a synonym for associations.
1073:             *  @see #associations()
1074:             *  @see #iterator()
1075:             */
1076:            /*@  public normal_behavior
1077:              @    ensures \result != null &&
1078:              @      \result.equals(associations());
1079:              @*/
1080:            public/*@ non_null @*/
1081:            JMLValueToValueRelationEnumerator elements() {
1082:                return associations();
1083:            }
1084:
1085:            /** Returns an Iterator over the set of pairs conceptually
1086:             *  contained in this relation..
1087:             *  @see #associations()
1088:             *  @see #elements()
1089:             */
1090:            /*@ also
1091:              @    public normal_behavior
1092:              @      ensures \fresh(\result)
1093:              @          && \result.equals(new JMLEnumerationToIterator(elements()));
1094:              @*/
1095:            public JMLIterator iterator() {
1096:                return new JMLEnumerationToIterator(elements());
1097:            }
1098:
1099:            /** Return the set of all associations in this relation.
1100:             *  @see #associations()
1101:             *  @see #toBag()
1102:             *  @see #toSequence()
1103:             */
1104:            /*@ public normal_behavior
1105:              @    ensures \result != null && \result.size == int_size()
1106:              @        && (\forall JMLType pv; \result.has(pv);
1107:              @                pv != null && pv instanceof JMLValueValuePair
1108:              @             && this.isDefinedAt(((JMLValueValuePair)pv).key)
1109:              @             && this.elementImage(((JMLValueValuePair)pv).key)
1110:              @                    .has(((JMLValueValuePair)pv).value));
1111:              @             
1112:              @*/
1113:            public/*@ non_null @*/JMLValueSet toSet() {
1114:                JMLValueToValueRelationEnumerator pairEnum = this 
1115:                        .associations();
1116:                JMLValueSet ret = new JMLValueSet();
1117:                while (pairEnum.hasMoreElements()) {
1118:                    JMLValueValuePair p = pairEnum.nextPair();
1119:                    ret = ret.insert(p);
1120:                }
1121:                return ret;
1122:            }
1123:
1124:            /** Return the bag of all associations in this relation.
1125:             *  @see #toSet()
1126:             *  @see #toSequence()
1127:             */
1128:            /*@ public normal_behavior
1129:              @    ensures \result != null && \result.equals(toSet().toBag());
1130:              @*/
1131:            public/*@ non_null @*/JMLValueBag toBag() {
1132:                JMLValueToValueRelationEnumerator pairEnum = this 
1133:                        .associations();
1134:                JMLValueBag ret = new JMLValueBag();
1135:                while (pairEnum.hasMoreElements()) {
1136:                    JMLValueValuePair p = pairEnum.nextPair();
1137:                    ret = ret.insert(p);
1138:                }
1139:                return ret;
1140:            }
1141:
1142:            /** Return a sequence containing all associations in this relation.
1143:             *  @see #toSet()
1144:             *  @see #toBag()
1145:             */
1146:            /*@ public normal_behavior
1147:              @    ensures \result != null
1148:              @         && (\forall JMLValueValuePair p;; 
1149:              @                         \result.count(p) == 1 <==> this.has(p));
1150:              @*/
1151:            public/*@ non_null @*/JMLValueSequence toSequence() {
1152:                JMLValueToValueRelationEnumerator pairEnum = this 
1153:                        .associations();
1154:                JMLValueSequence ret = new JMLValueSequence();
1155:                while (pairEnum.hasMoreElements()) {
1156:                    JMLValueValuePair p = pairEnum.nextPair();
1157:                    ret = ret.insertFront(p);
1158:                }
1159:                return ret;
1160:            }
1161:
1162:            /** Return the set of image set pairs that make up this relation.
1163:             *  @see #imagePairs()
1164:             *  @see #toSet()
1165:             */
1166:            /*@ public normal_behavior
1167:              @    ensures \result != null && \result.int_size() == domain().int_size()
1168:              @        && (\forall JMLType dv; domain().has(dv);
1169:              @                \result.has(
1170:              @                    new JMLValueValuePair(dv, elementImage(dv))));
1171:              @*/
1172:            public/*@ non_null @*/JMLValueSet imagePairSet() {
1173:                return imagePairSet_;
1174:            }
1175:
1176:            /** Return the set of domain image set pairs that make up this relation.
1177:             *  @see #imagePairSet()
1178:             *  @see #associations()
1179:             *  @see #toSet()
1180:             */
1181:            /*@ public normal_behavior
1182:              @    ensures \result != null
1183:              @        && \result.abstractValue().int_size() == domain().int_size()
1184:              @        && (\forall JMLType dv; domain().has(dv);
1185:              @                \result.abstractValue().has(
1186:              @                    new JMLValueValuePair(dv, elementImage(dv))));
1187:              @*/
1188:            public/*@ non_null @*/
1189:            JMLValueToValueRelationImageEnumerator imagePairs() {
1190:                return new JMLValueToValueRelationImageEnumerator(this );
1191:            }
1192:
1193:            /** Return a enumerator for the set that is the domain of this
1194:             * relation.
1195:             * @see #domain()
1196:             * @see #rangeElements()
1197:             */
1198:            /*@  public normal_behavior
1199:              @    ensures \result.equals(domain().elements());
1200:              @*/
1201:            public/*@ non_null @*/JMLValueSetEnumerator domainElements() {
1202:                return domain_.elements();
1203:            }
1204:
1205:            /** Return a enumerator for the set that is the range of this
1206:             * relation.  (This was formerly called "elements").
1207:             * @see #range()
1208:             * @see #domainElements()
1209:             */
1210:            /*@  public normal_behavior
1211:              @    ensures \result.equals(range().elements());
1212:              @*/
1213:            public/*@ non_null @*/JMLValueSetEnumerator rangeElements() {
1214:                return range().elements();
1215:            }
1216:
1217:            /** Return the number of associations in this relation.
1218:             */
1219:            /*@ also
1220:              @   public normal_behavior
1221:              @     ensures \result == theRelation.int_size();
1222:              @*/
1223:            public int int_size() {
1224:                return size_;
1225:            }
1226:
1227:            /** Return a map that is contained in this relation.  If this
1228:             * relation is a function, then this method can be seen as a type
1229:             * conversion which does not make a change to the abstract value.
1230:             * However, if this relation is not a function, then this method
1231:             * chooses a function contained in this relation from among the
1232:             * possibilities available.
1233:             * @see #isaFunction
1234:             * @see JMLValueToValueMap
1235:             */
1236:            /*@  public normal_behavior
1237:              @    ensures (\forall JMLType dv; dv != null;
1238:              @             (this.isDefinedAt(dv) == \result.isDefinedAt(dv))
1239:              @             && \result.elementImage(dv).isSubset(this.elementImage(dv))
1240:              @             && \result.elementImage(dv).int_size() == 1);
1241:              @*/
1242:            public/*@ non_null @*/JMLValueToValueMap toFunction() {
1243:                JMLValueSet newDom = domain_;
1244:                int newSize = domain_.int_size();
1245:
1246:                JMLValueSet newImagePairSet = imagePairSet_;
1247:
1248:                if (newSize != size_) {
1249:                    // Have to restrict the result to be a function
1250:                    JMLValueToValueRelationImageEnumerator imagePairEnum = this 
1251:                            .imagePairs();
1252:                    newImagePairSet = new JMLValueSet();
1253:                    JMLValueValuePair imagePair;
1254:                    JMLValueSet img;
1255:                    while (imagePairEnum.hasMoreElements()) {
1256:                        imagePair = imagePairEnum.nextImagePair();
1257:                        img = (JMLValueSet) imagePair.value;
1258:                        Enumeration imgEnum = img.elements();
1259:                        Object o = imgEnum.nextElement();
1260:                        if (o == null) {
1261:                            img = new JMLValueSet(null);
1262:                        } else {
1263:                            JMLType rv = (JMLType) o;
1264:                            img = new JMLValueSet(rv);
1265:                        }
1266:                        newImagePairSet = newImagePairSet
1267:                                .insert(new JMLValueValuePair(imagePair.key,
1268:                                        img));
1269:                    }
1270:                }
1271:                return new JMLValueToValueMap(newImagePairSet, newDom, newSize);
1272:            }
1273:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.