// @(#) $Id: DualLink.jml-refined,v 1.5 2005/12/09 04:20:15 leavens 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.node2; //@ model import org.jmlspecs.models.JMLObjectSequence; public /*@ pure @*/ class DualLink extends Link { // Dual Directional Link // data members //@ public model JMLObjectSequence prevEntries; in entries; //@ public model nullable TwoWayNode dualNode; in prevEntries, node; //@ protected invariant node == dualNode; // dualNode is provided so downcasting is unnecessary in specifications /*@ public normal_behavior @ assignable entries; @ ensures node == null; @*/ public DualLink(); /*@ public normal_behavior @ assignable entries; @ ensures dualNode == node; @*/ public DualLink(/*@ nullable @*/ TwoWayNode node); /*@ public normal_behavior @ requires dualNode == null; @ assignable \nothing; @ ensures \result == null; @ also @ public normal_behavior @ requires dualNode != null; @ assignable \nothing; @ ensures \result.dualNode == dualNode.prevNode; @*/ public /*@ nullable @*/ DualLink getPrevious(); }