001: // @(#)$Id: JMLListValueNode.java 1.1.1.1 Mon, 09 May 2005 15:27:50 +0200 engelc $
002:
003: // Copyright (C) 1998, 1999 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: /** An implementation class used in various models. These are
024: * singly-linked list nodes containing values. The empty
025: * list is represented by null, which makes dealing with these lists
026: * tricky. Normal users should use {@link JMLValueSequence} instead of this
027: * type to avoid these difficulties.
028: *
029: * <p>
030: * This type uses ".equals" to compare elements. The cons method
031: * clones elements that are passed into the list.
032: *
033: * @version $Revision: 1.1.1.1 $
034: * @author Gary T. Leavens
035: * @author Albert L. Baker
036: * @see JMLValueSequence
037: * @see JMLValueBag
038: * @see JMLValueSet
039: */
040: //-@ immutable
041: /*@ pure spec_public @*/class JMLListValueNode implements JMLValueType {
042:
043: //*********************** equational theory ***********************
044:
045: /*@ public invariant (\forall JMLListValueNode l2;
046: @ (\forall JMLType e1, e2;
047: @ (\forall \bigint n;
048: @ equational_theory(this, l2, e1, e2, n) )));
049: @*/
050:
051: /** An `equational' specification of lists, for use in the invariant.
052: */
053: /*@ public normal_behavior
054: @ {|
055: @ // The following define itemAt and size. The behavior
056: @ // of the other methods is defined based by these two
057: @ // methods.
058: @
059: @ ensures \result <==>
060: @ (new JMLListValueNode(e1, null)).size() == 1;
061: @ also
062: @ ensures \result <==>
063: @ (ls != null)
064: @ ==> (new JMLListValueNode(e1, ls)).size() == 1 + ls.size();
065: @ also
066: @ ensures \result <==>
067: @ (ls != null)
068: @ ==> (ls.next == null) == (ls.size() == 1);
069: @ also
070: @ ensures \result <==>
071: @ ls != null && ls.next != null
072: @ ==> ls.size() == 1 + ls.next.size();
073: @ also
074: @ ensures \result <==>
075: @ (ls != null && ls.val != null)
076: @ ==> ls.val.equals(ls.head());
077: @ also
078: @ ensures \result <==>
079: @ (e1 != null)
080: @ ==> cons(e1, ls).head().equals(e1);
081: @ also
082: @ ensures \result <==>
083: @ (ls != null && ls.val != null)
084: @ ==> ls.itemAt(0).equals(ls.head());
085: @ also
086: @ ensures \result <==>
087: @ ls != null && 0 < n && n < ls.size()
088: @ ==> ls.itemAt(n).equals(ls.next.itemAt(n - 1));
089: @ |}
090: public pure model boolean equational_theory(
091: JMLListValueNode ls, JMLListValueNode ls2,
092: JMLType e1, JMLType e2, \bigint n);
093: @*/
094:
095: /** The data contained in this list node.
096: */
097: public final JMLType val;
098:
099: /** The next node in this list.
100: */
101: public final JMLListValueNode next;
102:
103: /** The type of the elements in this list. This type is an upper
104: * bound on the element's types. The type is computed
105: * pessimistically, so that the order of adding elements does not
106: * matter; that is, if any element in the list is null, then we
107: * use JMLType as the type of the list's elements.
108: */
109: //@ ghost public Object elementType;
110: //@ public constraint elementType == \old(elementType);
111: //@ public invariant elementType <: \type(JMLType);
112: //@ public invariant val != null ==> \typeof(val) <: elementType;
113: //@ public invariant val == null ==> \type(JMLType) == elementType;
114: /*@ public invariant_redundantly
115: @ containsNull ==> \type(JMLType) == elementType;
116: @*/
117: //@ public invariant next != null ==> next.elementType <: elementType;
118: /** Whether this list can contain null elements;
119: */
120: //@ ghost public boolean containsNull;
121: //@ public constraint containsNull == \old(containsNull);
122: //@ public invariant containsNull <==> has(null);
123: /*@ protected
124: @ invariant containsNull <==>
125: @ val == null || (next != null && next.containsNull);
126: @*/
127:
128: //@ public invariant owner == null;
129: //************************* Constructors ********************************
130: /** Initialize this list to have the given item as its first
131: * element followed by the given list.
132: * This does not do any cloning.
133: *
134: * @param item the value to place at the head of this list.
135: * @param nxt the _JMLListValueNode to make the tail of this list.
136: */
137: /*@ public normal_behavior
138: @ requires item != null;
139: @ assignable val, next, elementType, containsNull, owner;
140: @ ensures val.equals(item) && next == nxt
141: @ && \typeof(item) <: elementType
142: @ && (nxt != null ==> nxt.elementType <: elementType)
143: @ && (nxt == null ==> elementType == \typeof(item))
144: @ && containsNull == (nxt == null ? false : nxt.containsNull);
145: @ also
146: @ public normal_behavior
147: @ requires item == null;
148: @ assignable val, next, elementType, containsNull, owner;
149: @ ensures val == null && next == nxt
150: @ && elementType == \type(JMLType)
151: @ && containsNull;
152: @
153: @ implies_that
154: @ ensures val == item && next == nxt;
155: @ ensures item == null ==> containsNull;
156: @ ensures item != null && nxt != null
157: @ ==> containsNull == nxt.containsNull;
158: @*/
159: public JMLListValueNode(JMLType item, JMLListValueNode nxt) {
160: val = item;
161: next = nxt;
162: }
163:
164: /** Return a JMLListValueNode containing the given element
165: * followed by the given list.
166: *
167: * Note that cons() adds elements to the front of a list.
168: * It handles any necessary cloning for value lists and it handles
169: * inserting null elements.
170: *
171: * @param hd the value to place at the head of the result.
172: * @param tl the JMLListValueNode to make the tail of the result.
173: */
174: /*@ public normal_behavior
175: @ ensures \result.headEquals(hd) && \result.next == tl;
176: @ ensures \result.equals(new JMLListValueNode(hd, tl));
177: @
178: @ implies_that public normal_behavior
179: @ ensures \result != null
180: @ && \result.containsNull <==>
181: @ hd == null || (tl != null && tl.containsNull);
182: @*/
183: public static/*@ pure @*//*@ non_null @*/
184: JMLListValueNode cons(JMLType hd, JMLListValueNode tl) {
185: if (hd == null) {
186: JMLListValueNode ret = new JMLListValueNode(null, tl);
187: return ret;
188: } else {
189: Object h = hd.clone();
190: JMLListValueNode ret = new JMLListValueNode((JMLType) h, tl);
191: return ret;
192: }
193: }
194:
195: //**************************** Observers **********************************
196:
197: /** Return the first element in this list.
198: * Note that head() handles any cloning necessary for value lists.
199: */
200: /*@ public normal_behavior
201: @ requires val != null;
202: @ ensures \result != null && \result.equals(val);
203: @ also
204: @ public normal_behavior
205: @ requires val == null;
206: @ ensures \result == null;
207: @
208: @ implies_that
209: @ ensures \result != null ==> \typeof(\result) <: elementType;
210: @ ensures !containsNull ==> \result != null;
211: @*/
212: public JMLType head() {
213: JMLType ret = (val == null ? null : (JMLType) val.clone());
214: return ret;
215: }
216:
217: /** Tell if the head of the list is ".equals" to the given
218: * item.
219: * @see #has(JMLType)
220: */
221: /*@ public normal_behavior
222: @ requires val != null;
223: @ ensures \result == (val.equals(item));
224: @ also
225: @ public normal_behavior
226: @ requires val == null;
227: @ ensures \result == (item == null);
228: @*/
229: public boolean headEquals(JMLType item) {
230: return elem_equals(val, item);
231: }
232:
233: /** Tell if the given elements are equal, taking null into account.
234: */
235: private static/*@ pure @*/boolean elem_equals(JMLType item1,
236: JMLType item2) {
237: return (item1 != null && item1.equals(item2))
238: || (item1 == null && item2 == null);
239: }
240:
241: /*@ public normal_behavior
242: @ requires 0 <= i && i < length();
243: @ ensures \result != null ==>
244: @ (* \result ".equals" the ith element of this *);
245: @ also
246: @ public exceptional_behavior
247: @ requires !(0 <= i && i < length());
248: @ signals (JMLListException);
249: @
250: model public JMLType itemAt(\bigint i) throws JMLListException;
251: @*/
252:
253: /** Return the ith element of a list.
254: * @see #getItem(int)
255: */
256: /*@ public normal_behavior
257: @ requires 0 <= i && i < int_length();
258: @ ensures \result != null ==>
259: @ (* \result ".equals" the ith element of this *);
260: @ also
261: @ public exceptional_behavior
262: @ requires !(0 <= i && i < int_length());
263: @ signals (JMLListException);
264: @
265: @ implies_that
266: @ ensures \result != null ==> \typeof(\result) <: elementType;
267: @ ensures !containsNull ==> \result != null;
268: @*/
269: public JMLType itemAt(int i) throws JMLListException {
270: if (i < 0) {
271: throw new JMLListException(
272: "Index to itemAt(int) is negative " + i);
273: } else {
274: int k = i;
275: //@ assert k >= 0;
276: JMLListValueNode ptr = this ;
277: //@ maintaining k >= 0;
278: //@ decreasing k;
279: while (ptr != null && k > 0) {
280: k--;
281: ptr = ptr.next;
282: }
283: if (ptr == null) {
284: throw new JMLListException(
285: "Index to itemAt(int) out of range.");
286: } else {
287: JMLType ret = (ptr.val == null ? null
288: : (JMLType) (ptr.val).clone());
289: return ret;
290: }
291: }
292: }
293:
294: /** Tells the number of elements in the sequence; a synonym for length
295: */
296: /*@ public normal_behavior
297: @ ensures (* \result is the number of JMLListValueNode(s) in this *);
298: @
299: @ public model pure \bigint size();
300: @*/
301:
302: /** Tells the number of elements in the sequence; a synonym for length
303: */
304: /*@ public normal_behavior
305: @ ensures \result == size();
306: @ public model pure \bigint length();
307: @*/
308:
309: /** Tells the number of elements in the list; a synonym for length.
310: */
311: /*@ public normal_behavior
312: @ ensures \result == size();
313: @
314: @ implies_that
315: @ ensures \result > 0;
316: @*/
317: public int int_size() {
318: int count = 0;
319: JMLListValueNode ptr = this ;
320: //@ maintaining (* ptr is count next's from this *);
321: while (ptr != null) {
322: ptr = ptr.next;
323: count++;
324: }
325: return count;
326: }
327:
328: /** Tells the number of elements in the list; a synonym for size.
329: */
330: /*@ public normal_behavior
331: @ ensures \result == length();
332: @
333: @ implies_that
334: @ ensures \result > 0;
335: @*/
336: public int int_length() {
337: return int_size();
338: }
339:
340: /** Tells whether the given element is ".equals" to an
341: * element in the list.
342: */
343: /*@ public normal_behavior
344: @ requires item != null;
345: @ ensures \result <==>
346: @ (\exists int i; 0 <= i && i < int_length();
347: @ (itemAt(i) == null
348: @ ? item == null
349: @ : itemAt(i).equals(item)));
350: @ also
351: @ public normal_behavior
352: @ requires item == null;
353: @ ensures \result <==>
354: @ (\exists int i; 0 <= i && i < int_length();
355: @ itemAt(i) == null);
356: @*/
357: public boolean has(JMLType item) {
358: JMLListValueNode ptr = this ;
359: //@ maintaining (* no earlier element is elem_equals to item *);
360: while (ptr != null) {
361: if (elem_equals(ptr.val, item)) {
362: return true;
363: }
364: ptr = ptr.next;
365: }
366: return false;
367: }
368:
369: /** Tells whether the elements of this list occur, in
370: * order, at the beginning of the given list, using ".equals" for
371: * comparisons.
372: */
373: /*@ public normal_behavior
374: @ requires ls2 != null;
375: @ ensures \result <==>
376: @ int_length() <= ls2.int_length()
377: @ && (\forall int i; 0 <= i && i < int_length();
378: @ (ls2.itemAt(i) == null && itemAt(i) == null)
379: @ || (ls2.itemAt(i) != null &&
380: @ ls2.itemAt(i).equals(itemAt(i))));
381: @ also
382: @ public normal_behavior
383: @ requires ls2 == null;
384: @ ensures !\result;
385: @*/
386: public boolean isPrefixOf(JMLListValueNode ls2) {
387: if (ls2 == null) {
388: return false;
389: }
390: JMLListValueNode othLst = ls2;
391: JMLListValueNode this Lst = this ;
392: /*@ maintaining
393: @ (* all earlier elements of both lists are elem_equals *);
394: @*/
395: while (this Lst != null && othLst != null) {
396: if (!elem_equals(this Lst.val, othLst.val)) {
397: return false;
398: }
399: this Lst = this Lst.next;
400: othLst = othLst.next;
401: }
402: return this Lst == null;
403: }
404:
405: /** Test whether this object's value is equal to the given argument.
406: */
407: /*@ also
408: @ public normal_behavior
409: @ requires ls2 != null && ls2 instanceof JMLListValueNode;
410: @ ensures \result <==> isPrefixOf((JMLListValueNode)ls2)
411: @ && ((JMLListValueNode)ls2).isPrefixOf(this);
412: @ also
413: @ public normal_behavior
414: @ requires ls2 == null || !(ls2 instanceof JMLListValueNode);
415: @ ensures \result <==> false;
416: @*/
417: public boolean equals(Object ls2) {
418: if (ls2 != null && ls2 instanceof JMLListValueNode) {
419: JMLListValueNode othLst = (JMLListValueNode) ls2;
420: JMLListValueNode this Lst = this ;
421: //@ maintaining (* all earlier elements of both lists are elem_equals *);
422: while (this Lst != null && othLst != null) {
423: if (!elem_equals(this Lst.val, othLst.val)) {
424: return false;
425: }
426: this Lst = this Lst.next;
427: othLst = othLst.next;
428: }
429: return (othLst == this Lst); // both must be null.
430: } else {
431: return false;
432: }
433: }
434:
435: /** Return a hash code for this object.
436: */
437: public int hashCode() {
438: int hash = 0;
439: JMLListValueNode ptr = this ;
440: while (ptr != null) {
441: Object v = ptr.val;
442: if (v != null) {
443: hash += v.hashCode();
444: }
445: ptr = ptr.next;
446: }
447: return hash;
448: }
449:
450: /*@ public normal_behavior
451: @ requires has(item) && item != null;
452: @ ensures itemAt(\result).equals(item)
453: @ && (\forall \bigint i; 0 <= i && i < \result;
454: @ !(itemAt(i) != null
455: @ && itemAt(i).equals(item)));
456: @ also
457: @ public normal_behavior
458: @ requires has(item) && item == null;
459: @ ensures itemAt(\result) == null
460: @ && (\forall \bigint i; 0 <= i && i < \result;
461: @ itemAt(i) != null);
462: @ also
463: @ public normal_behavior
464: @ requires !has(item);
465: @ ensures \result == -1;
466: @
467: model public \bigint bi_indexOf(JMLType item);
468: @*/
469:
470: /*@ public normal_behavior
471: @ requires has(item) && item != null;
472: @ ensures itemAt(\result).equals(item)
473: @ && (\forall int i; 0 <= i && i < \result;
474: @ !(itemAt(i) != null
475: @ && itemAt(i).equals(item)));
476: @ also
477: @ public normal_behavior
478: @ requires has(item) && item == null;
479: @ ensures itemAt(\result) == null
480: @ && (\forall int i; 0 <= i && i < \result;
481: @ itemAt(i) != null);
482: @ also
483: @ public normal_behavior
484: @ requires !has(item);
485: @ ensures \result == -1;
486: @
487: @ implies_that
488: @ ensures \result >= -1;
489: @*/
490: public int indexOf(JMLType item) {
491: int idx = 0;
492: JMLListValueNode ptr = this ;
493: while (ptr != null) {
494: if (elem_equals(ptr.val, item)) {
495: return idx;
496: }
497: ptr = ptr.next;
498: idx++;
499: }
500: return -1;
501: }
502:
503: /*@ public normal_behavior
504: @ ensures (\result == null && itemAt((int)(int_length()-1)) == null)
505: @ || \result.equals(itemAt((int)(int_length()-1)));
506: @
507: @ implies_that
508: @ ensures \result != null ==> \typeof(\result) <: elementType;
509: @ ensures !containsNull ==> \result != null;
510: @*/
511: public JMLType last() {
512: if (next == null) {
513: return head();
514: } else {
515: JMLListValueNode ptr = this ;
516: //@ maintaining ptr != null;
517: while (ptr.next != null) {
518: ptr = ptr.next;
519: }
520: JMLType ret = (ptr.val == null ? null : (JMLType) (ptr.val)
521: .clone());
522: return ret;
523: }
524: }
525:
526: /*@ public normal_behavior
527: @ requires has(item);
528: @ {|
529: @ requires item != null;
530: @ ensures \result.equals(itemAt(indexOf(item)));
531: @ also
532: @ requires item == null;
533: @ ensures \result == null;
534: @ |}
535: @ also
536: @ public exceptional_behavior
537: @ requires !has(item);
538: @ signals (JMLListException);
539: @*/
540: public JMLType getItem(JMLType item) throws JMLListException {
541: JMLListValueNode ptr = this ;
542: //@ maintaining (* no earlier element is elem_equals to item *);
543: while (ptr != null) {
544: if (elem_equals(ptr.val, item)) {
545: return ptr.val;
546: }
547: ptr = ptr.next;
548: }
549: throw new JMLListException("No matching item in list.");
550: }
551:
552: // ******************** building new JMLValueLists ***********************
553:
554: /** Return a clone of this object.
555: */
556: /*@ also
557: @ public normal_behavior
558: @ ensures \result != null && \result instanceof JMLListValueNode
559: @ && ((JMLListValueNode)\result).equals(this);
560: @*/
561: public Object clone() {
562: // Recall that cons() handles cloning.
563: JMLListValueNode ret = cons(val, (next == null ? null
564: : (JMLListValueNode) next.clone()));
565: return ret;
566: }
567:
568: /*@ public normal_behavior
569: @ {|
570: @ requires 0 < n && n <= length();
571: @ ensures \result != null
572: @ && \result.length() == n
573: @ && (\forall \bigint i; 0 <= i && i < n;
574: @ \result.itemAt(i) == itemAt(i));
575: @ also
576: @ requires n <= 0;
577: @ ensures \result == null;
578: @ also
579: @ requires length() < n;
580: @ ensures this.equals(\result);
581: @ |}
582: model public JMLListValueNode prefix(\bigint n);
583: @*/
584:
585: /** Return a list containing the first n elements in this list.
586: * @param n the number of elements to leave in the result.
587: * @return null if n is not positive or greater than the length of this list.
588: */
589: /*@ public normal_behavior
590: @ {|
591: @ requires 0 < n && n <= int_length();
592: @ ensures \result != null
593: @ && \result.int_length() == n
594: @ && (\forall int i; 0 <= i && i < n;
595: @ \result.itemAt(i) == itemAt(i));
596: @ also
597: @ requires n <= 0;
598: @ ensures \result == null;
599: @ also
600: @ requires int_length() < n;
601: @ ensures this.equals(\result);
602: @ |}
603: @ implies_that
604: @ ensures !containsNull && \result != null ==> !\result.containsNull;
605: @*/
606: public JMLListValueNode prefix(int n) {
607: return (n <= 0 ? null : new JMLListValueNode(val,
608: (next == null ? null : next.prefix(n - 1))));
609: }
610:
611: /*@ public normal_behavior
612: @ {|
613: @ requires 0 < n && n < length();
614: @ ensures \result != null
615: @ && \result.length() == length() - n
616: @ && (\forall \bigint i; n <= i && i < length();
617: @ \result.itemAt(i-n) == itemAt(i));
618: @ also
619: @ requires n <= 0;
620: @ ensures this.equals(\result);
621: @ also
622: @ requires length() <= n;
623: @ ensures \result == null;
624: @ |}
625: model public JMLListValueNode removePrefix(\bigint n);
626: @*/
627:
628: /*@ public normal_behavior
629: @ {|
630: @ requires 0 < n && n < int_length();
631: @ ensures \result != null
632: @ && \result.int_length() == int_length() - n
633: @ && (\forall int i; n <= i && i < int_length();
634: @ \result.itemAt((int)(i-n)) == itemAt(i));
635: @ also
636: @ requires n <= 0;
637: @ ensures this.equals(\result);
638: @ also
639: @ requires int_length() <= n;
640: @ ensures \result == null;
641: @ |}
642: @*/
643: public JMLListValueNode removePrefix(int n) {
644: return (n <= 0 ? this : (next == null ? null : next
645: .removePrefix(n - 1)));
646: }
647:
648: /*@ public normal_behavior
649: @ requires n == 0 && length() == 1;
650: @ ensures \result == null;
651: @ also
652: @ public normal_behavior
653: @ requires n == 0 && length() > 1;
654: @ ensures \result.equals(removePrefix(1));
655: @ also
656: @ public normal_behavior
657: @ requires 0 < n && n < length();
658: @ ensures \result != null
659: @ && \result.length() == length() - 1
660: @ && \result.equals(prefix(n).concat(removePrefix(n+1)));
661: @ // !FIXME! This spec is inconsistent. Take n == length() - 1.
662: @ // then removePrefix(n+1) --> removePrefix(length()) --> null.
663: @ // But concat requires non_null. Maybe spec of concat should be relaxed?
664: model public JMLListValueNode removeItemAt(\bigint n);
665: @*/
666:
667: /*@ public normal_behavior
668: @ requires n == 0 && int_length() == 1;
669: @ ensures \result == null;
670: @ also
671: @ public normal_behavior
672: @ requires n == 0 && int_length() > 1;
673: @ ensures \result.equals(removePrefix(1));
674: @ also
675: @ public normal_behavior
676: @ requires 0 < n && n < int_length();
677: @ ensures \result != null
678: @ && \result.int_length() == int_length() - 1
679: @ && \result.equals(prefix(n).concat(removePrefix((int)(n+1))));
680: @ // !FIXME! This spec is inconsistent. Take n == int_length() - 1.
681: @ // then removePrefix((int)(n+1)) --> removePrefix(int_length()) --> null.
682: @ // But concat requires non_null. Maybe spec of concat should be relaxed?
683: @*/
684: public JMLListValueNode removeItemAt(int n) {
685: return (n <= 0 ? next : (next == null ? null
686: : new JMLListValueNode(val, next.removeItemAt(n - 1))));
687: }
688:
689: /*@ public normal_behavior
690: @ requires 0 <= n && n < length();
691: @ ensures \result != null && \result.length() == length();
692: @ also
693: @ public normal_behavior
694: @ requires n == 0 && length() == 1;
695: @ ensures \result != null
696: @ && \result.equals(cons(item, next));
697: @ also
698: @ public normal_behavior
699: @ requires n == 0 && length() > 1;
700: @ ensures \result != null
701: @ && \result.equals(removePrefix(1).prepend(item));
702: @ also
703: @ public normal_behavior
704: @ requires 0 < n && n == length()-1;
705: @ ensures \result != null
706: @ && \result.equals(prefix(n).append(item));
707: @ also
708: @ public normal_behavior
709: @ requires 0 < n && n < length()-1;
710: @ ensures \result != null && \result.length() == length()
711: @ && \result.equals(prefix(n)
712: @ .concat(removePrefix(n+1).prepend(item)));
713: model public JMLListValueNode replaceItemAt(\bigint n, JMLType item) {
714: return (n <= 0
715: ? cons(item, next) // cons() handles any necessary cloning
716: : (next == null ? null
717: : new JMLListValueNode(val,
718: next.replaceItemAt(n-1, item)))
719: );
720: }
721: @*/
722:
723: /** Return a list like this, but with item replacing the element at the
724: * given zero-based index.
725: * @param n the zero-based index into this list.
726: * @param item the item to put at index index
727: */
728: /*@ public normal_behavior
729: @ requires 0 <= n && n < int_length();
730: @ ensures \result != null && \result.int_length() == int_length();
731: @ also
732: @ public normal_behavior
733: @ requires n == 0 && int_length() == 1;
734: @ ensures \result != null
735: @ && \result.equals(cons(item, next));
736: @ also
737: @ public normal_behavior
738: @ requires n == 0 && int_length() > 1;
739: @ ensures \result != null
740: @ && \result.equals(removePrefix(1).prepend(item));
741: @ also
742: @ public normal_behavior
743: @ requires 0 < n && n == int_length()-1;
744: @ ensures \result != null
745: @ && \result.equals(prefix(n).append(item));
746: @ also
747: @ public normal_behavior
748: @ requires 0 < n && n < int_length()-1;
749: @ ensures \result != null && \result.int_length() == int_length()
750: @ && \result.equals(prefix(n)
751: @ .concat(removePrefix(n+1).prepend(item)));
752: @*/
753: public JMLListValueNode replaceItemAt(int n, JMLType item) {
754: return (n <= 0 ? cons(item, next) // cons() handles any necessary cloning
755: : (next == null ? null : new JMLListValueNode(val, next
756: .replaceItemAt(n - 1, item))));
757: }
758:
759: /*@ public normal_behavior // !FIXME! inconsistent spec [when int_length() == 1]
760: @ ensures \result == null ==> int_length() == 1;
761: @ ensures \result != null ==> \result.equals(prefix((int)(int_length() - 1)));
762: @*/
763: public JMLListValueNode removeLast() {
764: return (next == null ? null : new JMLListValueNode(val, next
765: .removeLast()));
766: }
767:
768: /** Return a list that is the concatenation of this with the given
769: * lists.
770: * @param ls2 the list to place at the end of this list in the
771: * result.
772: * @return the concatenation of this list and ls2.
773: */
774: /*@ public normal_behavior
775: @ requires ls2 != null;
776: @ ensures \result != null
777: @ && \result.int_length() == int_length() + ls2.int_length()
778: @ && (\forall int i; 0 <= i && i < int_length();
779: @ \result.itemAt(i) == itemAt(i))
780: @ && (\forall int i; 0 <= i && i < ls2.int_length();
781: @ \result.itemAt((int)(int_length()+i)) == ls2.itemAt(i));
782: @*/
783: public/*@ non_null @*/
784: JMLListValueNode concat(/*@ non_null @*/JMLListValueNode ls2) {
785: return (next == null ? new JMLListValueNode(val, ls2)
786: : new JMLListValueNode(val, next.concat(ls2)));
787: }
788:
789: /** Return a list that is like this, but with the given item at
790: * the front. Note that this clones the item if necessary.
791: * @param item the element to place at the front of the result.
792: */
793: /*@ public normal_behavior
794: @ ensures \result != null && \result.equals(cons(item, this));
795: @ ensures_redundantly \result != null
796: @ && \result.int_length() == int_length() + 1;
797: @*/
798: public/*@ non_null @*/JMLListValueNode prepend(JMLType item) {
799: // cons() handles any necessary cloning
800: return cons(item, this );
801: }
802:
803: /** Return a list that consists of this list and the given element.
804: */
805: /*@ public normal_behavior
806: @ ensures \result != null
807: @ && \result.equals(cons(item, this.reverse()).reverse());
808: @ ensures_redundantly \result != null
809: @ && \result.int_length() == int_length() + 1;
810: @*/
811: public/*@ non_null @*/JMLListValueNode append(JMLType item) {
812: // To avoid full recursion, we build the reverse of what we want in
813: // revret, then reverse it. To make sure we only clone once,
814: // we let reverse do the cloning
815: JMLListValueNode ptr = this ;
816: JMLListValueNode revret = null;
817: //@ maintaining (* reverse(revret) concatenated with ptr equals this *);
818: while (ptr != null) {
819: revret = new JMLListValueNode(ptr.val, revret); // don't clone yet
820: ptr = ptr.next;
821: }
822: return (new JMLListValueNode(item, revret)).reverse();
823: }
824:
825: /** Return a list that is the reverse of this list.
826: */
827: /*@ public normal_behavior
828: @ ensures \result.int_length() == int_length()
829: @ && (\forall int i; 0 <= i && i < int_length();
830: @ (\result.itemAt((int)(int_length()-i-1)) != null
831: @ && \result.itemAt((int)(int_length()-i-1)).equals(itemAt(i)))
832: @ || (\result.itemAt((int)(int_length()-i-1)) == null
833: @ && itemAt(i) == null) );
834: @ ensures_redundantly
835: @ (* \result has the same elements but with the items
836: @ arranged in the reverse order *);
837: @
838: @ implies_that
839: @ ensures elementType == \result.elementType;
840: @ ensures containsNull <==> \result.containsNull;
841: @*/
842: public/*@ non_null @*/JMLListValueNode reverse() {
843: JMLListValueNode ptr = this ;
844: JMLListValueNode ret = null;
845: //@ loop_invariant ptr != this ==> ret != null;
846: //@ maintaining (* ret is the reverse of items in this up to ptr *);
847: while (ptr != null) {
848: ret = new JMLListValueNode(ptr.val == null ? null
849: : (JMLType) (ptr.val).clone(), ret);
850: ptr = ptr.next;
851: }
852: return ret;
853: }
854:
855: /** Return a list that is like this list but with the given item
856: * inserted before the given index.
857: */
858: /*@ public normal_behavior
859: @ requires 0 < n && n <= length();
860: @ ensures \result != null
861: @ && \result.equals(prefix(n).concat(cons(item, removePrefix(n))));
862: @ also
863: @ public normal_behavior
864: @ requires n == 0;
865: @ ensures \result != null && \result.equals(cons(item, this));
866: @ also
867: @ public exceptional_behavior
868: @ requires !(0 <= n && n <= length());
869: @ signals (JMLListException);
870: model public non_null
871: JMLListValueNode insertBefore(\bigint n, JMLType item)
872: throws JMLListException {
873: if ( n < 0 || (n > 1 && next == null) ) {
874: throw new JMLListException("Index to insertBefore out of range.");
875: } else if (n == 0) {
876: return cons(item, this); // cons() handles any necessary cloning
877: } else {
878: assert n > 0;
879: return new JMLListValueNode(val,
880: (next == null
881: ? cons(item, null)
882: : next.insertBefore(n-1, item)));
883: }
884: }
885: @*/
886:
887: /** Return a list that is like this list but with the given item
888: * inserted before the given index.
889: */
890: /*@ public normal_behavior
891: @ requires 0 < n && n <= int_length();
892: @ ensures \result != null
893: @ && \result.equals(prefix(n).concat(cons(item, removePrefix(n))));
894: @ also
895: @ public normal_behavior
896: @ requires n == 0;
897: @ ensures \result != null && \result.equals(cons(item, this));
898: @ also
899: @ public exceptional_behavior
900: @ requires !(0 <= n && n <= int_length());
901: @ signals (JMLListException);
902: @*/
903: public/*@ non_null @*/
904: JMLListValueNode insertBefore(int n, JMLType item)
905: throws JMLListException {
906: if (n < 0 || (n > 1 && next == null)) {
907: throw new JMLListException(
908: "Index to insertBefore out of range.");
909: } else if (n == 0) {
910: return cons(item, this ); // cons() handles any necessary cloning
911: } else {
912: return new JMLListValueNode(val, (next == null ? cons(item,
913: null) : next.insertBefore(n - 1, item)));
914: }
915: }
916:
917: /** Return a list that is like this list but without the first
918: * occurrence of the given item.
919: */
920: /*@ public normal_behavior
921: @ requires !has(item);
922: @ ensures this.equals(\result);
923: @ also
924: @ public normal_behavior
925: @ old int index = indexOf(item);
926: @ requires has(item);
927: @ ensures \result == null <==> \old(int_size() == 1);
928: @ ensures \result != null && index == 0
929: @ ==> \result.equals(removePrefix(1));
930: @ ensures \result != null && index > 0 // !FIXME! [? index == int_length() - 1]
931: @ ==> \result.equals(prefix(index).concat(removePrefix((int)(index+1))));
932: @*/
933: public JMLListValueNode remove(JMLType item) {
934: if (item == null) {
935: if (val == null) {
936: return next;
937: } else {
938: return new JMLListValueNode(val, (next == null ? null
939: : next.remove(item)));
940: }
941: } else if (item.equals(val)) {
942: return next;
943: } else {
944: return new JMLListValueNode(val, (next == null ? null
945: : next.remove(item)));
946: }
947: }
948:
949: /** Return a string representation for this list. The output is ML style.
950: */
951: public String toString() {
952: String ret = "[";
953: JMLListValueNode this Lst = this ;
954: boolean firstTime = true;
955: while (this Lst != null) {
956: if (!firstTime) {
957: ret += ", ";
958: } else {
959: firstTime = false;
960: }
961: if (this Lst.val == null) {
962: ret += "null";
963: } else {
964: ret += this Lst.val.toString();
965: }
966: this Lst = this Lst.next;
967: }
968: ret += "]";
969: return ret;
970: }
971:
972: }
|