// @(#) $Id: OneWayList.jml-refined,v 1.7 2007/07/01 02:38:46 chalin Exp $ // Copyright (C) 1998, 1999 Iowa State University // This file is part of JML // JML is free software; you can redistribute it and/or modify // it under the terms of the GNU General Public License as published by // the Free Software Foundation; either version 2, or (at your option) // any later version. // JML is distributed in the hope that it will be useful, // but WITHOUT ANY WARRANTY; without even the implied warranty of // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the // GNU General Public License for more details. // You should have received a copy of the GNU General Public License // along with JML; see the file COPYING. If not, write to // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA. // Author: Clyde Ruby package org.jmlspecs.samples.list.list3; //@ model import org.jmlspecs.models.JMLObjectSequence; // FIXME: adapt this file to non-null-by-default and remove the following modifier. /*@ nullable_by_default @*/ public class OneWayList { //@ public model JMLObjectSequence theList; //@ public model int cursor; //@ public model Object cursorEntry; in cursor; /*@ public invariant isOffFront() || isOffEnd() @ || (0 <= cursor && cursor < theList.int_length()); @*/ /*@ public invariant theList != null @ && (\forall int i; 0<=i && i