0001: // @(#)$Id: JMLListObjectNode.java 1.3 Wed, 25 May 2005 14:55:29 +0200 engelc $
0002:
0003: // Copyright (C) 1998, 1999 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: /** An implementation class used in various models. These are
0024: * singly-linked list nodes containing objects. The empty
0025: * list is represented by null, which makes dealing with these lists
0026: * tricky. Normal users should use {@link JMLObjectSequence} instead of this
0027: * type to avoid these difficulties.
0028: *
0029: * <p>
0030: * This type uses "==" to compare elements. The cons method
0031: * does not clone elements that are passed into the list.
0032: *
0033: * @version $Revision: 1.3 $
0034: * @author Gary T. Leavens
0035: * @author Albert L. Baker
0036: * @see JMLObjectSequence
0037: * @see JMLObjectBag
0038: * @see JMLObjectSet
0039: */
0040: //-@ immutable
0041: /*@ pure spec_public @*/class JMLListObjectNode implements JMLType {
0042:
0043: //*********************** equational theory ***********************
0044:
0045: /*@ public invariant (\forall JMLListObjectNode l2;
0046: @ (\forall Object e1, e2;
0047: @ (\forall \bigint n;
0048: @ equational_theory(this, l2, e1, e2, n) )));
0049: @*/
0050:
0051: /** An `equational' specification of lists, for use in the invariant.
0052: */
0053: /*@ public normal_behavior
0054: @ {|
0055: @ // The following define itemAt and size. The behavior
0056: @ // of the other methods is defined based by these two
0057: @ // methods.
0058: @
0059: @ ensures \result <==>
0060: @ (new JMLListObjectNode(e1, null)).size() == 1;
0061: @ also
0062: @ ensures \result <==>
0063: @ (ls != null)
0064: @ ==> (new JMLListObjectNode(e1, ls)).size() == 1 + ls.size();
0065: @ also
0066: @ ensures \result <==>
0067: @ (ls != null)
0068: @ ==> (ls.next == null) == (ls.size() == 1);
0069: @ also
0070: @ ensures \result <==>
0071: @ ls != null && ls.next != null
0072: @ ==> ls.size() == 1 + ls.next.size();
0073: @ also
0074: @ ensures \result <==>
0075: @ (ls != null && ls.val != null)
0076: @ ==> ls.val == (ls.head());
0077: @ also
0078: @ ensures \result <==>
0079: @ (e1 != null)
0080: @ ==> cons(e1, ls).head() == e1;
0081: @ also
0082: @ ensures \result <==>
0083: @ (ls != null && ls.val != null)
0084: @ ==> ls.itemAt(0) == (ls.head());
0085: @ also
0086: @ ensures \result <==>
0087: @ ls != null && 0 < n && n < ls.size()
0088: @ ==> ls.itemAt(n) == (ls.next.itemAt(n - 1));
0089: @ |}
0090: public pure model boolean equational_theory(
0091: JMLListObjectNode ls, JMLListObjectNode ls2,
0092: Object e1, Object e2, \bigint n);
0093: @*/
0094:
0095: /** The data contained in this list node.
0096: */
0097: public final Object val;
0098:
0099: /** The next node in this list.
0100: */
0101: public final JMLListObjectNode next;
0102:
0103: /** The type of the elements in this list. This type is an upper
0104: * bound on the element's types. The type is computed
0105: * pessimistically, so that the order of adding elements does not
0106: * matter; that is, if any element in the list is null, then we
0107: * use Object as the type of the list's elements.
0108: */
0109: //@ ghost public Object elementType;
0110: //@ public constraint elementType == \old(elementType);
0111: //@ public invariant elementType <: \type(Object);
0112: //@ public invariant val != null ==> \typeof(val) <: elementType;
0113: //@ public invariant val == null ==> \type(Object) == elementType;
0114: /*@ public invariant_redundantly
0115: @ containsNull ==> \type(Object) == elementType;
0116: @*/
0117: //@ public invariant next != null ==> next.elementType <: elementType;
0118: /** Whether this list can contain null elements;
0119: */
0120: //@ ghost public boolean containsNull;
0121: //@ public constraint containsNull == \old(containsNull);
0122: //@ public invariant containsNull <==> has(null);
0123: /*@ protected
0124: @ invariant containsNull <==>
0125: @ val == null || (next != null && next.containsNull);
0126: @*/
0127:
0128: //@ public invariant owner == null;
0129: //************************* Constructors ********************************
0130: /** Initialize this list to have the given item as its first
0131: * element followed by the given list.
0132: * This does not do any cloning.
0133: *
0134: * @param item the object to place at the head of this list.
0135: * @param nxt the _JMLListObjectNode to make the tail of this list.
0136: */
0137: /*@ public normal_behavior
0138: @ requires item != null;
0139: @ assignable val, next, elementType, containsNull, owner;
0140: @ ensures val == item && next == nxt
0141: @ && \typeof(item) <: elementType
0142: @ && (nxt != null ==> nxt.elementType <: elementType)
0143: @ && (nxt == null ==> elementType == \typeof(item))
0144: @ && containsNull == (nxt == null ? false : nxt.containsNull);
0145: @ also
0146: @ public normal_behavior
0147: @ requires item == null;
0148: @ assignable val, next, elementType, containsNull, owner;
0149: @ ensures val == null && next == nxt
0150: @ && elementType == \type(Object)
0151: @ && containsNull;
0152: @
0153: @*/
0154: public JMLListObjectNode(Object item, JMLListObjectNode nxt) {
0155: val = item;
0156: next = nxt;
0157: }
0158:
0159: /** Return a JMLListObjectNode containing the given element
0160: * followed by the given list.
0161: *
0162: * Note that cons() adds elements to the front of a list.
0163: * It handles any necessary cloning for value lists and it handles
0164: * inserting null elements.
0165: *
0166: * @param hd the object to place at the head of the result.
0167: * @param tl the JMLListObjectNode to make the tail of the result.
0168: */
0169: /*@ public normal_behavior
0170: @ ensures \result.headEquals(hd) && \result.next == tl;
0171: @ ensures \result.equals(new JMLListObjectNode(hd, tl));
0172: @
0173: @*/
0174: public static/*@ pure @*//*@ non_null @*/
0175: JMLListObjectNode cons(Object hd, JMLListObjectNode tl) {
0176: if (hd == null) {
0177: JMLListObjectNode ret = new JMLListObjectNode(null, tl);
0178: return ret;
0179: } else {
0180: Object h = hd;
0181: JMLListObjectNode ret = new JMLListObjectNode((Object) h,
0182: tl);
0183: return ret;
0184: }
0185: }
0186:
0187: //**************************** Observers **********************************
0188:
0189: /** Return the first element in this list.
0190: * Note that head() handles any cloning necessary for value lists.
0191: */
0192: /*@ public normal_behavior
0193: @ requires val != null;
0194: @ ensures \result != null && \result == val;
0195: @ also
0196: @ public normal_behavior
0197: @ requires val == null;
0198: @ ensures \result == null;
0199: @
0200: @*/
0201: public Object head() {
0202: Object ret = (val == null ? null : (Object) val);
0203: return ret;
0204: }
0205:
0206: /** Tell if the head of the list is "==" to the given
0207: * item.
0208: * @see #has(Object)
0209: */
0210: /*@ public normal_behavior
0211: @ requires val != null;
0212: @ ensures \result == (val == item);
0213: @ also
0214: @ public normal_behavior
0215: @ requires val == null;
0216: @ ensures \result == (item == null);
0217: @*/
0218: public boolean headEquals(Object item) {
0219: return elem_equals(val, item);
0220: }
0221:
0222: /** Tell if the given elements are equal, taking null into account.
0223: */
0224: private static/*@ pure @*/boolean elem_equals(Object item1,
0225: Object item2) {
0226: return (item1 != null && item1 == item2)
0227: || (item1 == null && item2 == null);
0228: }
0229:
0230: /** Return the ith element of a list.
0231: * @see #getItem(\bigint)
0232: */
0233: /*@ public normal_behavior
0234: @ requires 0 <= i && i < length();
0235: @ ensures \result != null ==>
0236: @ (* \result "==" the ith element of this *);
0237: @ also
0238: @ public exceptional_behavior
0239: @ requires !(0 <= i && i < length());
0240: @ signals (JMLListException);
0241: @
0242: model public Object itemAt(\bigint i) throws JMLListException {
0243: if (i < 0) {
0244: throw new JMLListException("Index to itemAt(int) is negative "
0245: + i);
0246: } else {
0247: \bigint k = i;
0248: assert k >= 0;
0249: JMLListObjectNode ptr = this;
0250: maintaining k >= 0;
0251: decreasing k;
0252: while (ptr != null && k > 0) {
0253: k = k - 1;
0254: ptr = ptr.next;
0255: }
0256: if (ptr == null) {
0257: throw new JMLListException("Index to itemAt(\bigint) out of range.");
0258: } else {
0259: assert ptr != null && k == 0;
0260: assume ptr.val != null
0261: ==> \typeof(ptr.val) <: \type(Object);
0262:
0263: Object ret = (ptr.val == null
0264: ? null
0265: : (Object)(ptr.val) );
0266: assume ret != null ==> \typeof(ret) <: elementType;
0267: assume !containsNull ==> ret != null;
0268: return ret;
0269: }
0270: }
0271: }
0272: @*/
0273:
0274: /** Return the ith element of a list.
0275: * @see #getItem(int)
0276: */
0277: /*@ public normal_behavior
0278: @ requires 0 <= i && i < int_length();
0279: @ ensures \result != null ==>
0280: @ (* \result "==" the ith element of this *);
0281: @ also
0282: @ public exceptional_behavior
0283: @ requires !(0 <= i && i < int_length());
0284: @ signals (JMLListException);
0285: @
0286: @ implies_that
0287: @ ensures \result != null ==> \typeof(\result) <: elementType;
0288: @ ensures !containsNull ==> \result != null;
0289: @*/
0290: public Object itemAt(int i) throws JMLListException {
0291: if (i < 0) {
0292: throw new JMLListException(
0293: "Index to itemAt(int) is negative " + i);
0294: } else {
0295: int k = i;
0296: JMLListObjectNode ptr = this ;
0297: //@ maintaining k >= 0;
0298: //@ decreasing k;
0299: while (ptr != null && k > 0) {
0300: k--;
0301: ptr = ptr.next;
0302: }
0303: if (ptr == null) {
0304: throw new JMLListException(
0305: "Index to itemAt(int) out of range.");
0306: } else {
0307: Object ret = (ptr.val == null ? null
0308: : (Object) (ptr.val));
0309: return ret;
0310: }
0311: }
0312: }
0313:
0314: /** Tells the number of elements in the sequence; a synonym for length
0315: */
0316: /*@ public normal_behavior
0317: @ ensures (* \result is the number of JMLListObjectNode(s) in this *);
0318: @
0319: @ implies_that
0320: @ ensures \result > 0;
0321: @ public model pure \bigint size() {
0322: \bigint count = 0;
0323: JMLListObjectNode ptr = this;
0324: maintaining (* ptr is count next's from this *);
0325: while (ptr != null) {
0326: ptr = ptr.next;
0327: count = count + 1;
0328: }
0329: return count;
0330: @ }
0331: @*/
0332:
0333: /** Tells the number of elements in the sequence; a synonym for length
0334: */
0335: /*@ public normal_behavior
0336: @ ensures \result == size();
0337: @
0338: @ implies_that
0339: @ ensures \result > 0;
0340: @ public model pure \bigint length() {
0341: @ return size();
0342: @ }
0343: @*/
0344:
0345: /** Tells the number of elements in the list; a synonym for length.
0346: */
0347: /*@ public normal_behavior
0348: @ ensures \result == size();
0349: @
0350: @ implies_that
0351: @ ensures \result > 0;
0352: @*/
0353: public int int_size() {
0354: int count = 0;
0355: JMLListObjectNode ptr = this ;
0356: //@ maintaining (* ptr is count next's from this *);
0357: while (ptr != null) {
0358: ptr = ptr.next;
0359: count++;
0360: }
0361: return count;
0362: }
0363:
0364: /** Tells the number of elements in the list; a synonym for size.
0365: */
0366: /*@ public normal_behavior
0367: @ ensures \result == length();
0368: @
0369: @ implies_that
0370: @ ensures \result > 0;
0371: @*/
0372: public int int_length() {
0373: return int_size();
0374: }
0375:
0376: /** Tells whether the given element is "==" to an
0377: * element in the list.
0378: */
0379: /*@ public normal_behavior
0380: @ requires item != null;
0381: @ ensures \result <==>
0382: @ (\exists int i; 0 <= i && i < int_length();
0383: @ (itemAt(i) == null
0384: @ ? item == null
0385: @ : itemAt(i) == item));
0386: @ also
0387: @ public normal_behavior
0388: @ requires item == null;
0389: @ ensures \result <==>
0390: @ (\exists int i; 0 <= i && i < int_length();
0391: @ itemAt(i) == null);
0392: @*/
0393: public boolean has(Object item) {
0394: JMLListObjectNode ptr = this ;
0395: //@ maintaining (* no earlier element is elem_equals to item *);
0396: while (ptr != null) {
0397: if (elem_equals(ptr.val, item)) {
0398: return true;
0399: }
0400: ptr = ptr.next;
0401: }
0402: return false;
0403: }
0404:
0405: /** Tells whether the elements of this list occur, in
0406: * order, at the beginning of the given list, using "==" for
0407: * comparisons.
0408: */
0409: /*@ public normal_behavior
0410: @ requires ls2 != null;
0411: @ ensures \result <==>
0412: @ int_length() <= ls2.int_length()
0413: @ && (\forall int i; 0 <= i && i < int_length();
0414: @ (ls2.itemAt(i) == null && itemAt(i) == null)
0415: @ || (ls2.itemAt(i) != null &&
0416: @ ls2.itemAt(i) == (itemAt(i))));
0417: @ also
0418: @ public normal_behavior
0419: @ requires ls2 == null;
0420: @ ensures !\result;
0421: @*/
0422: public boolean isPrefixOf(JMLListObjectNode ls2) {
0423: if (ls2 == null) {
0424: return false;
0425: }
0426: JMLListObjectNode othLst = ls2;
0427: JMLListObjectNode this Lst = this ;
0428: /*@ maintaining
0429: @ (* all earlier elements of both lists are elem_equals *);
0430: @*/
0431: while (this Lst != null && othLst != null) {
0432: if (!elem_equals(this Lst.val, othLst.val)) {
0433: return false;
0434: }
0435: this Lst = this Lst.next;
0436: othLst = othLst.next;
0437: }
0438: return this Lst == null;
0439: }
0440:
0441: /** Test whether this object's value is equal to the given argument.
0442: */
0443: /*@ also
0444: @ public normal_behavior
0445: @ requires ls2 != null && ls2 instanceof JMLListObjectNode;
0446: @ ensures \result <==> isPrefixOf((JMLListObjectNode)ls2)
0447: @ && ((JMLListObjectNode)ls2).isPrefixOf(this);
0448: @ also
0449: @ public normal_behavior
0450: @ requires ls2 == null || !(ls2 instanceof JMLListObjectNode);
0451: @ ensures \result <==> false;
0452: @*/
0453: public boolean equals(Object ls2) {
0454: if (ls2 != null && ls2 instanceof JMLListObjectNode) {
0455: JMLListObjectNode othLst = (JMLListObjectNode) ls2;
0456: JMLListObjectNode this Lst = this ;
0457: //@ maintaining (* all earlier elements of both lists are elem_equals *);
0458: while (this Lst != null && othLst != null) {
0459: if (!elem_equals(this Lst.val, othLst.val)) {
0460: return false;
0461: }
0462: this Lst = this Lst.next;
0463: othLst = othLst.next;
0464: }
0465: return (othLst == this Lst); // both must be null.
0466: } else {
0467: return false;
0468: }
0469: }
0470:
0471: /** Return a hash code for this object.
0472: */
0473: public int hashCode() {
0474: int hash = 0;
0475: JMLListObjectNode ptr = this ;
0476: while (ptr != null) {
0477: Object v = ptr.val;
0478: if (v != null) {
0479: hash += v.hashCode();
0480: }
0481: ptr = ptr.next;
0482: }
0483: return hash;
0484: }
0485:
0486: /** Return the zero-based index of the first occurrence of the given
0487: * element in the list, if there is one
0488: * @param item the Object sought in this.
0489: * @return the first index at which item occurs or -1 if it does not.
0490: */
0491: /*@ public normal_behavior
0492: @ requires has(item) && item != null;
0493: @ ensures itemAt(\result) == item
0494: @ && (\forall \bigint i; 0 <= i && i < \result;
0495: @ !(itemAt(i) != null
0496: @ && itemAt(i) == item));
0497: @ ensures_redundantly
0498: @ (* \result is the first index at which item occurs in this *);
0499: @ also
0500: @ public normal_behavior
0501: @ requires has(item) && item == null;
0502: @ ensures itemAt(\result) == null
0503: @ && (\forall \bigint i; 0 <= i && i < \result;
0504: @ itemAt(i) != null);
0505: @ ensures_redundantly
0506: @ (* \result is the first index at which null occurs in this *);
0507: @ also
0508: @ public normal_behavior
0509: @ requires !has(item);
0510: @ ensures \result == -1;
0511: @
0512: @ implies_that
0513: @ ensures \result >= -1;
0514: model public \bigint bi_indexOf(Object item) {
0515: \bigint idx = 0;
0516: JMLListObjectNode ptr = this;
0517: maintaining (* ptr is idx next's from this *);
0518: while (ptr != null) {
0519: if (elem_equals(ptr.val, item)) {
0520: return idx;
0521: }
0522: ptr = ptr.next;
0523: idx = idx + 1;
0524: }
0525: return -1;
0526: }
0527: @*/
0528:
0529: /** Return the zero-based index of the first occurrence of the given
0530: * element in the list, if there is one
0531: * @param item the Object sought in this.
0532: * @return the first index at which item occurs or -1 if it does not.
0533: */
0534: /*@ public normal_behavior
0535: @ requires has(item) && item != null;
0536: @ ensures itemAt(\result) == item
0537: @ && (\forall int i; 0 <= i && i < \result;
0538: @ !(itemAt(i) != null
0539: @ && itemAt(i) == item));
0540: @ ensures_redundantly
0541: @ (* \result is the first index at which item occurs in this *);
0542: @ also
0543: @ public normal_behavior
0544: @ requires has(item) && item == null;
0545: @ ensures itemAt(\result) == null
0546: @ && (\forall int i; 0 <= i && i < \result;
0547: @ itemAt(i) != null);
0548: @ ensures_redundantly
0549: @ (* \result is the first index at which null occurs in this *);
0550: @ also
0551: @ public normal_behavior
0552: @ requires !has(item);
0553: @ ensures \result == -1;
0554: @
0555: @ implies_that
0556: @ ensures \result >= -1;
0557: @*/
0558: public int indexOf(Object item) {
0559: int idx = 0;
0560: JMLListObjectNode ptr = this ;
0561: //@ maintaining (* ptr is idx next's from this *);
0562: while (ptr != null) {
0563: if (elem_equals(ptr.val, item)) {
0564: return idx;
0565: }
0566: ptr = ptr.next;
0567: idx++;
0568: }
0569: return -1;
0570: }
0571:
0572: /** Return the last element in this list.
0573: */
0574: /*@ public normal_behavior
0575: @ ensures (\result == null && itemAt((int)(int_length()-1)) == null)
0576: @ || \result == (itemAt((int)(int_length()-1)));
0577: @
0578: @ implies_that
0579: @ ensures \result != null ==> \typeof(\result) <: elementType;
0580: @ ensures !containsNull ==> \result != null;
0581: @*/
0582: public Object last() {
0583: if (next == null) {
0584: return head();
0585: } else {
0586: JMLListObjectNode ptr = this ;
0587: //@ maintaining ptr != null;
0588: while (ptr.next != null) {
0589: ptr = ptr.next;
0590: }
0591: Object ret = (ptr.val == null ? null : (Object) (ptr.val));
0592: return ret;
0593: }
0594: }
0595:
0596: /** Return the zero-based index of the first occurrence of the given
0597: * element in the list, if there is one
0598: * @param item the Object sought in this list.
0599: * @return the first zero-based index at which item occurs.
0600: * @exception JMLListException if the item does not occur in this list.
0601: * @see #itemAt(int)
0602: */
0603: /*@ public normal_behavior
0604: @ requires has(item);
0605: @ {|
0606: @ requires item != null;
0607: @ ensures \result == (itemAt(indexOf(item)));
0608: @ also
0609: @ requires item == null;
0610: @ ensures \result == null;
0611: @ |}
0612: @ also
0613: @ public exceptional_behavior
0614: @ requires !has(item);
0615: @ signals (JMLListException);
0616: @ implies_that
0617: @ ensures \result != null ==> \typeof(\result) <: elementType;
0618: @ ensures !containsNull ==> \result != null;
0619: @*/
0620: public Object getItem(Object item) throws JMLListException {
0621: JMLListObjectNode ptr = this ;
0622: //@ maintaining (* no earlier element is elem_equals to item *);
0623: while (ptr != null) {
0624: if (elem_equals(ptr.val, item)) {
0625: return ptr.val;
0626: }
0627: ptr = ptr.next;
0628: }
0629: throw new JMLListException("No matching item in list.");
0630: }
0631:
0632: // ******************** building new JMLObjectLists ***********************
0633:
0634: /** Return a clone of this object.
0635: */
0636: /*@ also
0637: @ public normal_behavior
0638: @ ensures \result != null && \result instanceof JMLListObjectNode
0639: @ && ((JMLListObjectNode)\result).equals(this);
0640: @*/
0641: public Object clone() {
0642: return this ;
0643: }
0644:
0645: /** Return a list containing the first n elements in this list.
0646: * @param n the number of elements to leave in the result.
0647: * @return null if n is not positive or greater than the length of this list.
0648: */
0649: /*@ public normal_behavior
0650: @ {|
0651: @ requires 0 < n && n <= length();
0652: @ ensures \result != null
0653: @ && \result.length() == n
0654: @ && (\forall \bigint i; 0 <= i && i < n;
0655: @ \result.itemAt(i) == itemAt(i));
0656: @ also
0657: @ requires n <= 0;
0658: @ ensures \result == null;
0659: @ also
0660: @ requires length() < n;
0661: @ ensures this.equals(\result);
0662: @ |}
0663: @ implies_that
0664: @ ensures !containsNull && \result != null ==> !\result.containsNull;
0665: model public JMLListObjectNode prefix(\bigint n) {
0666: return (n <= 0
0667: ? null
0668: : new JMLListObjectNode(val,
0669: (next == null ? null
0670: : next.prefix(n-1)))
0671: );
0672: }
0673: @*/
0674:
0675: /** Return a list containing the first n elements in this list.
0676: * @param n the number of elements to leave in the result.
0677: * @return null if n is not positive or greater than the length of this list.
0678: */
0679: /*@ public normal_behavior
0680: @ {|
0681: @ requires 0 < n && n <= int_length();
0682: @ ensures \result != null
0683: @ && \result.int_length() == n
0684: @ && (\forall int i; 0 <= i && i < n;
0685: @ \result.itemAt(i) == itemAt(i));
0686: @ also
0687: @ requires n <= 0;
0688: @ ensures \result == null;
0689: @ also
0690: @ requires int_length() < n;
0691: @ ensures this.equals(\result);
0692: @ |}
0693: @ implies_that
0694: @ ensures !containsNull && \result != null ==> !\result.containsNull;
0695: @*/
0696: public JMLListObjectNode prefix(int n) {
0697: return (n <= 0 ? null : new JMLListObjectNode(val,
0698: (next == null ? null : next.prefix(n - 1))));
0699: }
0700:
0701: /** Return a list containing all but the first n elements in this list.
0702: * @param n the number of elements to remove
0703: * @return null if n is negative or greater than the length of this list.
0704: */
0705: /*@ public normal_behavior
0706: @ {|
0707: @ requires 0 < n && n < length();
0708: @ ensures \result != null
0709: @ && \result.length() == length() - n
0710: @ && (\forall \bigint i; n <= i && i < length();
0711: @ \result.itemAt(i-n) == itemAt(i));
0712: @ also
0713: @ requires n <= 0;
0714: @ ensures this.equals(\result);
0715: @ also
0716: @ requires length() <= n;
0717: @ ensures \result == null;
0718: @ |}
0719: @
0720: @ implies_that
0721: @ ensures !containsNull && \result != null ==> !\result.containsNull;
0722: model public JMLListObjectNode removePrefix(\bigint n) {
0723: return (n <= 0
0724: ? this
0725: : (next == null ? null : next.removePrefix(n-1))
0726: );
0727: }
0728: @*/
0729:
0730: /** Return a list containing all but the first n elements in this list.
0731: * @param n the number of elements to remove
0732: * @return null if n is negative or greater than the length of this list.
0733: */
0734: /*@ public normal_behavior
0735: @ {|
0736: @ requires 0 < n && n < int_length();
0737: @ ensures \result != null
0738: @ && \result.int_length() == int_length() - n
0739: @ && (\forall int i; n <= i && i < int_length();
0740: @ \result.itemAt((int)(i-n)) == itemAt(i));
0741: @ also
0742: @ requires n <= 0;
0743: @ ensures this.equals(\result);
0744: @ also
0745: @ requires int_length() <= n;
0746: @ ensures \result == null;
0747: @ |}
0748: @
0749: @ implies_that
0750: @ ensures !containsNull && \result != null ==> !\result.containsNull;
0751: @*/
0752: public JMLListObjectNode removePrefix(int n) {
0753: return (n <= 0 ? this : (next == null ? null : next
0754: .removePrefix(n - 1)));
0755: }
0756:
0757: /** Return a list like this list, but without the element at the
0758: * given zero-based index.
0759: * @param n the zero-based index into the list.
0760: * @return null if the index is out of range or if the list was of size 1.
0761: */
0762: /*@ public normal_behavior
0763: @ requires n == 0 && length() == 1;
0764: @ ensures \result == null;
0765: @ also
0766: @ public normal_behavior
0767: @ requires n == 0 && length() > 1;
0768: @ ensures \result.equals(removePrefix(1));
0769: @ also
0770: @ public normal_behavior
0771: @ requires 0 < n && n < length();
0772: @ ensures \result != null
0773: @ && \result.length() == length() - 1
0774: @ && \result.equals(prefix(n).concat(removePrefix(n+1)));
0775: @ // !FIXME! This spec is inconsistent. Take n == length() - 1.
0776: @ // then removePrefix(n+1) --> removePrefix(length()) --> null.
0777: @ // But concat requires non_null. Maybe spec of concat should be relaxed?
0778: @
0779: @ implies_that
0780: @ ensures !containsNull && \result != null ==> !\result.containsNull;
0781: model public JMLListObjectNode removeItemAt(\bigint n) {
0782: return (n <= 0
0783: ? next
0784: : (next == null ? null
0785: : new JMLListObjectNode(val, next.removeItemAt(n-1)))
0786: );
0787: }
0788: @*/
0789:
0790: /** Return a list like this list, but without the element at the
0791: * given zero-based index.
0792: * @param n the zero-based index into the list.
0793: * @return null if the index is out of range or if the list was of size 1.
0794: */
0795: /*@ public normal_behavior
0796: @ requires n == 0 && int_length() == 1;
0797: @ ensures \result == null;
0798: @ also
0799: @ public normal_behavior
0800: @ requires n == 0 && int_length() > 1;
0801: @ ensures \result.equals(removePrefix(1));
0802: @ also
0803: @ public normal_behavior
0804: @ requires 0 < n && n < int_length();
0805: @ ensures \result != null
0806: @ && \result.int_length() == int_length() - 1
0807: @ && \result.equals(prefix(n).concat(removePrefix((int)(n+1))));
0808: @ // !FIXME! This spec is inconsistent. Take n == int_length() - 1.
0809: @ // then removePrefix((int)(n+1)) --> removePrefix(int_length()) --> null.
0810: @ // But concat requires non_null. Maybe spec of concat should be relaxed?
0811: @
0812: @ implies_that
0813: @ ensures !containsNull && \result != null ==> !\result.containsNull;
0814: @*/
0815: public JMLListObjectNode removeItemAt(int n) {
0816: return (n <= 0 ? next : (next == null ? null
0817: : new JMLListObjectNode(val, next.removeItemAt(n - 1))));
0818: }
0819:
0820: /** Return a list like this, but with item replacing the element at the
0821: * given zero-based index.
0822: * @param n the zero-based index into this list.
0823: * @param item the item to put at index index
0824: */
0825: /*@ public normal_behavior
0826: @ requires 0 <= n && n < length();
0827: @ ensures \result != null && \result.length() == length();
0828: @ also
0829: @ public normal_behavior
0830: @ requires n == 0 && length() == 1;
0831: @ ensures \result != null
0832: @ && \result.equals(cons(item, next));
0833: @ also
0834: @ public normal_behavior
0835: @ requires n == 0 && length() > 1;
0836: @ ensures \result != null
0837: @ && \result.equals(removePrefix(1).prepend(item));
0838: @ also
0839: @ public normal_behavior
0840: @ requires 0 < n && n == length()-1;
0841: @ ensures \result != null
0842: @ && \result.equals(prefix(n).append(item));
0843: @ also
0844: @ public normal_behavior
0845: @ requires 0 < n && n < length()-1;
0846: @ ensures \result != null && \result.length() == length()
0847: @ && \result.equals(prefix(n)
0848: @ .concat(removePrefix(n+1).prepend(item)));
0849: model public JMLListObjectNode replaceItemAt(\bigint n, Object item) {
0850: return (n <= 0
0851: ? cons(item, next) // cons() handles any necessary cloning
0852: : (next == null ? null
0853: : new JMLListObjectNode(val,
0854: next.replaceItemAt(n-1, item)))
0855: );
0856: } nowarn Post;
0857: @*/
0858:
0859: /** Return a list like this, but with item replacing the element at the
0860: * given zero-based index.
0861: * @param n the zero-based index into this list.
0862: * @param item the item to put at index index
0863: */
0864: /*@ public normal_behavior
0865: @ requires 0 <= n && n < int_length();
0866: @ ensures \result != null && \result.int_length() == int_length();
0867: @ also
0868: @ public normal_behavior
0869: @ requires n == 0 && int_length() == 1;
0870: @ ensures \result != null
0871: @ && \result.equals(cons(item, next));
0872: @ also
0873: @ public normal_behavior
0874: @ requires n == 0 && int_length() > 1;
0875: @ ensures \result != null
0876: @ && \result.equals(removePrefix(1).prepend(item));
0877: @ also
0878: @ public normal_behavior
0879: @ requires 0 < n && n == int_length()-1;
0880: @ ensures \result != null
0881: @ && \result.equals(prefix(n).append(item));
0882: @ also
0883: @ public normal_behavior
0884: @ requires 0 < n && n < int_length()-1;
0885: @ ensures \result != null && \result.int_length() == int_length()
0886: @ && \result.equals(prefix(n)
0887: @ .concat(removePrefix(n+1).prepend(item)));
0888: @*/
0889: public JMLListObjectNode replaceItemAt(int n, Object item) {
0890: return (n <= 0 ? cons(item, next) // cons() handles any necessary cloning
0891: : (next == null ? null : new JMLListObjectNode(val,
0892: next.replaceItemAt(n - 1, item))));
0893: }
0894:
0895: /** Return a list containing all but the last element in this.
0896: */
0897: /*@ public normal_behavior // !FIXME! inconsistent spec [when int_length() == 1]
0898: @ ensures \result == null ==> int_length() == 1;
0899: @ ensures \result != null ==> \result.equals(prefix((int)(int_length() - 1)));
0900: @*/
0901: public JMLListObjectNode removeLast() {
0902: return (next == null ? null : new JMLListObjectNode(val, next
0903: .removeLast()));
0904: }
0905:
0906: /** Return a list that is the concatenation of this with the given
0907: * lists.
0908: * @param ls2 the list to place at the end of this list in the
0909: * result.
0910: * @return the concatenation of this list and ls2.
0911: */
0912: /*@ public normal_behavior
0913: @ requires ls2 != null;
0914: @ ensures \result != null
0915: @ && \result.int_length() == int_length() + ls2.int_length()
0916: @ && (\forall int i; 0 <= i && i < int_length();
0917: @ \result.itemAt(i) == itemAt(i))
0918: @ && (\forall int i; 0 <= i && i < ls2.int_length();
0919: @ \result.itemAt((int)(int_length()+i)) == ls2.itemAt(i));
0920: @ ensures (* \result is the concatenation of this followed by ls2 *);
0921: @*/
0922: public/*@ non_null @*/
0923: JMLListObjectNode concat(/*@ non_null @*/JMLListObjectNode ls2) {
0924: return (next == null ? new JMLListObjectNode(val, ls2)
0925: : new JMLListObjectNode(val, next.concat(ls2)));
0926: }
0927:
0928: /** Return a list that is like this, but with the given item at
0929: * the front. Note that this clones the item if necessary.
0930: * @param item the element to place at the front of the result.
0931: */
0932: /*@ public normal_behavior
0933: @ ensures \result != null && \result.equals(cons(item, this));
0934: @ ensures_redundantly \result != null
0935: @ && \result.int_length() == int_length() + 1;
0936: @*/
0937: public/*@ non_null @*/JMLListObjectNode prepend(Object item) {
0938: // cons() handles any necessary cloning
0939: return cons(item, this );
0940: }
0941:
0942: /** Return a list that consists of this list and the given element.
0943: */
0944: /*@ public normal_behavior
0945: @ ensures \result != null
0946: @ && \result.equals(cons(item, this.reverse()).reverse());
0947: @ ensures_redundantly \result != null
0948: @ && \result.int_length() == int_length() + 1;
0949: @*/
0950: public/*@ non_null @*/JMLListObjectNode append(Object item) {
0951: // To avoid full recursion, we build the reverse of what we want in
0952: // revret, then reverse it. To make sure we only clone once,
0953: // we let reverse do the cloning
0954: JMLListObjectNode ptr = this ;
0955: JMLListObjectNode revret = null;
0956: //@ maintaining (* reverse(revret) concatenated with ptr equals this *);
0957: while (ptr != null) {
0958: revret = new JMLListObjectNode(ptr.val, revret); // don't clone yet
0959: ptr = ptr.next;
0960: }
0961: return (new JMLListObjectNode(item, revret)).reverse();
0962: }
0963:
0964: /** Return a list that is the reverse of this list.
0965: */
0966: /*@ public normal_behavior
0967: @ ensures \result.int_length() == int_length()
0968: @ && (\forall int i; 0 <= i && i < int_length();
0969: @ (\result.itemAt((int)(int_length()-i-1)) != null
0970: @ && \result.itemAt((int)(int_length()-i-1)) == (itemAt(i)))
0971: @ || (\result.itemAt((int)(int_length()-i-1)) == null
0972: @ && itemAt(i) == null) );
0973: @ ensures_redundantly
0974: @ (* \result has the same elements but with the items
0975: @ arranged in the reverse order *);
0976: @
0977: @*/
0978: public/*@ non_null @*/JMLListObjectNode reverse() {
0979: JMLListObjectNode ptr = this ;
0980: JMLListObjectNode ret = null;
0981: //@ loop_invariant ptr != this ==> ret != null;
0982: //@ maintaining (* ret is the reverse of items in this up to ptr *);
0983: while (ptr != null) {
0984: ret = new JMLListObjectNode(ptr.val == null ? null
0985: : (Object) (ptr.val), ret);
0986: ptr = ptr.next;
0987: }
0988: return ret;
0989: }
0990:
0991: /** Return a list that is like this list but with the given item
0992: * inserted before the given index.
0993: */
0994: /*@ public normal_behavior
0995: @ requires 0 < n && n <= length();
0996: @ ensures \result != null
0997: @ && \result.equals(prefix(n).concat(cons(item, removePrefix(n))));
0998: @ also
0999: @ public normal_behavior
1000: @ requires n == 0;
1001: @ ensures \result != null && \result.equals(cons(item, this));
1002: @ also
1003: @ public exceptional_behavior
1004: @ requires !(0 <= n && n <= length());
1005: @ signals (JMLListException);
1006: model public non_null
1007: JMLListObjectNode insertBefore(\bigint n, Object item)
1008: throws JMLListException {
1009: if ( n < 0 || (n > 1 && next == null) ) {
1010: throw new JMLListException("Index to insertBefore out of range.");
1011: } else if (n == 0) {
1012: return cons(item, this); // cons() handles any necessary cloning
1013: } else {
1014: assert n > 0;
1015: return new JMLListObjectNode(val,
1016: (next == null
1017: ? cons(item, null)
1018: : next.insertBefore(n-1, item)));
1019: }
1020: }
1021: @*/
1022:
1023: /** Return a list that is like this list but with the given item
1024: * inserted before the given index.
1025: */
1026: /*@ public normal_behavior
1027: @ requires 0 < n && n <= int_length();
1028: @ ensures \result != null
1029: @ && \result.equals(prefix(n).concat(cons(item, removePrefix(n))));
1030: @ also
1031: @ public normal_behavior
1032: @ requires n == 0;
1033: @ ensures \result != null && \result.equals(cons(item, this));
1034: @ also
1035: @ public exceptional_behavior
1036: @ requires !(0 <= n && n <= int_length());
1037: @ signals (JMLListException);
1038: @*/
1039: public/*@ non_null @*/
1040: JMLListObjectNode insertBefore(int n, Object item)
1041: throws JMLListException {
1042: if (n < 0 || (n > 1 && next == null)) {
1043: throw new JMLListException(
1044: "Index to insertBefore out of range.");
1045: } else if (n == 0) {
1046: return cons(item, this ); // cons() handles any necessary cloning
1047: } else {
1048: return new JMLListObjectNode(val, (next == null ? cons(
1049: item, null) : next.insertBefore(n - 1, item)));
1050: }
1051: }
1052:
1053: /** Return a list that is like this list but without the first
1054: * occurrence of the given item.
1055: */
1056: /*@ public normal_behavior
1057: @ requires !has(item);
1058: @ ensures this.equals(\result);
1059: @ also
1060: @ public normal_behavior
1061: @ old int index = indexOf(item);
1062: @ requires has(item);
1063: @ ensures \result == null <==> \old(int_size() == 1);
1064: @ ensures \result != null && index == 0
1065: @ ==> \result.equals(removePrefix(1));
1066: @ ensures \result != null && index > 0 // !FIXME! [? index == int_length() - 1]
1067: @ ==> \result.equals(prefix(index).concat(removePrefix((int)(index+1))));
1068: @*/
1069: public JMLListObjectNode remove(Object item) {
1070: if (item == null) {
1071: if (val == null) {
1072: return next;
1073: } else {
1074: return new JMLListObjectNode(val, (next == null ? null
1075: : next.remove(item)));
1076: }
1077: } else if (item == val) {
1078: return next;
1079: } else {
1080: return new JMLListObjectNode(val, (next == null ? null
1081: : next.remove(item)));
1082: }
1083: }
1084:
1085: /** Return a string representation for this list. The output is ML style.
1086: */
1087: public String toString() {
1088: String ret = "[";
1089: JMLListObjectNode this Lst = this ;
1090: boolean firstTime = true;
1091: while (this Lst != null) {
1092: if (!firstTime) {
1093: ret += ", ";
1094: } else {
1095: firstTime = false;
1096: }
1097: if (this Lst.val == null) {
1098: ret += "null";
1099: } else {
1100: ret += this Lst.val.toString();
1101: }
1102: this Lst = this Lst.next;
1103: }
1104: ret += "]";
1105: return ret;
1106: }
1107:
1108: }
|