01: // @(#)$Id: JMLValueType.java 1.1 Mon, 02 May 2005 14:31:03 +0200 engelc $
02:
03: // Copyright (C) 1998, 1999 Iowa State University
04:
05: // This file is part of JML
06:
07: // JML is free software; you can redistribute it and/or modify
08: // it under the terms of the GNU General Public License as published by
09: // the Free Software Foundation; either version 2, or (at your option)
10: // any later version.
11:
12: // JML is distributed in the hope that it will be useful,
13: // but WITHOUT ANY WARRANTY; without even the implied warranty of
14: // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15: // GNU General Public License for more details.
16:
17: // You should have received a copy of the GNU General Public License
18: // along with JML; see the file COPYING. If not, write to
19: // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
20:
21: package org.jmlspecs.models;
22:
23: /** Objects that contain values.
24: * It is the intention that classes that implement JMLValueType provide a
25: * "value semantics" for both clone() and equal(). Equality must be defined
26: * by the ".equals()" for any objects contained within an instance of the
27: * class. clone() must use the ".clone()" methods of any objects contained in
28: * an instance of the class.
29: * Hence, classes that implement JMLValueType have objects that are
30: * "containers of values", in the sense that the user is interested
31: * in the values referenced, not not simply the "addresses".
32: *
33: * @version $Revision: 1.1 $
34: * @author Gary T. Leavens
35: * @author Albert L. Baker
36: * @see JMLType
37: */
38: //-@ immutable
39: //@ pure
40: public interface JMLValueType extends JMLType {
41:
42: /** Return a deep copy of this object.
43: */
44: /*@ also
45: @ public normal_behavior
46: @ ensures \result instanceof JMLValueType
47: @ && (* all externally-visible mutable objects
48: @ contained directly in "this" must be cloned in \result. *);
49: @ implies_that
50: @ ensures (* no direct aliases are created between this and \result *);
51: @*/
52: public/*@ pure @*/Object clone();
53:
54: /** Compare with ob2 using .equals on underlying objects.
55: */
56: /*@ also
57: @ public normal_behavior
58: @ ensures \result ==>
59: @ ob2 != null
60: @ && (* all externally-visible objects contained in ob2 test
61: @ as ".equals()" to the corresponding object in this
62: @ (and vice versa) *);
63: @*/
64: public/*@ pure @*/boolean equals(Object ob2);
65: }
|