Source Code Cross Referenced for JMLMap.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) 


001:        // @(#)$Id: JMLMap.java 1.2 Wed, 25 May 2005 14:55:29 +0200 engelc $
002:
003:        // Copyright (C) 1998, 1999, 2002 Iowa State University
004:
005:        // This file is part of JML
006:
007:        // JML is free software; you can redistribute it and/or modify
008:        // it under the terms of the GNU General Public License as published by
009:        // the Free Software Foundation; either version 2, or (at your option)
010:        // any later version.
011:
012:        // JML is distributed in the hope that it will be useful,
013:        // but WITHOUT ANY WARRANTY; without even the implied warranty of
014:        // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
015:        // GNU General Public License for more details.
016:
017:        // You should have received a copy of the GNU General Public License
018:        // along with JML; see the file COPYING.  If not, write to
019:        // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
020:
021:        package org.jmlspecs.models;
022:
023:        import java.util.Enumeration;
024:
025:        /** Maps (i.e., binary relations that are functional) from non-null
026:         *  elements of {@link _DomainType_} to non-null elements of {@link
027:         *  _RangeType_}.  The first type, <kbd>_DomainType_</kbd>, is called
028:         *  the domain type of the map; the second type,
029:         *  <kbd>_RangeType_</kbd>, is called the range type of the map.  A
030:         *  map can be seen as a set of pairs, of form <em>(dv, rv)</em>,
031:         *  consisting of an element of the domain type, <em>dv</em>, and an
032:         *  element of the range type, <em>rv</em>.  Alternatively, it can be
033:         *  seen as a function that maps each element of the domain to some of
034:         *  elements of the range type.
035:         *
036:         *  <p> This type is a subtype of {@link
037:         *  JML_Domain_To_Range_Relation}, and as such as can be treated as a
038:         *  binary relation or a set valued function also.  See the
039:         *  documentation for {@link JML_Domain_To_Range_Relation} and for the
040:         *  methods inherited from this supertype for more information.
041:         *
042:         *  <p> This type considers elements <kbd>val</kbd> and <kbd>dv</kbd>
043:         *  of the domain type, to be distinct just when
044:         *  <kbd>_val_not_equal_to_dv_</kbd>.  It considers elements of
045:         *  <kbd>r</kbd> and <kbd>rv</kbd> of the range type to be distinct
046:         *  just when <kbd>_r_not_equal_to_rv_</kbd>.  Cloning takes place for
047:         *  the domain or range elements if the corresponding domain or range
048:         *  type is {@link JMLType}.
049:         *
050:         * @version $Revision: 1.2 $
051:         * @author Gary T. Leavens
052:         * @author Clyde Ruby
053:         * @see JMLCollection
054:         * @see JMLType
055:         * @see JML_Domain_To_Range_Relation
056:         * @see JML_Domain_To_Range_RelationEnumerator
057:         * @see JML_Domain_To_Range_RelationImageEnumerator
058:         * @see JMLValueSet
059:         * @see JMLObjectSet
060:         * @see JMLObjectToObjectMap
061:         * @see JMLValueToObjectMap
062:         * @see JMLObjectToValueMap
063:         * @see JMLValueToValueMap
064:         * @see JML_Domain_To_Range_Relation#toFunction()
065:         */
066:        //-@ immutable
067:        public/*@ pure @*/
068:        class JML_Domain_To_Range_Map extends JML_Domain_To_Range_Relation {
069:
070:            /*@ public invariant isaFunction();
071:              @ public invariant_redundantly
072:              @        (\forall _DomainType_ dv; isDefinedAt(dv);
073:              @                                  elementImage(dv).int_size() == 1);
074:              @*/
075:
076:            /** Initialize this map to be the empty mapping.
077:             * @see #EMPTY
078:             */
079:            /*@  public normal_behavior
080:              @    assignable theRelation, owner, elementType, containsNull;
081:              @    ensures theRelation.equals(new JMLValueSet());
082:              @    ensures_redundantly theRelation.isEmpty();
083:              @*/
084:            public JML_Domain_To_Range_Map() {
085:                super ();
086:            }
087:
088:            /** Initialize this map to be a mapping that maps the given domain
089:             * element to the given range element.
090:             * @see #singletonMap(_DomainType_, _RangeType_)
091:             * @see #JML_Domain_To_Range_Map(JML_Domain__Range_Pair)
092:             */
093:            /*@  public normal_behavior
094:              @    requires dv != null && rv != null;
095:              @    assignable theRelation, owner, elementType, containsNull;
096:              @    ensures (theRelation.int_size() == 1) && elementImage(dv).has(rv);
097:              @    ensures_redundantly isDefinedAt(dv);
098:              @*/
099:            public JML_Domain_To_Range_Map(/*@ non_null @*/_DomainType_ dv,
100:            /*@ non_null @*/_RangeType_ rv) {
101:                super (dv, rv);
102:            }
103:
104:            /** Initialize this map to be a mapping that maps the key in the
105:             * given pair to the value in that pair.
106:             * @see #singletonMap(JML_Domain__Range_Pair)
107:             * @see #JML_Domain_To_Range_Map(_DomainType_, _RangeType_)
108:             */
109:            /*@  public normal_behavior
110:              @    requires pair != null;
111:              @    assignable theRelation, owner, elementType, containsNull;
112:              @    ensures (theRelation.int_size() == 1)
113:              @         && elementImage(pair.key).has(pair.value);
114:              @    ensures_redundantly isDefinedAt(pair.key);
115:              @*/
116:            public JML_Domain_To_Range_Map(/*@ non_null @*/
117:            JML_Domain__Range_Pair pair) {
118:                super (pair.key, pair.value);
119:            }
120:
121:            /** Initialize this map based on the representation values given.
122:             */
123:            /*@    requires ipset != null && dom != null && 0 <= sz;
124:              @    assignable theRelation, owner, elementType, containsNull;
125:              @    ensures imagePairSet_ == ipset && domain_ == dom && size_ == sz;
126:              @*/
127:            protected JML_Domain_To_Range_Map(JMLValueSet ipset,
128:                    JML_Domain_Set dom, int sz) {
129:                super (ipset, dom, sz);
130:            }
131:
132:            /** The empty JML_Domain_To_Range_Map.
133:             * @see #JML_Domain_To_Range_Map()
134:             */
135:            public static final/*@ non_null @*/JML_Domain_To_Range_Map EMPTY = new JML_Domain_To_Range_Map();
136:
137:            /** Return the singleton map containing the given association.
138:             * @see #JML_Domain_To_Range_Map(_DomainType_, _RangeType_)
139:             * @see #singletonMap(JML_Domain__Range_Pair)
140:             */
141:            /*@ public normal_behavior
142:              @    requires dv != null && rv != null;
143:              @    ensures \result != null
144:              @         && \result.equals(new JML_Domain_To_Range_Map(dv, rv));
145:              @*/
146:            public static/*@ pure @*//*@ non_null @*/
147:            JML_Domain_To_Range_Map singletonMap(
148:                    /*@ non_null @*/_DomainType_ dv,
149:                    /*@ non_null @*/_RangeType_ rv) {
150:                return new JML_Domain_To_Range_Map(dv, rv);
151:            }
152:
153:            /** Return the singleton map containing the association described
154:             * by the given pair.
155:             * @see #JML_Domain_To_Range_Map(JML_Domain__Range_Pair)
156:             * @see #singletonMap(_DomainType_, _RangeType_)
157:             */
158:            /*@ public normal_behavior
159:              @    requires pair != null;
160:              @    ensures \result != null
161:              @         && \result.equals(new JML_Domain_To_Range_Map(pair));
162:              @*/
163:            public static/*@ pure @*//*@ non_null @*/
164:            JML_Domain_To_Range_Map singletonMap(
165:                    /*@ non_null @*/JML_Domain__Range_Pair pair) {
166:                return new JML_Domain_To_Range_Map(pair);
167:            }
168:
169:            /** Tells whether this relation is a function.
170:             */
171:            /*@ also
172:              @    public normal_behavior
173:              @      ensures \result;
174:              @*/
175:            //@ pure
176:            public boolean isaFunction() {
177:                return true;
178:            }
179:
180:            /** Return the range element corresponding to dv, if there is one.
181:             *
182:             * @param dv the domain element for which an association is
183:             * sought (the key to the table).
184:             * @exception JMLNoSuchElementException when dv is not associated
185:             * to any range element by this.
186:             * @see JML_Domain_To_Range_Relation#isDefinedAt
187:             * @see JML_Domain_To_Range_Relation#elementImage
188:             * @see JML_Domain_To_Range_Relation#image
189:             */
190:            /*@  public normal_behavior
191:              @    requires isDefinedAt(dv);
192:              @    ensures elementImage(dv).has(\result);
193:              @ also
194:              @  public exceptional_behavior
195:              @    requires !isDefinedAt(dv);
196:              @    signals (JMLNoSuchElementException);
197:              @*/
198:            public/*@ non_null @*/_RangeType_ apply(_DomainType_ dv)
199:                    throws JMLNoSuchElementException {
200:                JML_Range_Set img = elementImage(dv);
201:                if (img.int_size() == 1) {
202:                    _RangeType_ res = img.choose();
203:                    return res;
204:                } else {
205:                    throw new JMLNoSuchElementException("Map not defined at "
206:                            + dv);
207:                }
208:            }
209:
210:            /*@ also
211:              @   public normal_behavior
212:              @     ensures \result instanceof JML_Domain_To_Range_Map
213:              @          && ((JML_Domain_To_Range_Map)\result)
214:              @                .theRelation.equals(this.theRelation);
215:              @*/
216:            //@ pure
217:            public Object clone() {
218:                return new JML_Domain_To_Range_Map(imagePairSet_, domain_,
219:                        size_);
220:            }
221:
222:            /** Return a new map that is like this but maps the given domain
223:             *  element to the given range element.  Any previously existing
224:             *  mapping for the domain element is removed first.
225:             * @see JML_Domain_To_Range_Relation#insert(_DomainType_, _RangeType_)
226:             */
227:            /*@  public normal_behavior
228:              @    requires dv != null && rv != null;
229:              @    requires !isDefinedAt(dv) ==> int_size() < Integer.MAX_VALUE;
230:              @    ensures \result.equals(this.removeDomainElement(dv).add(dv, rv));
231:              @*/
232:            public/*@ non_null @*/
233:            JML_Domain_To_Range_Map extend(/*@ non_null @*/_DomainType_ dv,
234:            /*@ non_null @*/_RangeType_ rv) {
235:                JML_Domain_To_Range_Map newMap = this .removeDomainElement(dv);
236:                newMap = newMap.disjointUnion(new JML_Domain_To_Range_Map(dv,
237:                        rv));
238:                return newMap;
239:            }
240:
241:            /** Return a new map that is like this but has no association for the
242:             *  given domain element.
243:             * @see JML_Domain_To_Range_Relation#removeFromDomain
244:             */
245:            /*@  public normal_behavior
246:              @    ensures \result.equals(removeFromDomain(dv).toFunction());
247:              @    ensures_redundantly !isDefinedAt(dv) ==> \result.equals(this);
248:              @*/
249:            public/*@ non_null @*/
250:            JML_Domain_To_Range_Map removeDomainElement(_DomainType_ dv) {
251:                return super .removeFromDomain(dv).toFunction();
252:            }
253:
254:            /** Return a new map that is the composition of this and the given
255:             *  map.  The composition is done in the usual order; that is, if
256:             *  the given map maps x to y and this maps y to z, then the
257:             *  result maps x to z.
258:             * @see #compose(JMLObjectTo_Domain_Map)
259:             */
260:            /*@  public normal_behavior
261:              @    requires othMap != null;
262:              @    ensures (\forall JMLValue_Range_Pair pair; ;
263:              @                 \result.theRelation.has(pair) 
264:              @                    == (\exists _DomainType_ val;
265:              @                            othMap.elementImage(pair.key).has(val);
266:              @                            this.elementImage(val).has(pair.value) 
267:              @                            )
268:              @                );
269:              @*/
270:            public/*@ non_null @*/
271:            JMLValueTo_Range_Map compose(
272:                    /*@ non_null @*/JMLValueTo_Domain_Map othMap) {
273:                return super .compose(othMap).toFunction();
274:            }
275:
276:            /** Return a new map that is the composition of this and the given
277:             *  map.  The composition is done in the usual order; that is, if
278:             *  the given map maps x to y and this maps y to z, then the
279:             *  result maps x to z.
280:             * @see #compose(JMLValueTo_Domain_Map)
281:             */
282:            /*@  public normal_behavior
283:              @    requires othMap != null;
284:              @    ensures (\forall JMLObject_Range_Pair pair; ;
285:              @                 \result.theRelation.has(pair) 
286:              @                    == (\exists _DomainType_ val;
287:              @                            othMap.elementImage(pair.key).has(val);
288:              @                            this.elementImage(val).has(pair.value) 
289:              @                            )
290:              @                );
291:              @*/
292:            public/*@ non_null @*/
293:            JMLObjectTo_Range_Map compose(
294:                    /*@ non_null @*/JMLObjectTo_Domain_Map othMap) {
295:                return super .compose(othMap).toFunction();
296:            }
297:
298:            /** Return a new map that only maps elements in the given domain
299:             * to the corresponding range elements in this map.
300:             * @see #rangeRestrictedTo
301:             * @see JML_Domain_To_Range_Relation#restrictDomainTo
302:             */
303:            /*@  public normal_behavior
304:              @    requires dom != null;
305:              @    ensures (\forall JML_Domain__Range_Pair pair; ; 
306:              @                 \result.theRelation.has(pair)
307:              @                    == 
308:              @                       dom.has(pair.key) 
309:              @                    && elementImage(pair.key).has(pair.value)
310:              @                );
311:              @*/
312:            public/*@ non_null @*/
313:            JML_Domain_To_Range_Map restrictedTo(
314:                    /*@ non_null @*/JML_Domain_Set dom) {
315:                return super .restrictDomainTo(dom).toFunction();
316:            }
317:
318:            /** Return a new map that is like this map but only contains
319:             *  associations that map to range elements in the given set.
320:             * @see #restrictedTo
321:             * @see JML_Domain_To_Range_Relation#restrictRangeTo
322:             */
323:            /*@  public normal_behavior
324:              @    requires rng != null;
325:              @    ensures (\forall JML_Domain__Range_Pair pair; ;
326:              @                 \result.theRelation.has(pair)
327:              @                    == 
328:              @                       rng.has(pair.value) 
329:              @                    && elementImage(pair.key).has(pair.value)
330:              @                );
331:              @*/
332:            public/*@ non_null @*/
333:            JML_Domain_To_Range_Map rangeRestrictedTo(
334:                    /*@ non_null @*/JML_Range_Set rng) {
335:                return super .restrictRangeTo(rng).toFunction();
336:            }
337:
338:            /** Return a new map that is like the union of the given map and
339:             *  this map, except that if both define a mapping for a given domain
340:             *  element, then only the mapping in the given map is retained.
341:             * @see #clashReplaceUnion
342:             * @see #disjointUnion
343:             * @see JML_Domain_To_Range_Relation#union
344:             */
345:            /*@  public normal_behavior
346:              @    requires othMap != null;
347:              @    requires int_size()
348:              @             <= Integer.MAX_VALUE - othMap.difference(this).int_size();
349:              @    ensures (\forall JML_Domain__Range_Pair pair; ;
350:              @                 \result.theRelation.has(pair)
351:              @                    == 
352:              @                       othMap.elementImage(pair.key).has(pair.value)
353:              @                    || (!othMap.isDefinedAt(pair.key)
354:              @                        && this.elementImage(pair.key).has(pair.value))
355:              @                );
356:              @*/
357:            public/*@ non_null @*/
358:            JML_Domain_To_Range_Map extendUnion(
359:                    /*@ non_null @*/JML_Domain_To_Range_Map othMap)
360:                    throws IllegalStateException {
361:                JML_Domain_To_Range_Map newMap = this .restrictedTo(this .domain_
362:                        .difference(othMap.domain_));
363:                if (newMap.size_ <= Integer.MAX_VALUE - othMap.size_) {
364:                    return new JML_Domain_To_Range_Map(newMap.imagePairSet_
365:                            .union(othMap.imagePairSet_), newMap.domain_
366:                            .union(othMap.domain_), newMap.size_ + othMap.size_);
367:                } else {
368:                    throw new IllegalStateException(TOO_BIG_TO_UNION);
369:                }
370:            }
371:
372:            /** Return a new map that is like the union of the given map and
373:             * this map, except that if both define a mapping for a given
374:             * domain element, then each of these clashes is replaced by a
375:             * mapping from the domain element in question to the given range
376:             * element.
377:             * @param othMap the other map.
378:             * @param errval the range element to use when clashes occur.
379:             * @see #extendUnion
380:             * @see #disjointUnion
381:             * @see JML_Domain_To_Range_Relation#union
382:             */
383:            /*@  public normal_behavior
384:              @    requires othMap != null && errval != null;
385:              @    requires int_size()
386:              @             <= Integer.MAX_VALUE - othMap.difference(this).int_size();
387:              @    ensures (\forall JML_Domain__Range_Pair pair; ; 
388:              @                 \result.theRelation.has(pair)
389:              @                    == 
390:              @                       (!othMap.isDefinedAt(pair.key)
391:              @                        && this.elementImage(pair.key).has(pair.value))
392:              @                    || (!this.isDefinedAt(pair.key)
393:              @                        && othMap.elementImage(pair.key)
394:              @                                 .has(pair.value))
395:              @                    || (this.isDefinedAt(pair.key)
396:              @                        && othMap.isDefinedAt(pair.key)
397:              @                        && pair.value _rangeEquals_ (errval))
398:              @                );
399:              @ implies_that
400:              @    requires othMap != null && errval != null;
401:              @*/
402:            public/*@ non_null @*/
403:            JML_Domain_To_Range_Map clashReplaceUnion(
404:                    JML_Domain_To_Range_Map othMap, _RangeType_ errval)
405:                    throws IllegalStateException {
406:                JML_Domain_Set overlap = this .domain_
407:                        .intersection(othMap.domain_);
408:                Enumeration overlapEnum = overlap.elements();
409:                othMap = othMap
410:                        .restrictedTo(othMap.domain_.difference(overlap));
411:                JML_Domain_To_Range_Map newMap = this .restrictedTo(this .domain_
412:                        .difference(overlap));
413:                JML_Domain_To_Range_Relation newRel;
414:                if (newMap.size_ <= Integer.MAX_VALUE - othMap.size_) {
415:                    newRel = new JML_Domain_To_Range_Relation(
416:                            newMap.imagePairSet_.union(othMap.imagePairSet_),
417:                            newMap.domain_.union(othMap.domain_), newMap.size_
418:                                    + othMap.size_);
419:                } else {
420:                    throw new IllegalStateException(TOO_BIG_TO_UNION);
421:                }
422:                _DomainType_ dv;
423:                while (overlapEnum.hasMoreElements()) {
424:                    Object oo = overlapEnum.nextElement();
425:                    dv = (_DomainType_) oo;
426:                    newRel = newRel.add(dv, errval);
427:                }
428:                return newRel.toFunction();
429:            }
430:
431:            /** Return a map that is the disjoint union of this and othMap.
432:             *  @param othMap the other mapping
433:             *  @exception JMLMapException the ranges of this and othMap have elements
434:             *  in common (i.e., when they interesect).
435:             * @see #extendUnion
436:             * @see #clashReplaceUnion
437:             * @see JML_Domain_To_Range_Relation#union
438:             */
439:            /*@  public normal_behavior
440:              @    requires othMap != null
441:              @          && this.domain().intersection(othMap.domain()).isEmpty();
442:              @    requires int_size() <= Integer.MAX_VALUE - othMap.int_size();
443:              @    ensures \result.equals(this.union(othMap));
444:              @ also
445:              @  public exceptional_behavior
446:              @    requires othMap != null
447:              @          && !this.domain().intersection(othMap.domain()).isEmpty();
448:              @    signals (JMLMapException);
449:              @*/
450:            public/*@ non_null @*/
451:            JML_Domain_To_Range_Map disjointUnion(
452:                    /*@ non_null @*/JML_Domain_To_Range_Map othMap)
453:                    throws JMLMapException, IllegalStateException {
454:                JML_Domain_Set overlappingDom = domain_
455:                        .intersection(othMap.domain_);
456:                if (overlappingDom.isEmpty()) {
457:                    if (this .size_ <= Integer.MAX_VALUE - othMap.size_) {
458:                        return new JML_Domain_To_Range_Map(this .imagePairSet_
459:                                .union(othMap.imagePairSet_), this .domain_
460:                                .union(othMap.domain_), this .size_
461:                                + othMap.size_);
462:                    } else {
463:                        throw new IllegalStateException(TOO_BIG_TO_UNION);
464:                    }
465:                } else {
466:                    throw new JMLMapException("Overlapping domains in "
467:                            + " disjointUnion operation", overlappingDom);
468:                }
469:            }
470:
471:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.