BABYL OPTIONS: -*- rmail -*- Version: 5 Labels: Note: This is the header of an rmail file. Note: If you are seeing it in rmail, Note: it means the file has no messages in it.  1, filed,, X-Coding-System: undecided-unix Mail-from: From leavens@cs.iastate.edu Fri Jan 7 11:17:28 2000 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id LAA29773; Fri, 7 Jan 2000 11:17:26 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id LAA28136; Fri, 7 Jan 2000 11:17:21 -0600 (CST) Date: Fri, 7 Jan 2000 11:17:21 -0600 (CST) Message-Id: <200001071717.LAA28136@larch.cs.iastate.edu> From: "Gary T. Leavens" To: rustan@pa.dec.com CC: leavens@cs.iastate.edu In-reply-to: <199912221631.KAA23932@ren.cs.iastate.edu> (leavens@cs.iastate.edu) Subject: Re: JML-Interest: Re: lightweight specifications and the default for JML's modifiable clause References: <199912221631.KAA23932@ren.cs.iastate.edu> *** EOOH *** Date: Fri, 7 Jan 2000 11:17:21 -0600 (CST) From: "Gary T. Leavens" To: rustan@pa.dec.com CC: leavens@cs.iastate.edu In-reply-to: <199912221631.KAA23932@ren.cs.iastate.edu> (leavens@cs.iastate.edu) Subject: Re: JML-Interest: Re: lightweight specifications and the default for JML's modifiable clause Rustan, Hope you're having a great century so far. When you get a chance, could you react to this e-mail? I think that the proposal contained in the first paragraph below would be workable, if that's agreeable to you. Gary > Date: Wed, 22 Dec 1999 10:31:24 -0600 (CST) > From: "Gary T. Leavens" > CC: leavens@cs.iastate.edu > Sender: owner-jml-interest-list@cs.iastate.edu > Precedence: bulk > > Rustan, et al, > > I wonder if having a default for the modifiable clause in lightweight > specifications be "not specified" would be better. This could be > interpreted as "everything" for purposes of formal verification, and it > would turn off checking in static analysis tools like ESC/Java. > That way we wouldn't lose information that the modifiable clause simply > wasn't specified, instead of trying to choose a default. > > Rustan, while I understand that you would be happy with "modifiable: \nothing" > as the default, even for lightweight specifications even if you did > enforce it, I'm not so sure it fits with your philosophy. Doing that > would effectively mean people would have to specify the modifiable > clause for everything that made assignments. That doesn't seem so > lightweight. > > Gary > > > Cc: jml-interest@cs.iastate.edu > > Date: Tue, 21 Dec 1999 17:13:17 -0800 > > From: "K. Rustan M. Leino" > > X-Mts: smtp > > > > > > | From: "Gary T. Leavens" > > | [...] > > | public void inc_x() > > | //@ requires: x < Integer.MAX_VALUE; > > | { > > | x = x + 1; > > | } > > | [...] > > | Rustan, when the modifiable clause is omitted in the specification of a > > | method in ESC/Java, does ESC/Java complain when assignments are made in > > | the method? > > > > ESC/Java is intended for lightweight specifications and it uses "modifiable > > \nothing" as the default modifies clause. While I'm happy with this > > choice for ESC/Java, it does turn out that ESC/Java currently does > > not enforce modifies clauses. Thus, ESC/Java would not complain > > about the assignment to "x" in your example. > > > > We do have a plan for doing partial modifies clause checking, but > > we've never implemented it. That plan is that "o.f" is allowed to > > be modified if either "o.f" is mentioned in a modifies clause, "o" > > is newly allocated, or "o" not a formal parameter or static field. > > If we did implement this plan, I would still be happy with the choice > > of "modifiable \nothing" as the default modifies clause. > > > > Rustan > > >  1,, Summary-line: 7-Jan rustan@pa.dec.com [76] #Re: JML-Interest: Re: lightweight specifications and the default for JML's modifiable clause X-Coding-System: undecided-unix Mail-from: From rustan@pa.dec.com Fri Jan 7 13:25:54 2000 Return-Path: Received: from mail1.digital.com (mail1.digital.com [204.123.2.50]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id NAA03186; Fri, 7 Jan 2000 13:25:51 -0600 (CST) Received: from neuf.pa.dec.com (neuf.pa.dec.com [16.4.80.69]) by mail1.digital.com (8.9.2/8.9.2/WV2.0g) with SMTP id LAA20748; Fri, 7 Jan 2000 11:25:48 -0800 (PST) Received: by neuf.pa.dec.com; id AA24689; Fri, 7 Jan 2000 11:25:48 -0800 Message-Id: <200001071925.AA24689@neuf.pa.dec.com> To: "Gary T. Leavens" Cc: jml-interest@cs.iastate.edu Subject: Re: JML-Interest: Re: lightweight specifications and the default for JML's modifiable clause In-Reply-To: Message of Fri, 7 Jan 2000 11:17:21 -0600 (CST) from "Gary T. Leavens" <200001071717.LAA28136@larch.cs.iastate.edu> Date: Fri, 07 Jan 2000 11:25:48 -0800 From: "K. Rustan M. Leino" X-Mts: smtp *** EOOH *** To: "Gary T. Leavens" Cc: jml-interest@cs.iastate.edu Subject: Re: JML-Interest: Re: lightweight specifications and the default for JML's modifiable clause In-Reply-To: Message of Fri, 7 Jan 2000 11:17:21 -0600 (CST) from "Gary T. Leavens" <200001071717.LAA28136@larch.cs.iastate.edu> Date: Fri, 07 Jan 2000 11:25:48 -0800 From: "K. Rustan M. Leino" X-Mts: smtp Gary, Sorry for the late reply. | From: "Gary T. Leavens" | Date: Wed, 22 Dec 1999 10:31:24 -0600 (CST) | | Rustan, et al, | | I wonder if having a default for the modifiable clause in lightweight | specifications be "not specified" would be better. This could be | interpreted as "everything" for purposes of formal verification, and it | would turn off checking in static analysis tools like ESC/Java. | That way we wouldn't lose information that the modifiable clause simply | wasn't specified, instead of trying to choose a default. Yes, I think it would be nice to know which routines have a specification and which are to be treated as unknown. This would even cater for checkers that would want the strongest possible checking (that is, the checking that will produce the largest number of spurious warnings) as follows: for every call, take an omitted modifiable clause to mean "modifiable \everything", and for every implementation, take an omitted modifiable clause to mean "modifiable \nothing". Note, if an omitted specifiction would mean calls can't be checked, then programmers have a lot of specifications (in libraries, etc.) to write down. This suggests that having some default meaning for an omitted specification is a good idea (even if the meaning varies with the use of the specification, for example calling contexts vs. checking an implementation). | | Rustan, while I understand that you would be happy with "modifiable: \nothing" | as the default, even for lightweight specifications even if you did | enforce it, I'm not so sure it fits with your philosophy. Doing that | would effectively mean people would have to specify the modifiable | clause for everything that made assignments. That doesn't seem so | lightweight. Your observations are correct about having to specify every routine that makes an assignment (to a field of an object that is not freshly allocated). However, by choosing "modifiable \everything" as the default, callers will be unhappy because the entire world might change as a result of a call. This effectively means people would have to specify the modifiable clause for everything that they call. This is probably worse, for suppose the thing called lives in an unannotated library whose source code you don't own, then you might have trouble declaring a specification for it at all. And consider a beginning programmer who write one short method implementation that contains some calls to unannotated libraries. Instead of just having to specify her own method, that programmer would have to write specifications for the libraries she calls. Rustan  1,, X-Coding-System: undecided-unix Mail-from: From leavens@cs.iastate.edu Fri Jan 7 13:46:12 2000 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id NAA03722; Fri, 7 Jan 2000 13:46:09 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id NAA29823; Fri, 7 Jan 2000 13:46:03 -0600 (CST) Date: Fri, 7 Jan 2000 13:46:03 -0600 (CST) Message-Id: <200001071946.NAA29823@larch.cs.iastate.edu> From: "Gary T. Leavens" To: rustan@pa.dec.com CC: jml-interest@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: <200001071925.AA24689@neuf.pa.dec.com> (rustan@pa.dec.com) Subject: Re: JML-Interest: Re: lightweight specifications and the default for JML's modifiable clause References: <200001071925.AA24689@neuf.pa.dec.com> *** EOOH *** Date: Fri, 7 Jan 2000 13:46:03 -0600 (CST) From: "Gary T. Leavens" To: rustan@pa.dec.com CC: jml-interest@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: <200001071925.AA24689@neuf.pa.dec.com> (rustan@pa.dec.com) Subject: Re: JML-Interest: Re: lightweight specifications and the default for JML's modifiable clause Rustan, Thanks for your response. I think we're in agreement now, so my plan is to add to JML "\not_specified", and to use that as the default for the modifiable clause in the lightweight specifications (those without some sort of "behavior" keyword). The default when one of the "behavior" keywords is used, would be "modifiable \nothing" as is currently the case. Other comments anyone? Gary  1,, X-Coding-System: undecided-unix Mail-from: From erikpoll@cs.kun.nl Tue Jan 11 06:26:29 2000 Return-Path: Received: from pandora.cs.kun.nl (pandora.cs.kun.nl [131.174.33.4]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id GAA09376 for ; Tue, 11 Jan 2000 06:26:27 -0600 (CST) Received: from hera.cs.kun.nl by pandora.cs.kun.nl via hera.cs.kun.nl [131.174.33.2] with SMTP for id NAA02436 (8.8.8/3.12); Tue, 11 Jan 2000 13:26:21 +0100 (MET) Date: Tue, 11 Jan 2000 13:26:20 +0100 (MET) From: Erik Poll To: "Gary T. Leavens" Subject: Re: JML-Interest: Re: lightweight specifications and the default for JML's modifiable clause In-Reply-To: <200001071946.NAA29823@larch.cs.iastate.edu> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII *** EOOH *** Date: Tue, 11 Jan 2000 13:26:20 +0100 (MET) From: Erik Poll To: "Gary T. Leavens" Subject: Re: JML-Interest: Re: lightweight specifications and the default for JML's modifiable clause In-Reply-To: <200001071946.NAA29823@larch.cs.iastate.edu> Content-Type: TEXT/PLAIN; charset=US-ASCII On Fri, 7 Jan 2000, Gary T. Leavens wrote: > Thanks for your response. I think we're in agreement now, so my plan is > to add to JML "\not_specified", and to use that as the > default for the modifiable clause in the lightweight specifications > (those without some sort of "behavior" keyword). I don't follow this. Where & how would one use this "\not_specified", and what does it mean ? Does the lightweight spec //@ requires: x < Integer.MAX_VALUE; mean the same as //@ requires: x < Integer.MAX_VALUE; //@ modifiable: \not_specified and, if so, what's does "modifiable: \not_specified" mean here ? Erik  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Tue Jan 11 08:36:28 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id IAA11644 for jml-interest-list-outgoing; Tue, 11 Jan 2000 08:36:13 -0600 (CST) Received: from pandora.cs.kun.nl (pandora.cs.kun.nl [131.174.33.4]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id IAA11640 for ; Tue, 11 Jan 2000 08:36:10 -0600 (CST) Received: from hera.cs.kun.nl by pandora.cs.kun.nl via hera.cs.kun.nl [131.174.33.2] with SMTP for id PAA06618 (8.8.8/3.12); Tue, 11 Jan 2000 15:36:08 +0100 (MET) Date: Tue, 11 Jan 2000 15:36:08 +0100 (MET) From: Erik Poll To: jml-interest@cs.iastate.edu Subject: JML-Interest: JML-interest: parameters & modifiability Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Tue, 11 Jan 2000 15:36:08 +0100 (MET) From: Erik Poll To: jml-interest@cs.iastate.edu Subject: JML-Interest: JML-interest: parameters & modifiability Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi all, I have two questions about the modifiablity of parameters of methods: (i) If a method modifies one of its parameters, should this be declared in a modifiable clause ? For example, in a spec for int m (int j) {j=j+1; return 5;} do we have to declare j as modifiable ? I would think not, and that we only use modifiable for fields of objects. There are good reasons for saying that it is silly to have to declare j as modifiable. After all, j is passed by value, and whether or not j is modified is of no interest whatsoever to anyone invoking the method. Saying that j may not be modified unless this is allowed by the specification imposes an unneccesary restriction on the implementor, and it a bit strange for _behavioural_ specifications to impose such restrictions. (ii) Suppose a method may modify its parameter j (irrespective of the answer to (i), ie. of whether this is by default or because this has been explicitly declared). We then have to be VERY careful with writing its postcondition, because j and \old(j) may not be the same value. For example, consider the following lightweight spec int choose (int j) //@ modifiable: \everything; //or can I omit this modifiable clause because it's the default now ? //@ ensures: \result < j; A possible implementation is int choose (int j) {j=j+10; return j-1;} This is probably not what we intended ! Someone who has read the spec above will be very surprised when choose(8) returns 17. To rule out such sick implementations, we should specify the method as follows //@ ensures: \result < \old(i) The same problem occurs with parameters that have a reference type. For instance, the specification void m (byte[] arr) /*@ behaviour modifiable: \everything; ensures: arr[0] == 1; signals: (NullPointerException) arr==null; @*/ can be implemented as { arr = new byte[27]; arr[0] = 1; } or { arr = null; throw (new NullPointerException()); } Again, this is probably not what we want; we should have specified the method as follows: ensures: \old(arr)[0] == 1; signals: (NullPointerException) \old(arr)==null; It is extremely annoying to have to write \old around all parameters in the postcondition, i.e. in ensures and signals clauses; it really clutters things up. It is very easy to end up with an incorrect spec, either by forgetting to write \old somewhere (or everywhere, if one is not aware of this problem), or by making mistakes, like confusing \old(arr)[0] and \old(arr[0]). I see two ways to avoid these problems, by saying: (a) parameters may not be modified unless explicitly declared as modifiable or (b) any occurrence of a parameter name in a postcondition always refers to the \old value of this parameter. Of course (a) brings us back to question (i). If we do not like the restrictions this imposes on the code, or if we're specifying existing methods which happen to modify their parameters, then we still have to resort to using \old(j), \old(arr), ... in postconditions. >From a practical point of view, (b) always seems to give specifications their intended meaning. I cannot think of any sensible spec where one would want to refer to the new value that a parameter has at the end of the method invocation. The parameter is a local variable which will cease to exist when the method invocation ends anyway. (Of course, it may be confusing to have these implicit \old's; one could image that the jml compiler made them explicit. A more conservative option than (b) would be to have the jml compiler produce warnings whenever we refer to the new as opposed to the old value of a parameter, to warn us of probable errors in the spec.) One can also think of variations of (a) or (b) where variables of primitive type and variables of reference type are treated differently. Though the problem is the same for primitive and reference types, for parameters that have a reference type we can construct sicker examples than the ones given so far. For example: void sick (byte[] arr) //@ ensures: arr[0] == \old(arr[0]) // or: \not_modified(arr[0]) { byte[] original; original = arr; arr = arr.clone(); original[0] = 23; } One can argue that this spec if correct, because "arr[0] == \old(arr[0])" does hold at the end of invoking sick; it is \old(arr)[0] that has been changed to 23. But anyone invoking sick, eg as "sick(c)", will notice that c[0] has changed to 23. Any thoughts ? Erik  1, filed,, X-Coding-System: undecided-unix Mail-from: From erikpoll@cs.kun.nl Tue Jan 11 06:26:29 2000 Return-Path: Received: from pandora.cs.kun.nl (pandora.cs.kun.nl [131.174.33.4]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id GAA09376 for ; Tue, 11 Jan 2000 06:26:27 -0600 (CST) Received: from hera.cs.kun.nl by pandora.cs.kun.nl via hera.cs.kun.nl [131.174.33.2] with SMTP for id NAA02436 (8.8.8/3.12); Tue, 11 Jan 2000 13:26:21 +0100 (MET) Date: Tue, 11 Jan 2000 13:26:20 +0100 (MET) From: Erik Poll To: "Gary T. Leavens" Subject: Re: JML-Interest: Re: lightweight specifications and the default for JML's modifiable clause In-Reply-To: <200001071946.NAA29823@larch.cs.iastate.edu> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII *** EOOH *** Date: Tue, 11 Jan 2000 13:26:20 +0100 (MET) From: Erik Poll To: "Gary T. Leavens" Subject: Re: JML-Interest: Re: lightweight specifications and the default for JML's modifiable clause In-Reply-To: <200001071946.NAA29823@larch.cs.iastate.edu> Content-Type: TEXT/PLAIN; charset=US-ASCII On Fri, 7 Jan 2000, Gary T. Leavens wrote: > Thanks for your response. I think we're in agreement now, so my plan is > to add to JML "\not_specified", and to use that as the > default for the modifiable clause in the lightweight specifications > (those without some sort of "behavior" keyword). I don't follow this. Where & how would one use this "\not_specified", and what does it mean ? Does the lightweight spec //@ requires: x < Integer.MAX_VALUE; mean the same as //@ requires: x < Integer.MAX_VALUE; //@ modifiable: \not_specified and, if so, what's does "modifiable: \not_specified" mean here ? Erik  1,, X-Coding-System: undecided-unix Mail-from: From leavens@cs.iastate.edu Tue Jan 11 12:16:46 2000 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id MAA15817; Tue, 11 Jan 2000 12:16:45 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id MAA06905; Tue, 11 Jan 2000 12:16:39 -0600 (CST) Date: Tue, 11 Jan 2000 12:16:39 -0600 (CST) Message-Id: <200001111816.MAA06905@larch.cs.iastate.edu> From: "Gary T. Leavens" To: erikpoll@cs.kun.nl CC: leavens@cs.iastate.edu, jml-interest@cs.iastate.edu In-reply-to: (message from Erik Poll on Tue, 11 Jan 2000 13:26:20 +0100 (MET)) Subject: Re: JML-Interest: Re: lightweight specifications and the default for JML's modifiable clause References: *** EOOH *** Date: Tue, 11 Jan 2000 12:16:39 -0600 (CST) From: "Gary T. Leavens" To: erikpoll@cs.kun.nl CC: leavens@cs.iastate.edu, jml-interest@cs.iastate.edu In-reply-to: (message from Erik Poll on Tue, 11 Jan 2000 13:26:20 +0100 (MET)) Subject: Re: JML-Interest: Re: lightweight specifications and the default for JML's modifiable clause Erik, > Date: Tue, 11 Jan 2000 13:26:20 +0100 (MET) > From: Erik Poll > Content-Type: TEXT/PLAIN; charset=US-ASCII > > On Fri, 7 Jan 2000, Gary T. Leavens wrote: > > > Thanks for your response. I think we're in agreement now, so my plan is > > to add to JML "\not_specified", and to use that as the > > default for the modifiable clause in the lightweight specifications > > (those without some sort of "behavior" keyword). > > I don't follow this. Where & how would one use this "\not_specified", Generally, one would not explicitly write down a specification using "\not_specified". It would just come out as the default. > ... and > what does it mean ? Does the lightweight spec > > //@ requires: x < Integer.MAX_VALUE; > > mean the same as > > //@ requires: x < Integer.MAX_VALUE; > //@ modifiable: \not_specified Yes. > and, if so, what's does "modifiable: \not_specified" mean here ? Right, this is the key question. I think it will mean different things when used for different purposes by in different systems. For purposes of formal verification, what it should mean, I think, is that there is no frame axiom added to the postcondition. What I'm thinking of here is boiling down specifications into a pre- and postcondition pair. For example, the meaning of the specification you gave //@ requires: x < Integer.MAX_VALUE; //@ modifiable: \not_specified; Should be the same as the pre- and postcondition pair: /*@ behavior @ requires: x < Integer.MAX_VALUE; @ ensures: true; @*/ Note that, for the purpose of formal verification, this is the same the desugaring one would get from the lightweight specification: //@ requires: x < Integer.MAX_VALUE; //@ modifiable: \everything; However, ESC/Java would treat these differently. I believe, that the meaning of the original specification you gave in for ESC/Java would be the same as that of the following specification: //@ requires: x < Integer.MAX_VALUE; //@ modifiable: \nothing; One of the original motivations for considering this has to do with how the defaults for the modifiable clause interacted with the "also" combination of specification cases. In particular, if one writes something like: /*@ @ requires: x < Integer.MAX_VALUE; @ also: @ modifiable: x; @*/ then we would like this to be sensible. With this proposal the meaning of this is the same as: /*@ @ requires: x < Integer.MAX_VALUE; @ modifiable: \not_specified; @ ensures: true; @ also: @ modifiable: x; @ ensures: true; @*/ which should be the same as: /*@ @ behavior @ requires: x < Integer.MAX_VALUE; @ modifiable: \not_specified; @ ensures: true; @ signals (Exception): true; @ also: @ behavior @ requires: true; @ modifiable: x; @ ensures: true; @ signals (Exception): true; @*/ which should desugar into: /*@ @ behavior @ requires: x < Integer.MAX_VALUE || true; @ modifiable: x; @ ensures: (x < Integer.MAX_VALUE ==> true) @ && (true ==> true); @ signals (Exception): (x < Integer.MAX_VALUE ==> true) @ && (true ==> true); @*/ Notice that in this last specification, there is no frame that comes from the first specification case; that would not have been true with the old semantics of having the modifiable clause default to "\nothing". Generalizing, I propose that in an "also" and in an "and" combination, the meaning of "modifiable: \not_specified" be that there is no effect on the combination. In essence, this is the same as the meaning of a "modifiable: \everything" in these situations. In summary, Erik, you, for the work you are doing personally, can take "\not_specified" to mean the same thing as "\everything". Good question. Does that clear things up? Gary  1,, X-Coding-System: undecided-unix Mail-from: From leavens@cs.iastate.edu Tue Jan 11 14:54:49 2000 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id OAA19309; Tue, 11 Jan 2000 14:54:48 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id OAA08269; Tue, 11 Jan 2000 14:54:41 -0600 (CST) Date: Tue, 11 Jan 2000 14:54:41 -0600 (CST) Message-Id: <200001112054.OAA08269@larch.cs.iastate.edu> From: "Gary T. Leavens" To: erikpoll@cs.kun.nl CC: jml-interest@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Tue, 11 Jan 2000 15:36:08 +0100 (MET)) Subject: Re: JML-Interest: JML-interest: parameters & modifiability References: *** EOOH *** Date: Tue, 11 Jan 2000 14:54:41 -0600 (CST) From: "Gary T. Leavens" To: erikpoll@cs.kun.nl CC: jml-interest@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Tue, 11 Jan 2000 15:36:08 +0100 (MET)) Subject: Re: JML-Interest: JML-interest: parameters & modifiability Dear Erik, et al., > Date: Tue, 11 Jan 2000 15:36:08 +0100 (MET) > From: Erik Poll > > I have two questions about the modifiablity of parameters of methods: > > (i) > > If a method modifies one of its parameters, should this be declared in a > modifiable clause ? For example, in a spec for > > int m (int j) {j=j+1; return 5;} > > do we have to declare j as modifiable ? > > I would think not, and that we only use modifiable for fields of > objects. Yes, I agree with you that j is not modifiable from the clients' point of view. Technically this is because Java uses call by value, as you point out below. > There are good reasons for saying that it is silly to have to declare j > as modifiable. After all, j is passed by value, and whether or not j is > modified is of no interest whatsoever to anyone invoking the method. > Saying that j may not be modified unless this is allowed by the > specification imposes an unneccesary restriction on the implementor, > and it a bit strange for _behavioural_ specifications to impose such > restrictions. Right. > (ii) > > Suppose a method may modify its parameter j (irrespective of the answer > to (i), ie. of whether this is by default or because this has been > explicitly declared). We then have to be VERY careful with writing > its postcondition, because j and \old(j) may not be the same value. > For example, consider the following lightweight spec > > int choose (int j) > //@ modifiable: \everything; > //or can I omit this modifiable clause because it's the default now ? > //@ ensures: \result < j; You can omit that modifiable clause, but then it won't mean the same thing as what you wrote. It would mean instead \not_specified. > A possible implementation is > > int choose (int j) {j=j+10; return j-1;} > > This is probably not what we intended ! Someone who has read the spec > above will be very surprised when choose(8) returns 17. Yes, I do not believe that should be correct. Indeed I think that a better specification of what you want is the following: int choose (int j) //@ modifiable: \nothing; //@ ensures: \result < j; > To rule out such > sick implementations, we should specify the method as follows > > //@ ensures: \result < \old(i) > > The same problem occurs with parameters that have a reference type. > For instance, the specification > > void m (byte[] arr) > /*@ behaviour > modifiable: \everything; > ensures: arr[0] == 1; > signals: (NullPointerException) arr==null; > @*/ > > can be implemented as > > { arr = new byte[27]; arr[0] = 1; } > or > { arr = null; throw (new NullPointerException()); } > > Again, this is probably not what we want; we should have specified > the method as follows: > > ensures: \old(arr)[0] == 1; > signals: (NullPointerException) \old(arr)==null; > > > It is extremely annoying to have to write \old around all parameters in > the postcondition, i.e. in ensures and signals clauses; it really > clutters things up. > It is very easy to end up with an incorrect spec, either by forgetting to > write \old somewhere (or everywhere, if one is not aware of this problem), > or by making mistakes, like confusing \old(arr)[0] and \old(arr[0]). Yes, I agree with this analysis of the problem. > I see two ways to avoid these problems, by saying: > > (a) parameters may not be modified unless explicitly declared as modifiable > > or > > (b) any occurrence of a parameter name in a postcondition always refers to > the \old value of this parameter. > > Of course (a) brings us back to question (i). If we do not like the > restrictions this imposes on the code, or if we're specifying existing > methods which happen to modify their parameters, then we still have to > resort to using \old(j), \old(arr), ... in postconditions. While I'm not really opposed to this, one of the goals of JML was to deal to specify as much Java code as possible, regardless of the programming style in which it was written. This would seem to contradict that. > From a practical point of view, (b) always seems to give specifications > their intended meaning. I cannot think of any sensible spec where one > would want to refer to the new value that a parameter has at the end of > the method invocation. The parameter is a local variable which will > cease to exist when the method invocation ends anyway. > > (Of course, it may be confusing to have these implicit \old's; one could > image that the jml compiler made them explicit. A more conservative option > than (b) would be to have the jml compiler produce warnings whenever we > refer to the new as opposed to the old value of a parameter, to warn > us of probable errors in the spec.) I agree, although I'm not sure which you mean by the JML "compiler". I think that option (b) is quite sensible given the call by value semantics of Java. > One can also think of variations of (a) or (b) where variables of > primitive type and variables of reference type are treated > differently. I'd rather not make a special case based on this type distinction, although I admit it's possible. > Though the problem is the same for primitive and reference types, for > parameters that have a reference type we can construct sicker examples > than the ones given so far. For example: > > void sick (byte[] arr) > > //@ ensures: arr[0] == \old(arr[0]) // or: \not_modified(arr[0]) > > { byte[] original; > original = arr; > arr = arr.clone(); > original[0] = 23; > } > > One can argue that this spec if correct, because "arr[0] == \old(arr[0])" > does hold at the end of invoking sick; it is \old(arr)[0] that has been > changed to 23. But anyone invoking sick, eg as "sick(c)", will notice > that c[0] has changed to 23. Right. > Any thoughts ? On the other hand, Eiffel would make you just write these uses of \old. However, the situation in Eiffel is a bit different, because the specifications are written as part of the code (the ensures clause goes at the end of a method body). I suppose someone could argue that using \old explicitly as in Eiffel would be more readable, but it does seem to get in the way to me. Comments? Gary  1, answered,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Thu Jan 13 18:27:01 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id SAA09190 for jml-interest-list-outgoing; Thu, 13 Jan 2000 18:26:52 -0600 (CST) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id SAA09185; Thu, 13 Jan 2000 18:26:46 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id SAA01015; Thu, 13 Jan 2000 18:26:37 -0600 (CST) Date: Thu, 13 Jan 2000 18:26:37 -0600 (CST) Message-Id: <200001140026.SAA01015@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: defaults for omitted clauses in JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Thu, 13 Jan 2000 18:26:37 -0600 (CST) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: defaults for omitted clauses in JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk In our seminar today at Iowa state we discussed the defaults for omitted clauses in JML. I have written at discussion up into the following which appears in appendix A of the JML preliminary design document, which I have updated on the Web (without yet assigning in a new revision number). I put a copy of that below for your convenience. Forgive the formatting (this is the info version). Gary If a specification case does not use one of the behavior keywords (`behavior', `normal_behavior', or `exceptional_behavior'), then it is called a "lightweight" specification. When the various clauses of a specification case are omitted, they have the defaults given in the table below. The table distinguishes between lightweight and non-lightweight specifications. The only differences in the defaults are for the `modifiable' and `diverges' clauses. The idea is that in a lightweight specification, no assumption is made about the meaning of an omitted clause. However, in a non-lightweight specification, the specifier is assumed to be giving a complete specification. Therefore, in a non-lightweight specification the meaning of an omitted modifiable clause is that nothing can be modified. Furthermore, in a non-lightweight specification, the meaning of an omitted diverges clause is that the method may not diverge in that case. ` Default' `Omitted clause lightweight non-lightweight' ___________________________________________________ `requires: true true' `when: true true' `measured_by: \not_specified \not_specified' `modifiable: \not_specified \nothing' `ensures: true true' `signals: (Exception) true (Exception) true' `diverges: true false' A completely omitted specification is taken to be a lightweight specification. Thus one can read off the meaning of a completely omitted specification from the lightweight column of table.  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Mon Jan 24 14:55:07 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id OAA19234 for jml-interest-list-outgoing; Mon, 24 Jan 2000 14:54:48 -0600 (CST) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id OAA19229; Mon, 24 Jan 2000 14:54:43 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id OAA14416; Mon, 24 Jan 2000 14:54:35 -0600 (CST) Date: Mon, 24 Jan 2000 14:54:35 -0600 (CST) Message-Id: <200001242054.OAA14416@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: privacy of method specifications Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Mon, 24 Jan 2000 14:54:35 -0600 (CST) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: privacy of method specifications Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk In JML, we currently have privacy specified on invariants and constraint clauses, as well as several other clauses such as depends, and represents. For example, package edu.iastate.cs.jml.samples.stacks; //@ model import edu.iastate.cs.jml.models.*; public interface BoundedStackInterface extends BoundedThing { /*@ public model instance JMLObjectSequence theStack @ initially: theStack != null && theStack.isEmpty(); @*/ //@ public depends: size -> theStack; //@ public represents: size <- theStack.length(); //@ public invariant: theStack != null; //@ public invariant redundantly: theStack.length() <= MAX_SIZE; Abhay and I have been looking into what needs to be done to check preconditions at run-time. For this there seems to be a problem with behavioral subtyping, more specifically with specification inheritance. The problem is that a precondition in the superclass may mention private variables, which will not be accessible to the subclass. Although this seems pretty drastic, it seems necessary to change JML to allow the specification of what level of privacy a method specification refers to. The reason for this is that if one thinks about compiling into the source code the precondition checks inherited from the superclass, then one will need access to those variables in the specification that is inherited. This suggests that we can only inherit the "public"and "protected" parts of a specification. (This would include the spec_public and spec_protected variables.) Unfortunately, these are not identified currently. Furthermore, we wish to allow one to specify classes at several levels of abstraction, including specifications that discuss how the protected and private variables are affected by methods. It's inconsistent that we do this currently only for invariants and constraints, besides the need for dealing with specification inheritance properly. Here's an example of the problem: public abstract class Super { private int z; public int f (int y) ; //@ requires: y >= z; // would be illegal with our proposal } public abstract class Subtype extends Super { public int f (int y) { //... } } In the above example, the effective precondition for method f of class Subtype is "y>=z". At run-time, however, method f of class Subtype can not refer to z as z is a private data member of Super. This makes it difficult to check the precondition at run-time. Also, from this example it is clear that the specification given for f in Super is not intended for clients, for the same reason. We're proposing the following: - for lightweight specifications, without any form of behavior keyword, the default privacy will be "public", and this will not be able to be changed at all. That is, you will not be able to attach a privacy specification to a lightweight clause. - For specifications that use behavior keywords, that is that are not lightweight, the privacy must always be explicitly specified. This is because the default in Java, when the privacy specification is omitted,is package protected. - the privacy of a specification limits the variables it can access in the usual way. For example, in a public specification, one can only access public, or spec_public variables. As a first example, one could rewrite the super and subtype example above as follows: public abstract class Super { private int z; public int f (int y) ; /*@ private behavior @ requires: y >= z; @*/ } public abstract class Subtype extends Super { public int f (int y) { //... } } In the above example, the inherited precondition of f in Subtype will be "true". Alternatively, one could declare the variable z to be spec_public as follows: public abstract class Super { /*@ spec_public @*/ private int z; public int f (int y) ; //@ requires: y >= z; } public abstract class Subtype extends Super { public int f (int y) { //... } } As another example, we continue the bounded stack interface example given above. package edu.iastate.cs.jml.samples.stacks; //@ model import edu.iastate.cs.jml.models.*; public interface BoundedStackInterface extends BoundedThing { /*@ public model instance JMLObjectSequence theStack @ initially: theStack != null && theStack.isEmpty(); @*/ //@ public depends: size -> theStack; //@ public represents: size <- theStack.length(); //@ public invariant: theStack != null; //@ public invariant redundantly: theStack.length() <= MAX_SIZE; public void pop( ) throws BoundedStackException; /*@ public normal_behavior @ requires: !theStack.isEmpty(); @ modifiable: size, theStack; @ ensures: theStack.equals(\old(theStack.trailer())); @ also @ public exceptional_behavior @ requires: theStack.isEmpty(); @ signals: (BoundedStackException); @*/ public void push(Object x ) throws BoundedStackException; /*@ public normal_behavior @ requires: theStack.length() < MAX_SIZE; @ modifiable: size, theStack; @ ensures: theStack.equals(\old(theStack.insertFront(x))); @ ensures redundantly: theStack != null && top() == x @ && theStack.length() == \old(theStack.length()+1); @ also @ public exceptional_behavior @ requires: theStack.length() == MAX_SIZE; @ signals: (BoundedStackException); @*/ public /*@ pure @*/ Object top( ) throws BoundedStackException; /*@ public normal_behavior @ requires: !theStack.isEmpty(); @ ensures: \result == theStack.first(); @ also @ public exceptional_behavior @ requires: theStack.isEmpty(); @ signals: (BoundedStackException); @*/ } Clearly this is an incompatible change to JML, so we are interested in hearing what everyone thinks about this, before we adopt it. Is there some way to avoid it? Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Tue Jan 25 11:34:35 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id LAA08395 for jml-interest-list-outgoing; Tue, 25 Jan 2000 11:34:15 -0600 (CST) Received: from cicero.cs.kun.nl (cicero.cs.kun.nl [131.174.33.247]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id LAA08391 for ; Tue, 25 Jan 2000 11:34:13 -0600 (CST) Received: from localhost (joachim@localhost) by cicero.cs.kun.nl (8.9.3/8.9.3) with ESMTP id SAA01001 for ; Tue, 25 Jan 2000 18:34:10 +0100 Date: Tue, 25 Jan 2000 18:34:10 +0100 (CET) From: Joachim van den Berg To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: thoughts on static fields, and the new operator Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Tue, 25 Jan 2000 18:34:10 +0100 (CET) From: Joachim van den Berg To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: thoughts on static fields, and the new operator Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, I have been working on the formalisation of the semantics of JML and this formalisation gave rise to some questions I would like to share with you. The page numbers I mention in this email refer to pages of the Preliminary Design document, version 'h'. 1. Is it possible to refer to a static (non-model) fields within an invariant? My guess is, according to the definition of 'visible states' on page 9, this is not allowed. If it is allowed to refer to static fields, it seems to me that it is very hard to show that an invariant holds again after changing a static field.... 2. Several JML declarations (e.g. invariant and constraint) have three access modifiers: public, protected, and private. For me it is clear what private means in the setting of JML, but what's the difference between the 'public' and 'protected' modifiers? Should it be possible to refer to invariants from another class? In my opinion, the public modifier is redundant because an invariant is visible in the class in which it is declared, and in its subclasses, only. 3. JML allows a modeler to write predicates containing the new operator. This new operator allocates storage, but to this storage can never be referred to after evaluation of the predicate. I agree on this. On page 40 it is described that the new operator can be used with pure constructors. This definition is to loose. Consider the example below: class A { static int i = B.j = 2; /*@ pure @*/ static int get_i() { return i; } } class B { static int j; int k; /*@ pure @*/ B (int i) { k = i; } /*@ pure @*/ int get_jk() { return j + k; } } According to the definitions of pure method and pure constructor on page 19, the methods get_i and get_jk and the constructor of B are pure indeed. A modeler can write a predicate like (new B(1)).get_jk() == 1 & (new A()).get_i() == 2 This predicate satisfies the requirements as described on page 40. Moreover, this predicate yields true in a state X. A modeler can also write a predicate where the conjuncts are swapped : (new A()).get_i() == 2 & (new B(1)).get_jk() == 1 Suddenly this predicate yields false in the same state X. As one can see, these static fields mess up the things. Therefore, I would suggest that the new operator can only be used with a constructor of a pure class. The definition of a pure class should also be strengthened: a pure class may not contain static fields. This also has an implication for interfaces: they may not contain fields at all (fields of interfaces are implicitly declared static). Any thoughts on these topics are appreciated! Bye, Joachim  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Wed Jan 26 07:24:16 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id HAA25690 for jml-interest-list-outgoing; Wed, 26 Jan 2000 07:23:58 -0600 (CST) Received: from pandora.cs.kun.nl (pandora.cs.kun.nl [131.174.33.4]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id HAA25686 for ; Wed, 26 Jan 2000 07:23:56 -0600 (CST) Received: from hera.cs.kun.nl by pandora.cs.kun.nl via hera.cs.kun.nl [131.174.33.2] with ESMTP for id OAA03259 (8.8.8/3.12); Wed, 26 Jan 2000 14:23:54 +0100 (MET) Date: Wed, 26 Jan 2000 14:23:54 +0100 (MET) From: Erik Poll To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: Re: privacy of method specifications In-Reply-To: <200001242054.OAA14416@larch.cs.iastate.edu> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Wed, 26 Jan 2000 14:23:54 +0100 (MET) From: Erik Poll To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: Re: privacy of method specifications In-Reply-To: <200001242054.OAA14416@larch.cs.iastate.edu> Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi all, Gary's latest email raised a lot of questions for me. Basically, I have been wondering whether this suggestion to only inherit "public" and "protected" behaviour does not conflict with the idea of behavioural subtyping. Shouldn't we inherit ALL behaviors, invariants, and constraints, irrespective of whether they're private or public, in order to ensure behavioural subtyping ? But then, what the point of having the 'private' and 'public' qualifiers for behaviors, invariants, and constraint ? Maybe I'm missing something here. I must say that I never really thought about the meaning of "private" invariant" as opposed to "public invariant" till now. I don't think anything is explained about this distinction in the JML paper, but please correct me if I'm wrong. I expand on this below, Erik Consider public abstract class Super { private int z; public int f (int y) ; /*@ private behavior @ requires: y >= z; @ ensures: z = y @*/ } public abstract class Subtype extends Super { public int f (int y) { //... } Following Gary suggestion, the class Subtype would not inherit the specification of f given in Super. But there is a good reason for saying that f in Subtype should still meet this spec, even though this spec refers to the private field z which is no longer directly accessible. After all, the usual argument for behavioural subtyping still applies: if methods in Super invoke method f, then by late binding this may result in the execution of f as defined in Subtype; so this definition of f in Subtype should still meet the spec given in Super For example, if we define public abstract class Subtype extends Super { public int f (int y) { super.f(-99); } then Subtype is not a behavioural subtype of Super. (Even though the field z is not directly accessible in Subtype, the field _does_ exists, i.e. every object of class Subtype has a z field, and we can still get at this field via the inherited methods of the Super class.) So, I think that in order to get behavioural subtyping we should inherit ALL behaviour, even if it concerns private fields. Some further points: (i) Clearly it is impossible to add precondition checks to the code for inherited preconditions that refer to private fields, as Abhay and Gary noted. But I don't think we should discard the idea of behavioural subtyping to make this possible. Instead, I think we should accept that these checks cannot be added for such inherited preconditions. (There is still the danger that at some point we may need some syntax to refer to private fields of superclasses ... ) (ii) Of course referring to private fields in preconditions is a bit strange anyway if such preconditions are meant as obligations to a client invoking the method, as these clients are not meant to know about the existence of private fields. So maybe the restriction on adding run-time checks is not too bad. The argument about behavioural subtyping also applies to invariants and constraints: Don't subclasses have to inherit private invariants and constraints just as well as public ones, in order to ensure behavioural subtyping ? But then, what's the point of having the qualifiers 'private' and 'public' at all for behaviors, invariants, and constraints ? - Note that if an invariant only refers to private fields it is not possible to disturb this invariant in subclass. After all, the only way to alter the private fields is by invoking super methods, and all super methods leave the invariant intact if their preconditions are met. So, whether or not we say these private invariants are inherited doesn't really matter. But the same does not hold for all constraints: e.g. we can easily break a private constraint "z=\old(z)+1" in a subclass by doing two method invocations of super methods, after which z=\old(z)+2.  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Wed Jan 26 11:52:49 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id LAA01198 for jml-interest-list-outgoing; Wed, 26 Jan 2000 11:51:27 -0600 (CST) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id LAA01193; Wed, 26 Jan 2000 11:51:18 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id LAA08664; Wed, 26 Jan 2000 11:51:13 -0600 (CST) Date: Wed, 26 Jan 2000 11:51:13 -0600 (CST) Message-Id: <200001261751.LAA08664@larch.cs.iastate.edu> From: "Gary T. Leavens" To: erikpoll@cs.kun.nl CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Wed, 26 Jan 2000 14:23:54 +0100 (MET)) Subject: Re: JML-Interest: Re: privacy of method specifications References: Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Wed, 26 Jan 2000 11:51:13 -0600 (CST) From: "Gary T. Leavens" To: erikpoll@cs.kun.nl CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Wed, 26 Jan 2000 14:23:54 +0100 (MET)) Subject: Re: JML-Interest: Re: privacy of method specifications Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Erik, > Date: Wed, 26 Jan 2000 14:23:54 +0100 (MET) > From: Erik Poll > > Gary's latest email raised a lot of questions for me. Basically, > I have been wondering whether this suggestion to only inherit > "public" and "protected" behaviour does not conflict with the > idea of behavioural subtyping. > > Shouldn't we inherit ALL behaviors, invariants, and constraints, > irrespective of whether they're private or public, in order to > ensure behavioural subtyping ? I think that only the behavior visible to clients should matter for behavioral subtyping. Of course, it is up to us to decide what part of the specification determines that behavior. > But then, what [is] the point of having the 'private' and 'public' > qualifiers for behaviors, invariants, and constraint ? Part of the point of having these qualifiers is to be able to specify at several levels of abstraction. In particular, we would like to be able to specify a class describing the behavior visible to clients, to subclasses, to other classes in the same package, and to the rest of the implementation of that class. This describes the same set of levels as the privacy qualifiers in Java. I think it would be strange to have the private variables of a class be directly part of the client-visible behavior of that class, without some other indication (such as spec_public) On the part of the specification that that is what is intended. Another, more mundane, reason for doing this, is to make it possible to do type checking. It would seem unreasonable for the private variables of a superclass to be involved in the invariant of a subclass. (Again, without some other indication, such as spec_public.) > ... I don't think anything is explained > about this distinction in the JML paper, but please correct me > if I'm wrong. That is correct. > Consider > > public abstract class Super { > private int z; > > public int f (int y) ; > /*@ private behavior > @ requires: y >= z; > @ ensures: z = y > @*/ > } > > public abstract class Subtype extends Super { > public int f (int y) { > //... > } > > Following Gary suggestion, the class Subtype would not inherit the > specification of f given in Super. > > But there is a good reason for saying that f in Subtype should still meet > this spec, even though this spec refers to the private field z which is > no longer directly accessible. After all, the usual argument for > behavioural subtyping still applies: > > if methods in Super invoke method f, then by late binding this may > result in the execution of f as defined in Subtype; so this definition > of f in Subtype should still meet the spec given in Super > > For example, if we define > > public abstract class Subtype extends Super { > public int f (int y) { > super.f(-99); > } > > then Subtype is not a behavioural subtype of Super. > (Even though the field z is not directly accessible in Subtype, the field > _does_ exists, i.e. every object of class Subtype has a z field, and we > can still get at this field via the inherited methods of the Super class.) > > So, I think that in order to get behavioural subtyping we should inherit > ALL behaviour, even if it concerns private fields. This is a good example for bringing out the issues. As you point out below... > (ii) Of course referring to private fields in preconditions is a bit > strange anyway if such preconditions are meant as obligations to a > client invoking the method, as these clients are not meant to know > about the existence of private fields. ... it is not clear what such a specification can mean to clients. If we have in our code something like the following: Super s; /* ... */ s.f(0); how do we know whether this call to the method "f" satisfies the precondition? One way of looking at this, is that if only a private specification is given, then there are no constraints at all, and no guarantees given to the client. I think that this might argue for explicitly distinguishing between the various privacy levels in specifications. One could argue that it would make it clear to both the specifier and the reader what parts of the specification are intended for each audience (clients, subclasses, other classes in the same package, and the implementation). One way to "fix" the above example would be to declare the instance variable (field) z as spec_public. Perhaps a better way would be to declare a public method, that gives access to this information. Then one could write the specification as follows. public abstract class Super { /*@ spec_public @*/ private int z; public int state() /*@ public normal_behavior @ ensures: \result == z; @*/ public abstract int f (int y) ; /*@ public normal_behavior @ requires: y >= state(); @ ensures: state() == y; @ implies_that @ private normal_behavior @ requires: y >= z; @ ensures: z == y; @*/ } > - Note that if an invariant only refers to private fields it is not > possible to disturb this invariant in subclass. After all, the only > way to alter the private fields is by invoking super methods, and all > super methods leave the invariant intact if their preconditions are met. > So, whether or not we say these private invariants are inherited > doesn't really matter. That seems reasonable. > But the same does not hold for all constraints: e.g. we can easily break > a private constraint "z=\old(z)+1" in a subclass by doing two method > invocations of super methods, after which z=\old(z)+2. The history constraint that you have given is not really well-formed. A history constraint is supposed to be satisfied by all pairs of visible states, containing an earlier state and a later state. This history constraint would certainly be violated by the client also invoking a method twice. Other discussion? Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Wed Jan 26 12:12:48 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id MAA01696 for jml-interest-list-outgoing; Wed, 26 Jan 2000 12:12:46 -0600 (CST) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id MAA01690; Wed, 26 Jan 2000 12:12:42 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id MAA08973; Wed, 26 Jan 2000 12:12:37 -0600 (CST) Date: Wed, 26 Jan 2000 12:12:37 -0600 (CST) Message-Id: <200001261812.MAA08973@larch.cs.iastate.edu> From: "Gary T. Leavens" To: joachim@cicero.cs.kun.nl CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: (message from Joachim van den Berg on Tue, 25 Jan 2000 18:34:10 +0100 (CET)) Subject: Re: JML-Interest: thoughts on static fields, and the new operator References: Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Wed, 26 Jan 2000 12:12:37 -0600 (CST) From: "Gary T. Leavens" To: joachim@cicero.cs.kun.nl CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: (message from Joachim van den Berg on Tue, 25 Jan 2000 18:34:10 +0100 (CET)) Subject: Re: JML-Interest: thoughts on static fields, and the new operator Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Joachim, > Date: Tue, 25 Jan 2000 18:34:10 +0100 (CET) > From: Joachim van den Berg > > I have been working on the formalisation of the semantics of JML and this > formalisation gave rise to some questions I would like to share with you. > The page numbers I mention in this email refer to pages of the Preliminary > Design document, version 'h'. > > > 1. Is it possible to refer to a static (non-model) fields within an invariant? > My guess is, according to the definition of 'visible states' on page 9, > this is not allowed. If it is allowed to refer to static fields, > it seems to me that it is very hard to show that an invariant holds > again after changing a static field.... Generally, I think that we should adopt the same scope rules as in Java. This will help prevent confusion on the part of users of JML. With that in mind, I think that in invariants (and history constraints) should be allowed to refer to static fields of an enclosing class. The question of whether an invariant that refers to a non-final static field can actually be shown to be an invariant (or how difficult that will be) is outside the scope of the language design. Certainly it is easy to state invariants that are not satisfiable. (False comes to mind.) This is an interesting question for programming methodology however. > 2. Several JML declarations (e.g. invariant and constraint) have three access > modifiers: public, protected, and private. For me it is clear what private > means in the setting of JML, but what's the difference between the 'public' > and 'protected' modifiers? Should it be possible to refer to invariants > from another class? > In my opinion, the public modifier is redundant because an invariant is > visible in the class in which it is declared, and in its subclasses, only. We have been having some discussion of this in other e-mails. In a narrow sense these privacy qualifiers are used in type checking. A public invariant, cannot refer to non-public fields or methods. A protected invariant can only refer to public and protected fields or methods. An invariant that has package protection, by virtue of having no privacy qualifier, can refer to public and protected attributes as well as all attributes in the same package. A private invariant has no access restrictions. Although we might wish that the default privacy qualifier was "public", that is not the case in Java. I think it would be foolish for JML to use a default that is different than Java's. > 3. JML allows a modeler to write predicates containing the new operator. This > new operator allocates storage, but to this storage can never be referred > to after evaluation of the predicate. I agree on this. > On page 40 it is described that the new operator can be used with pure > constructors. This definition is to loose. Consider the example below: > > class A { > static int i = B.j = 2; > /*@ pure @*/ static int get_i() { return i; } > } > > class B { > static int j; > int k; > /*@ pure @*/ B (int i) { k = i; } > /*@ pure @*/ int get_jk() { return j + k; } > } We are assuming, I think, that these classes are in the same package. > According to the definitions of pure method and pure constructor on > page 19, the methods get_i and get_jk and the constructor of B are pure > indeed. Yes. > A modeler can write a predicate like > > (new B(1)).get_jk() == 1 & (new A()).get_i() == 2 > > This predicate satisfies the requirements as described on page 40. > Moreover, this predicate yields true in a state X. > A modeler can also write a predicate where the conjuncts are swapped : > > (new A()).get_i() == 2 & (new B(1)).get_jk() == 1 > > Suddenly this predicate yields false in the same state X. > As one can see, these static fields mess up the things. > > Therefore, I would suggest that the new operator can only be used with a > constructor of a pure class. The definition of a pure class should also be > strengthened: a pure class may not contain static fields. This also has an > implication for interfaces: they may not contain fields at all (fields of > interfaces are implicitly declared static). I'm not sure we have to go that far. I would think that we could get away with somehow limiting the static initializers. But I'm not sure yet how to do that. Any ideas? We certainly do want to allow interfaces to contain fields, especially non-static fields. This is the idea behind the "instance" attribute in JML. The use of model instance variables in interfaces is critical for giving abstract models of the data described by an interface. Note that the static data in an interface is implicitly declared final, I believe, in Java. Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Fri Jan 28 16:57:07 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id QAA00748 for jml-interest-list-outgoing; Fri, 28 Jan 2000 16:56:53 -0600 (CST) Received: from oak.fernuni-hagen.de (oak.fernuni-hagen.de [132.176.114.41]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id QAA00744 for ; Fri, 28 Jan 2000 16:56:50 -0600 (CST) Received: from sunpoet1.fernuni-hagen.de by oak.fernuni-hagen.de via local-channel with ESMTP; Fri, 28 Jan 2000 23:56:35 +0100 Received: (from mueller@localhost) by sunpoet1.fernuni-hagen.de (8.9.3+Sun/8.9.1) id XAA22240; Fri, 28 Jan 2000 23:55:38 +0100 (MET) Date: Fri, 28 Jan 2000 23:55:38 +0100 (MET) Message-Id: <200001282255.XAA22240@sunpoet1.fernuni-hagen.de> X-Authentication-Warning: sunpoet1.fernuni-hagen.de: mueller set sender to Peter.Mueller@fernuni-hagen.de using -f From: Peter Mueller MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: private specifications X-Mailer: VM 6.32 under Emacs 20.3.1 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Fri, 28 Jan 2000 23:55:38 +0100 (MET) X-Authentication-Warning: sunpoet1.fernuni-hagen.de: mueller set sender to Peter.Mueller@fernuni-hagen.de using -f From: Peter Mueller Content-Type: text/plain; charset=us-ascii To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: private specifications Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi all, > Gary's latest email raised a lot of questions for me. Basically, > I have been wondering whether this suggestion to only inherit > "public" and "protected" behavior does not conflict with the > idea of behavioral subtyping. > > Shouldn't we inherit ALL behaviors, invariants, and constraints, > irrespective of whether they're private or public, in order to > ensure behavioral subtyping ? > > But then, what the point of having the 'private' and 'public' > qualifiers for behaviors, invariants, and constraint ? Here are some of my thoughts about this topic. Let's first talk about pre-post-pairs. I think, to understand the issue, we have to take a software engineering point of view: Why does a programmer use private pre-post-specifications? I'd say, the intention of writing down private specifications is not to describe properties of a dynamically bound method. A programmer would do that in public specifications in an abstract way. The purpose of a private pre-post-pair is rather to describe some additional property of one specific *implementation* of the method. In other words, a method m1 and a method m2 overriding m1 can have the same abstract behavior, described in non-private pre-post-pairs. However, m1 might achieve this behavior in a different way than m2. So it could be reasonable to provide this additional information in private pre-post-pairs. So somebody who has access to the code (and therefore to private specifications) can use the additional information. Technically, this means that the semantics of private pre-post-pairs is different from protected or public ones. Say that a non-private pre-post-pair leads to the following proof obligation stated in Hoare logic: { R /\ P } method m { Q } where (P,Q) is the pre-post pair and R gives additional information, e.g. about typing, invariants, etc. The private pre-post-pair of method T.m would be translated into: { typeof(this) = T /\ R /\ P } method m { Q } This triple is automatically fulfilled by overriding methods, since typeof(this)=T is always false for such methods. For default-access specifications, one would have to include all subtypes of T in the package to which T belongs, e.g. { ( typeof(this) = T \/ typeof(this) = S) /\ R /\ P } method m { Q } > Maybe I'm missing something here. I must say that I never really > thought about the meaning of "private" invariant" as opposed to > "public invariant" till now. I don't think anything is explained > about this distinction in the JML paper, but please correct me > if I'm wrong. The situation for invariants is different from pre-post-pairs, since their semantics is different. I assume here the following semantics of an invariant, which is (as far as I know) used in JML: The invariant has to be established/preserved for all allocated objects of appropriate types by all non-private methods *of the program* (not just of the type that contains the invariant declaration and its subtypes). Unfortunately, I'm not too familiar with JML. However, I assume that JML uses depends-clauses also for invariants (as suggested by Rustan Leino's or my work). So proving that a method preserves an invariant entails two aspects: 1. One has to prove for every field update that the invariant (a) does not depend on that field or (b) is not modified by that particular update. So if an invariant is private, (b) might be impossible to show. So one has to take care that code that can modify a dependency of a private invariant has access to the invariants representation. In other words, private invariants should only depend on private fields (and accordingly for other access modifiers). Thus, private invariants and behavioral subtyping are no problem here. > - Note that if an invariant only refers to private fields it is not > possible to disturb this invariant in subclass. After all, the only > way to alter the private fields is by invoking super methods, and all > super methods leave the invariant intact if their preconditions are met. > So, whether or not we say these private invariants are inherited > doesn't really matter. That's exactly what I tried to explain above and shows that even in the absence of dependencies for invariants, private invariants can be restricted appropriately. > But the same does not hold for all constraints: e.g. we can easily break > a private constraint "z=\old(z)+1" in a subclass by doing two method > invocations of super methods, after which z=\old(z)+2. I though that history constraints are transitive predicates on states. So this example is not well-formed. I have not deeply thought about history constraints so far, but I have the impression that the restrictions for invariants would also be appropriate for constraints. Gary wrote: > One way to "fix" the above example would be to declare the instance > variable (field) z as spec_public. I would not recommend to introduce something like spec_public. As I understand access modes, they provide information hiding (besides encapsulation). In other words, they give an answer to the question "Whom do I have to inform when I change a program element with access mode X?" Using spec_public gives up information hiding (although it preserves encapsulation). This is illustrated in the example: public abstract class Super { /*@ spec_public @*/ private int z; public int state() /*@ public normal_behavior @ ensures: \result == z; @*/ public abstract int f (int y) ; /*@ public normal_behavior @ requires: y >= state(); @ ensures: state() == y; @ implies_that @ private normal_behavior @ requires: y >= z; @ ensures: z == y; @*/ } If the implementor of Super would like to use another private implementation (or e.g. just rename z to zz), he would have to inform all other classes (resp. their developers) that something has changed, which I find quite strange. Peter _/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/ _/ Peter Mueller _/ _/ Fernuniversitaet Hagen, Lehrgebiet Praktische Informatik V _/ _/ 58084 Hagen, Feithstr. 142, Raum 1.F13 _/ _/ _/ _/ Tel: 02331-987 4870 _/ _/ Fax: 02331-987 4487 _/ _/ E-Mail: peter.mueller@fernuni-hagen.de _/ _/ WWW: www.informatik.fernuni-hagen.de/pi5/mueller.html _/ _/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Mon Jan 31 11:38:54 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id LAA21378 for jml-interest-list-outgoing; Mon, 31 Jan 2000 11:38:39 -0600 (CST) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id LAA21373; Mon, 31 Jan 2000 11:38:23 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id LAA27748; Mon, 31 Jan 2000 11:38:17 -0600 (CST) Date: Mon, 31 Jan 2000 11:38:17 -0600 (CST) Message-Id: <200001311738.LAA27748@larch.cs.iastate.edu> From: "Gary T. Leavens" To: Peter.Mueller@FernUni-Hagen.de CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: <200001282255.XAA22240@sunpoet1.fernuni-hagen.de> (message from Peter Mueller on Fri, 28 Jan 2000 23:55:38 +0100 (MET)) Subject: Re: JML-Interest: private specifications References: <200001282255.XAA22240@sunpoet1.fernuni-hagen.de> Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Mon, 31 Jan 2000 11:38:17 -0600 (CST) From: "Gary T. Leavens" To: Peter.Mueller@FernUni-Hagen.de CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: <200001282255.XAA22240@sunpoet1.fernuni-hagen.de> (message from Peter Mueller on Fri, 28 Jan 2000 23:55:38 +0100 (MET)) Subject: Re: JML-Interest: private specifications Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Peter, et al., > Date: Fri, 28 Jan 2000 23:55:38 +0100 (MET) > From: Peter Mueller > > Here are some of my thoughts about this topic. Let's first talk about > pre-post-pairs. I think, to understand the issue, we have to take a software > engineering point of view: Why does a programmer use private > pre-post-specifications? I'd say, the intention of writing down private > specifications is not to describe properties of a dynamically bound method. > A programmer would do that in public specifications in an abstract way. The > purpose of a private pre-post-pair is rather to describe some additional > property of one specific *implementation* of the method. > > In other words, a method m1 and a method m2 overriding m1 can have the same > abstract behavior, described in non-private pre-post-pairs. However, m1 might > achieve this behavior in a different way than m2. So it could be reasonable to > provide this additional information in private pre-post-pairs. So > somebody who > has access to the code (and therefore to private specifications) can use the > additional information. Yes, I agree with that. > Technically, this means that the semantics of private pre-post-pairs is > different from protected or public ones. Say that a non-private pre-post-pair > leads to the following proof obligation stated in Hoare logic: > { R /\ P } method m { Q } > where (P,Q) is the pre-post pair and R gives additional information, > e.g. about typing, invariants, etc. > The private pre-post-pair of method T.m would be translated into: > { typeof(this) = T /\ R /\ P } method m { Q } > This triple is automatically fulfilled by overriding methods, since > typeof(this)=T is always false for such methods. That is an interesting way of looking at it. It seems like it might be a suitable semantics. > For default-access specifications, one would have to include all subtypes of T > in the package to which T belongs, e.g. > { ( typeof(this) = T \/ typeof(this) = S) /\ R /\ P } method m { Q } Perhaps the logic will need some way to express the property of being in the same package. I don't think that other subtypes of the classes that are in the same package also get this access do they? > > Maybe I'm missing something here. I must say that I never really > > thought about the meaning of "private" invariant" as opposed to > > "public invariant" till now. I don't think anything is explained > > about this distinction in the JML paper, but please correct me > > if I'm wrong. > > The situation for invariants is different from pre-post-pairs, since their > semantics is different. I assume here the following semantics of an invariant, > which is (as far as I know) used in JML: The invariant has to be > established/preserved for all allocated objects of appropriate types by all > non-private methods *of the program* (not just of the type that contains the > invariant declaration and its subtypes). > > Unfortunately, I'm not too familiar with JML. However, I assume that JML uses > depends-clauses also for invariants (as suggested by Rustan Leino's or my > work). Yes it does. > So proving that a method preserves an invariant entails two aspects: > 1. One has to prove for every field update that the invariant (a) does not > depend on that field or (b) is not modified by that particular update. So if > an invariant is private, (b) might be impossible to show. So one has to take > care that code that can modify a dependency of a private invariant has access > to the invariant's representation. In other words, private invariants should > only depend on private fields (and accordingly for other access > modifiers). Thus, private invariants and behavioral subtyping are no problem > here. > > > - Note that if an invariant only refers to private fields it is not > > possible to disturb this invariant in subclass. After all, the only > > way to alter the private fields is by invoking super methods, and all > > super methods leave the invariant intact if their preconditions are met. > > So, whether or not we say these private invariants are inherited > > doesn't really matter. > > That's exactly what I tried to explain above and shows that even in the > absence of dependencies for invariants, private invariants can be restricted > appropriately. All of this seems reasonable. > > Gary wrote: > > > One way to "fix" the above example would be to declare the instance > > variable (field) z as spec_public. > > I would not recommend to introduce something like spec_public. As I understand > access modes, they provide information hiding (besides encapsulation). In > other words, they give an answer to the question "Whom do I have to inform > when I change a program element with access mode X?" Using spec_public gives > up information hiding (although it preserves encapsulation). This is > illustrated in the example: > > public abstract class Super { > /*@ spec_public @*/ private int z; > > public int state() > /*@ public normal_behavior > @ ensures: \result == z; > @*/ > > public abstract int f (int y) ; > /*@ public normal_behavior > @ requires: y >= state(); > @ ensures: state() == y; > @ implies_that > @ private normal_behavior > @ requires: y >= z; > @ ensures: z == y; > @*/ > } > > If the implementor of Super would like to use another private implementation > (or e.g. just rename z to zz), he would have to inform all other classes > (resp. their developers) that something has changed, which I find quite > strange. The spec_public feature is adapted (stolen) from ESC/Java. I view it as a syntactic sugar for a more complicated set of declarations. Taking the example above, we can desugar it into the following. public abstract class Super { /*@ public model int z; @*/ private int z_priv; // this name has to be fresh /*@ depends z -> z_priv; @*/ /*@ represents z <- z_priv; @*/ public int state(); /*@ public normal_behavior @ ensures: \result == z; @*/ public abstract int f (int y) ; /*@ public normal_behavior @ requires: y >= state(); @ ensures: state() == y; @ implies_that @ private normal_behavior @ requires: y >= z_priv; @ ensures: z_priv == y; @*/ } Surely there cannot be any objection to such a specification. Can there? :-) Of course, we need to write down these desugarings. Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Tue Feb 1 05:43:56 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id FAA10874 for jml-interest-list-outgoing; Tue, 1 Feb 2000 05:43:40 -0600 (CST) Received: from oak.fernuni-hagen.de (oak.fernuni-hagen.de [132.176.114.41]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id FAA10869; Tue, 1 Feb 2000 05:43:36 -0600 (CST) Received: from sunpoet1.fernuni-hagen.de by oak.fernuni-hagen.de via local-channel with ESMTP; Tue, 1 Feb 2000 12:43:31 +0100 Received: (from mueller@localhost) by sunpoet1.fernuni-hagen.de (8.9.3+Sun/8.9.1) id MAA25655; Tue, 1 Feb 2000 12:42:30 +0100 (MET) Date: Tue, 1 Feb 2000 12:42:30 +0100 (MET) Message-Id: <200002011142.MAA25655@sunpoet1.fernuni-hagen.de> X-Authentication-Warning: sunpoet1.fernuni-hagen.de: mueller set sender to Peter.Mueller@fernuni-hagen.de using -f From: Peter Mueller MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit To: "Gary T. Leavens" Cc: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: private specifications In-Reply-To: <200001311738.LAA27748@larch.cs.iastate.edu> References: <200001282255.XAA22240@sunpoet1.fernuni-hagen.de> <200001311738.LAA27748@larch.cs.iastate.edu> X-Mailer: VM 6.32 under Emacs 20.3.1 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Tue, 1 Feb 2000 12:42:30 +0100 (MET) X-Authentication-Warning: sunpoet1.fernuni-hagen.de: mueller set sender to Peter.Mueller@fernuni-hagen.de using -f From: Peter Mueller Content-Type: text/plain; charset=us-ascii To: "Gary T. Leavens" Cc: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: private specifications In-Reply-To: <200001311738.LAA27748@larch.cs.iastate.edu> Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi again, > > For default-access specifications, one would have to include all subtypes of T > > in the package to which T belongs, e.g. > > { ( typeof(this) = T \/ typeof(this) = S) /\ R /\ P } method m { Q } > > Perhaps the logic will need some way to express the property of being in > the same package. That depends. In our system, a proof obligation like the one above would be generated. Thus, only the component that generates the proof obligations needs to know which types belong to which package. We don't have to refer to packages in the logic. > I don't think that other subtypes of the classes that > are in the same package also get this access do they? No, the access rights are just like in Java. > The spec_public feature is adapted (stolen) from ESC/Java. I view it as > a syntactic sugar for a more complicated set of declarations. Taking > the example above, we can desugar it into the following. > > public abstract class Super { > /*@ public model int z; @*/ > private int z_priv; // this name has to be fresh > /*@ depends z -> z_priv; @*/ > /*@ represents z <- z_priv; @*/ > > public int state(); > /*@ public normal_behavior > @ ensures: \result == z; > @*/ > > public abstract int f (int y) ; > /*@ public normal_behavior > @ requires: y >= state(); > @ ensures: state() == y; > @ implies_that > @ private normal_behavior > @ requires: y >= z_priv; > @ ensures: z_priv == y; > @*/ > } > > Surely there cannot be any objection to such a specification. Can > there? :-) That's also what I have thought of. Of course that's fine because if one wants e.g. to rename z_priv into xyz, it would be sufficient to modify the represents-clause (which should be private since it refers to a private field) and private pre-post-pairs. Peter _/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/ _/ Peter Mueller _/ _/ Fernuniversitaet Hagen, Lehrgebiet Praktische Informatik V _/ _/ 58084 Hagen, Feithstr. 142, Raum 1.F13 _/ _/ _/ _/ Tel: 02331-987 4870 _/ _/ Fax: 02331-987 4487 _/ _/ E-Mail: peter.mueller@fernuni-hagen.de _/ _/ WWW: www.informatik.fernuni-hagen.de/pi5/mueller.html _/ _/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Fri Feb 4 10:17:07 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id KAA27076 for jml-interest-list-outgoing; Fri, 4 Feb 2000 10:16:45 -0600 (CST) Received: from pandora.cs.kun.nl (pandora.cs.kun.nl [131.174.33.4]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id KAA27072 for ; Fri, 4 Feb 2000 10:16:42 -0600 (CST) Received: from hera.cs.kun.nl by pandora.cs.kun.nl via hera.cs.kun.nl [131.174.33.2] with ESMTP for id RAA20204 (8.8.8/3.12); Fri, 4 Feb 2000 17:16:40 +0100 (MET) Date: Fri, 4 Feb 2000 17:16:40 +0100 (MET) From: Erik Poll To: jml-interest@cs.iastate.edu Subject: JML-Interest: normal behavior with only a requires clause ? Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Fri, 4 Feb 2000 17:16:40 +0100 (MET) From: Erik Poll To: jml-interest@cs.iastate.edu Subject: JML-Interest: normal behavior with only a requires clause ? Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi all, I noticed that it's not possible to write normal_behavior specifications with only a requires clause, i.e. specs of the form //@ normal_behavior //@ requires : ; This means "the method terminates normally if is met", by the conventions about missing clauses. The current grammar for JML insists that a normal_behavior includes an ensures clause or a modifiable clause. It would be nice if specs just giving a precondition were allowed. In very 'light weight' specs such specs are quite common. (Here I use 'light weight' in the general sense, not the more specific JML sense.) In the specs I'm currently writing, specs with only a requires clause are much more common that those with only a ensures clause. The fact that the former are not allowed whereas the latter are seems a bit of an arbitrary choice to me. I don't have very strong feelings about this. (After all, just adding "ensures: true" to the spec above is not really a problem, though it would nice if it could be avoided.) So if allowing specs with only a requires clause really messes up the grammar then I'm happy to do without them. Any comments? Erik  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Fri Feb 4 21:33:24 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id VAA09727 for jml-interest-list-outgoing; Fri, 4 Feb 2000 21:33:19 -0600 (CST) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id VAA09722; Fri, 4 Feb 2000 21:33:15 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id VAA18727; Fri, 4 Feb 2000 21:33:05 -0600 (CST) Date: Fri, 4 Feb 2000 21:33:05 -0600 (CST) Message-Id: <200002050333.VAA18727@larch.cs.iastate.edu> From: "Gary T. Leavens" To: erikpoll@cs.kun.nl CC: jml-interest@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Fri, 4 Feb 2000 17:16:40 +0100 (MET)) Subject: Re: JML-Interest: normal behavior with only a requires clause ? References: Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Fri, 4 Feb 2000 21:33:05 -0600 (CST) From: "Gary T. Leavens" To: erikpoll@cs.kun.nl CC: jml-interest@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Fri, 4 Feb 2000 17:16:40 +0100 (MET)) Subject: Re: JML-Interest: normal behavior with only a requires clause ? Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Erik, > Date: Fri, 4 Feb 2000 17:16:40 +0100 (MET) > From: Erik Poll > > I noticed that it's not possible to write normal_behavior specifications > with only a requires clause, i.e. specs of the form > > //@ normal_behavior > //@ requires : ; > > This means "the method terminates normally if is met", > by the conventions about missing clauses. > The current grammar for JML insists that a normal_behavior includes > an ensures clause or a modifiable clause. You are right. The same also applies to exceptional_behavior clauses. > It would be nice if specs just giving a precondition were allowed. > In very 'light weight' specs such specs are quite common. (Here I use > 'light weight' in the general sense, not the more specific JML sense.) Right, the technically lightweight specifications already allow this kind of grammar. > In the specs I'm currently writing, specs with only a requires clause are > much more common that those with only a ensures clause. The fact that > the former are not allowed whereas the latter are seems a bit of an > arbitrary choice to me. Yes, I agree that this is a good suggestion. I think it makes the language more regular to make the grammatical change you suggest. It also makes the language more in line with ESC/Java. > I don't have very strong feelings about this. (After all, just adding > "ensures: true" to the spec above is not really a problem, though it would > nice if it could be avoided.) So if allowing specs with only a requires > clause really messes up the grammar then I'm happy to do without them. I have tested this grammar change, at least with our LL(k) ANTLR grammar it causes no problems. I also tested it with the new syntax for declaring specification cases to be public, protected, or private. Unless anyone has serious objections to this suggestion then, this will be part of the next release of JML. Thanks for the suggestion! By the way, I will be out of touch most of next week. Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Tue Feb 15 06:54:41 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id GAA16378 for jml-interest-list-outgoing; Tue, 15 Feb 2000 06:54:32 -0600 (CST) Received: from pandora.cs.kun.nl (pandora.cs.kun.nl [131.174.33.4]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id GAA16374 for ; Tue, 15 Feb 2000 06:54:29 -0600 (CST) Received: from hera.cs.kun.nl by pandora.cs.kun.nl via hera.cs.kun.nl [131.174.33.2] with ESMTP for id NAA07827 (8.8.8/3.12); Tue, 15 Feb 2000 13:54:28 +0100 (MET) Message-Id: <200002151254.NAA07827@pandora.cs.kun.nl> X-Mailer: exmh version 2.1.1 10/15/1999 To: jml-interest@cs.iastate.edu Subject: JML-Interest: JavaCard paper + programming jobs Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Tue, 15 Feb 2000 13:54:27 +0100 From: Bart Jacobs Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** To: jml-interest@cs.iastate.edu Subject: JML-Interest: JavaCard paper + programming jobs Content-Type: text/plain; charset=us-ascii Date: Tue, 15 Feb 2000 13:54:27 +0100 From: Bart Jacobs Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, Erik Poll, Joachim van den Berg and I completed a first paper on the (lightweight) use of JML for specificing the JavaCard API. It is available as: http://www.cs.kun.nl/~bart/PAPERS/JavaCardAPI_in_JMLlight.ps.Z If you have comments, please let us know. Probably, our group will temporarily be strengthened by a programmer and a foreign (master) student. They could help in developing tools which facilitate the use of JML (such as adapting javadoc to handle JML, possibly an Emacs mode for JML, ...). I am asking all of you to tell me: * what kind of tools you are developing, or have already developed, for JML (if any), in order to prevent duplication * what suggestions you might have for such tools: what do you think would be really convenient, and would be wanted potential JML users. Best, Bart.  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Tue Feb 15 21:41:35 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id VAA00423 for jml-interest-list-outgoing; Tue, 15 Feb 2000 21:41:31 -0600 (CST) Received: from ren.cs.iastate.edu (leavens@ren.cs.iastate.edu [129.186.3.41]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id VAA00418; Tue, 15 Feb 2000 21:41:27 -0600 (CST) Received: (from leavens@localhost) by ren.cs.iastate.edu (8.9.0/8.9.0) id VAA03081; Tue, 15 Feb 2000 21:41:22 -0600 (CST) Date: Tue, 15 Feb 2000 21:41:22 -0600 (CST) Message-Id: <200002160341.VAA03081@ren.cs.iastate.edu> From: "Gary T. Leavens" To: Bart.Jacobs@cs.kun.nl CC: jml-interest@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: <200002151254.NAA07827@pandora.cs.kun.nl> (message from Bart Jacobs on Tue, 15 Feb 2000 13:54:27 +0100) Subject: Re: JML-Interest: JavaCard paper + programming jobs References: <200002151254.NAA07827@pandora.cs.kun.nl> Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Tue, 15 Feb 2000 21:41:22 -0600 (CST) From: "Gary T. Leavens" To: Bart.Jacobs@cs.kun.nl CC: jml-interest@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: <200002151254.NAA07827@pandora.cs.kun.nl> (message from Bart Jacobs on Tue, 15 Feb 2000 13:54:27 +0100) Subject: Re: JML-Interest: JavaCard paper + programming jobs Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Bart, et al, At ISU, a student Arun Ragahavan is working on a javadoc clone that would take JML and produce web pages. Also Abhay Bhorkar is working on run-time assertion checking of JML specs; this tool would take in JML annotated Java and output Java with extra code to check preconditions. Clyde Ruby is working on a tool to generate subclassing contracts automatically. I would very much like an emacs mode... :-) It's a good idea to coordinate this effort. Gary  1, answered,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Wed Feb 23 17:41:52 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id RAA23187 for jml-interest-list-outgoing; Wed, 23 Feb 2000 17:41:43 -0600 (CST) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id RAA23182; Wed, 23 Feb 2000 17:41:40 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id RAA00855; Wed, 23 Feb 2000 17:41:31 -0600 (CST) Date: Wed, 23 Feb 2000 17:41:31 -0600 (CST) Message-Id: <200002232341.RAA00855@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: <200001140026.SAA01015@larch.cs.iastate.edu> (leavens@cs.iastate.edu) Subject: Re: JML-Interest: defaults for omitted clauses in JML References: <200001140026.SAA01015@larch.cs.iastate.edu> Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Wed, 23 Feb 2000 17:41:31 -0600 (CST) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: <200001140026.SAA01015@larch.cs.iastate.edu> (leavens@cs.iastate.edu) Subject: Re: JML-Interest: defaults for omitted clauses in JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, Picking up this discussion... > Date: Thu, 13 Jan 2000 18:26:37 -0600 (CST) > From: "Gary T. Leavens" > > In our seminar today at Iowa state we discussed the defaults for > omitted clauses in JML. I have written at discussion up into the > following which appears in appendix A of the JML preliminary design > document, which I have updated on the Web (without yet assigning in a > new revision number). I put a copy of that below for your convenience. > Forgive the formatting (this is the info version). > > Gary > > If a specification case does not use one of the > behavior keywords (`behavior', `normal_behavior', or > `exceptional_behavior'), then it is called a "lightweight" > specification. > > When the various clauses of a specification case are omitted, they > have the defaults given in the table below. The table distinguishes > between lightweight and non-lightweight specifications. The only > differences in the defaults are for the `modifiable' and `diverges' > clauses. The idea is that in a lightweight specification, no > assumption is made about the meaning of an omitted clause. However, in > a non-lightweight specification, the specifier is assumed to be giving > a complete specification. Therefore, in a non-lightweight > specification the meaning of an omitted modifiable clause is that > nothing can be modified. Furthermore, in a non-lightweight > specification, the meaning of an omitted diverges clause is that the > method may not diverge in that case. > > ` Default' > `Omitted clause lightweight non-lightweight' > ___________________________________________________ > `requires: true true' > `when: true true' > `measured_by: \not_specified \not_specified' > `modifiable: \not_specified \nothing' > `ensures: true true' > `signals: (Exception) true (Exception) true' > `diverges: true false' > > A completely omitted specification is taken to be a lightweight > specification. Thus one can read off the meaning of a completely > omitted specification from the lightweight column of table. I wonder if also the requires, when, ensures, and diverges clauses should default to \not_specified in the lightweight case. I think that would be sensible for also combinations for specifications that are omitted. This would make the table look like: ` Default' `Omitted clause lightweight non-lightweight' ___________________________________________________ `requires: \not_specified true' `when: \not_specified true' `measured_by: \not_specified \not_specified' `modifiable: \not_specified \nothing' `ensures: \not_specified true' `signals: (Exception) true (Exception) true' `diverges: \not_specified false' Comments? Gary  1, answered,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Wed Feb 23 23:51:18 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id XAA28718 for jml-interest-list-outgoing; Wed, 23 Feb 2000 23:51:14 -0600 (CST) Received: from ren.cs.iastate.edu (leavens@ren.cs.iastate.edu [129.186.3.41]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id XAA28713; Wed, 23 Feb 2000 23:51:10 -0600 (CST) Received: (from leavens@localhost) by ren.cs.iastate.edu (8.9.0/8.9.0) id XAA23608; Wed, 23 Feb 2000 23:51:05 -0600 (CST) Date: Wed, 23 Feb 2000 23:51:05 -0600 (CST) Message-Id: <200002240551.XAA23608@ren.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: Re: private specifications, syntax Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Wed, 23 Feb 2000 23:51:05 -0600 (CST) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: Re: private specifications, syntax Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, In previous emails we have discussed the desirability of labeling method specifications (i.e., behavior clauses) with a privacy (visibility) annotation. For the syntax, our original thought was to allow one of the modifiers public, private, or protected in front of the keywords behavior, normal_behavior, exceptional_behavior, and model_program. Unfortunately, that leads to a nasty shift/reduce conflict in a LALR(1) grammar. The alternatives are not wonderful, and we think the most acceptable is to use underbars to connect the modifiers to the other keywords, forming long keywords like public_normal_behavior, protected_normal_behavior, etc. For example, one would write: public abstract class Super { /*@ spec_public @*/ private int z; public int state() /*@ public_normal_behavior @ ensures: \result == z; @*/ public abstract int f (int y) ; /*@ public_normal_behavior @ requires: y >= state(); @ ensures: state() == y; @ implies_that @ private_normal_behavior @ requires: y >= z; @ ensures: z == y; @*/ } I should hasten to add that lightweight specifications would be unaffected; they would implicitly be "public", since that seems to be the most common desire (and matches ESC/Java). Two possible problems: 1. The defaults (public for lightweight and package visible otherwise) are potentially confusing and may be seen as inconsistent. 2. The keywords are long and potentially error-prone. However, I don't think they look bad, and they seem to convey the intended meaning clearly (to me). They are also somewhat consistent with other JML keywords (e.g. normal_behavior). Barring strenuous objections or better ideas, I think we should adopt this syntax in JML. Comments, better ideas? Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Mon Feb 28 18:26:08 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id SAA12771 for jml-interest-list-outgoing; Mon, 28 Feb 2000 18:26:02 -0600 (CST) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id SAA12759; Mon, 28 Feb 2000 18:25:57 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id SAA23804; Mon, 28 Feb 2000 18:25:48 -0600 (CST) Date: Mon, 28 Feb 2000 18:25:48 -0600 (CST) Message-Id: <200002290025.SAA23804@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu In-reply-to: <200002240551.XAA23608@ren.cs.iastate.edu> (leavens@cs.iastate.edu) Subject: Re: JML-Interest: Re: private specifications, syntax References: <200002240551.XAA23608@ren.cs.iastate.edu> Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Mon, 28 Feb 2000 18:25:48 -0600 (CST) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu In-reply-to: <200002240551.XAA23608@ren.cs.iastate.edu> (leavens@cs.iastate.edu) Subject: Re: JML-Interest: Re: private specifications, syntax Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, > Date: Wed, 23 Feb 2000 23:51:05 -0600 (CST) > From: "Gary T. Leavens" > > In previous emails we have discussed the desirability of labeling > method specifications (i.e., behavior clauses) with a privacy > (visibility) annotation. > > For the syntax, ... use underbars to connect the modifiers to the other > keywords, forming long keywords like public_normal_behavior, > protected_normal_behavior, etc. For example, one would write: > > public abstract class Super { > /*@ spec_public @*/ private int z; > > public int state() > /*@ public_normal_behavior > @ ensures: \result == z; > @*/ > > public abstract int f (int y) ; > /*@ public_normal_behavior > @ requires: y >= state(); > @ ensures: state() == y; > @ implies_that > @ private_normal_behavior > @ requires: y >= z; > @ ensures: z == y; > @*/ > } > > I should hasten to add that lightweight specifications would be > unaffected; they would implicitly be "public", since that seems to be > the most common desire (and matches ESC/Java). > > > Barring strenuous objections or better ideas, I think we should adopt > this syntax in JML. Since no one objected, we are adopting that syntax. We have also done similarly for examples, using normal_public_example, etc. Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Mon Feb 28 18:28:54 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id SAA12853 for jml-interest-list-outgoing; Mon, 28 Feb 2000 18:28:52 -0600 (CST) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id SAA12847; Mon, 28 Feb 2000 18:28:47 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id SAA23857; Mon, 28 Feb 2000 18:28:38 -0600 (CST) Date: Mon, 28 Feb 2000 18:28:38 -0600 (CST) Message-Id: <200002290028.SAA23857@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu In-reply-to: <200002232341.RAA00855@larch.cs.iastate.edu> (leavens@cs.iastate.edu) Subject: Re: JML-Interest: defaults for omitted clauses in JML References: <200001140026.SAA01015@larch.cs.iastate.edu> <200002232341.RAA00855@larch.cs.iastate.edu> Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Mon, 28 Feb 2000 18:28:38 -0600 (CST) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu In-reply-to: <200002232341.RAA00855@larch.cs.iastate.edu> (leavens@cs.iastate.edu) Subject: Re: JML-Interest: defaults for omitted clauses in JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, > Date: Wed, 23 Feb 2000 17:41:31 -0600 (CST) > From: "Gary T. Leavens" > > I wonder if also the requires, when, ensures, and diverges clauses > should default to \not_specified in the lightweight case. I think that > would be sensible for also combinations for specifications that are > omitted. > > This would make the table look like: > > ` Default' > `Omitted clause lightweight non-lightweight' > ___________________________________________________ > `requires: \not_specified true' > `when: \not_specified true' > `measured_by: \not_specified \not_specified' > `modifiable: \not_specified \nothing' > `ensures: \not_specified true' > `signals: (Exception) true (Exception) true' > `diverges: \not_specified false' No one has commented on this. However, the default for signals/exsures should also be \not_specified in the lightweight case. I'm assuming everyone is happy with this. Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Mon Mar 27 18:07:59 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id SAA03076 for jml-interest-list-outgoing; Mon, 27 Mar 2000 18:07:54 -0600 (CST) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id SAA03071; Mon, 27 Mar 2000 18:07:50 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id SAA08530; Mon, 27 Mar 2000 18:07:42 -0600 (CST) Date: Mon, 27 Mar 2000 18:07:42 -0600 (CST) Message-Id: <200003280007.SAA08530@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: Desugarings for JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Mon, 27 Mar 2000 18:07:42 -0600 (CST) From: "Gary T. Leavens" To: jml-interest@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: Desugarings for JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, I'd like to announce the following technical report, which will be of interest to JML folk. Arun D. Raghavan and Gary T. Leavens. Desugaring JML Method Specifications. Department of Computer Science, Iowa State University, TR #00-03, March 2000. You can get it from: ftp://ftp.cs.iastate.edu/pub/techreports/TR00-03/TR.ps.gz This paper presents a desugaring process that boils down all of the syntactic sugars in JML into a much simpler form. Comments on it are quite welcome. One interesting thing I'd like to bring to your attention is that we found it helpful in describing the desugaring to allow modifiable clauses of the form: modifiable: x, y if Q, a if R; where some condition is used to described when a variable can be modified. For example, x and y can only be modified if q is true, and if R is true then a can be modified. Any reactions to including this in JML for real? (I see in writing out this example that the grammar is a bit ambiguous, we'd have to work on that.) Gary Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1040 USA leavens@cs.iastate.edu phone: +1 515 294-1580 fax: +1 515 294-0258 URL: http://www.cs.iastate.edu/~leavens  1, forwarded,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Wed Apr 5 17:10:41 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id RAA25674 for jml-interest-list-outgoing; Wed, 5 Apr 2000 17:10:32 -0500 (CDT) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id RAA25669; Wed, 5 Apr 2000 17:10:29 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id RAA16355; Wed, 5 Apr 2000 17:10:21 -0500 (CDT) Date: Wed, 5 Apr 2000 17:10:21 -0500 (CDT) Message-Id: <200004052210.RAA16355@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: Safely Creating Correct Subclasses without Seeing Superclass Code Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Wed, 5 Apr 2000 17:10:21 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: Safely Creating Correct Subclasses without Seeing Superclass Code Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, I'd like to announce the following paper. Clyde Ruby and Gary T. Leavens. Safely Creating Correct Subclasses without Seeing Superclass Code. Department of Computer Science, Iowa State University, TR #00-05, April 2000. You can get it from ftp://ftp.cs.iastate.edu/pub/techreports/TR00-05/TR.ps.gz or the JML web page. The abstract is: A major problem for object-oriented frameworks and class libraries is how to provide enough information about a superclass, so programmers can safely create new subclasses without giving away the superclass's code. Code inherited from the superclass can call down to methods of the subclass, which may cause nontermination or unexpected behavior. We describe a reasoning technique that allows programmers, who have no access to the code of the superclass, to determine how to safely override and when it is safe to call the superclass's methods. The technique consists of a set of rules and some new forms of specification. Part of the specification would be generated automatically by a tool, a prototype of which is planned for the formal specification language JML. We give an example to show how our technique would be used in practice, and argue why the technique is sound. Comments are very welcome. Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Sun Apr 16 14:15:17 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id OAA24216 for jml-interest-list-outgoing; Sun, 16 Apr 2000 14:15:04 -0500 (CDT) Received: from ren.cs.iastate.edu (leavens@ren.cs.iastate.edu [129.186.3.41]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id OAA24211; Sun, 16 Apr 2000 14:15:00 -0500 (CDT) Received: (from leavens@localhost) by ren.cs.iastate.edu (8.9.0/8.9.0) id OAA13671; Sun, 16 Apr 2000 14:14:57 -0500 (CDT) Date: Sun, 16 Apr 2000 14:14:57 -0500 (CDT) Message-Id: <200004161914.OAA13671@ren.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: Query about changes and plans for JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Sun, 16 Apr 2000 14:14:57 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: Query about changes and plans for JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Issues and plans for JML The following are some issues and plans for JML from our seminar last week. We are interested in engaging in discussions about whether to proceed with them, or which variants should be used. Please send comments... 1. Remaining differences from ESC/Java A. colons in the JML syntax. Should there be optional in JML? Use ensures_redundantly, etc.? B. order of declaration and specification. Should the specification come after the declaration? C. we are changing \label to \lblpos, as requested. But should we keep \label has a syntactic sugar? Could \label be automatically translated into one of \lblpos or \lblneg depending on context? We also wondered whether some more convenient syntax for label insertions could be had. For example, what about something like a parenthesized expression with a label at the beginning followed by a colon? ensures: (Asmall : A < B); Or, we could use the colons following the JML keywords as a place to insert labels ensures Asmall: A < B; (We have not yet tried these options out to see which would be parseable.) D. the brackets for nested specifications in JML, {[ and ]}. Is there some way to use just { and }? Perhaps this can be done by not allowing nesting of specifications used as statements, and also by putting specifications before declarations? (We have not yet tried these options out to see which would be parseable.) 2. Other issues A. new syntax \other is needed for subclassing contracts in the callable and accessible clauses (as an expression) use "if" in the syntax for modifiable and measured_by clauses, e.g., modifiable: x if z > 0, y if z < 0; (this need some syntactic work) the conjoinable specifications, which occur after "and", can't be private or protected and are always lightweight. We propose making it possible to give a heavyweight version of a conjoinable specification, which would make specification of privacy possible. We would also need to be able to repeat several conjoinable specifications at the beginning of a method specification. T m(); and protected_behavior ensures: ...; signals: ...; diverges: ...; private_normal_behavior ensures: ...; (We have not yet tried this out to see if it would be parseable.) B. new defaults when \not_specified is used in the preconditions, the meaning it would be taken as follows for use in a subtype -> true (a warning would be given by the run-time checking generation tool) for use in refinement -> false subclassing_contracts should default to \not_specified C. new semantics the checker should allow model methods, fields, or types to be implemented in a refinement or subtype. In the implementation these are become like spec_V, where V is the visibility of the original D. changes to the tools the type checker should make sure that overriding methods use the extending specification form the type checker should do purity checking Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Fri May 12 18:51:40 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id SAA13065 for jml-interest-list-outgoing; Fri, 12 May 2000 18:51:36 -0500 (CDT) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id SAA13028; Fri, 12 May 2000 18:51:02 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id SAA13855; Fri, 12 May 2000 18:50:51 -0500 (CDT) Date: Fri, 12 May 2000 18:50:51 -0500 (CDT) Message-Id: <200005122350.SAA13855@larch.cs.iastate.edu> From: "Gary T. Leavens" To: bart@cs.kun.nl, marieke@cs.kun.nl, joachim@cs.kun.nl, erikpoll@cs.kun.nl, s.j.h.kent@ukc.ac.uk, stata@pa.dec.com, rustan@pa.dec.com, visray@hotmail.com (Rayan), htewis@curry.de (Holger_Tewis), Tom@OjodeAgua.COM (Tom_Shields), jhughes@mail.frostburg.edu (John_Hughes), jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: New Release of JML, 1.4 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Fri, 12 May 2000 18:50:51 -0500 (CDT) From: "Gary T. Leavens" To: bart@cs.kun.nl, marieke@cs.kun.nl, joachim@cs.kun.nl, erikpoll@cs.kun.nl, s.j.h.kent@ukc.ac.uk, stata@pa.dec.com, rustan@pa.dec.com, visray@hotmail.com (Rayan), htewis@curry.de (Holger_Tewis), Tom@OjodeAgua.COM (Tom_Shields), jhughes@mail.frostburg.edu (John_Hughes), jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: New Release of JML, 1.4 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, We've just made another release of JML, 1.4, which is available from the JML ftp site: ftp://ftp.cs.iastate.edu/pub/leavens/JML/ in the file JML.1.4.zip or from the JML web page (http://www.cs.iastate.edu/~leavens/JML.html). This release moves us closer to ESC/Java, but more importantly, has significant tool improvements. There are a few bugs, so if you're not in a rush, you might want to wait a week for another release. However, you'll find that the tool support is generally much better than the 1.3 release. We will be making another release shortly (in a week, I hope) to fix bugs and to convert the grammar to have method specifications before declarations of the corresponding method, to better match ESC/Java. New with release 1.4 (date: May 12, 2000) major improvements: - There is now support for run-time checking of preconditions, thanks to Abhay Bhorkar. Use bin/jassertc to compile and bin/jassert to run such applications. See the preliminary design document for an example. - The checker now recognizes specifications in Java documentation comments that are enclosed in and or and tags, thanks to Arun Raghavan. - The checker now enforces privacy restrictions in specifications; the keywords that start model programs and heavyweight specifications and examples now all have privacy modifiers public_, protected_, or private_ (e.g., public_behavior). Lightweight specifications are implicitly public. Thanks to Abhay Bhorkar and Clyde Ruby for help on this. - A still limited but somewhat useful capability of generating HTML from JML specifications, thanks to Arun Raghavan. - The syntax for modifiable clauses (and measured_by clauses) now allows for conditional specification with the "if" keyword. - Improvements and extensions to the syntax of conjoinable specifications (extending specifications that start with "and"), thanks to Arun Raghavan. See the NEWS.txt file for a host of other more minor improvements, and for incompatibilities. Please let us know your comments on JML, and if you find bugs. There are some already documented bugs in the BUGS.txt file... Also, we have gone to some pain to make development possible (although it may not yet be easy) outside of Iowa State. Since JML is open source, feel free to send us code with bug fixes also! Special thanks to the students named above on this release. See the preliminary design document for other acknowledgments. Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Mon May 15 13:18:10 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id NAA22300 for jml-interest-list-outgoing; Mon, 15 May 2000 13:18:03 -0500 (CDT) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id NAA22295; Mon, 15 May 2000 13:17:57 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id NAA08936; Mon, 15 May 2000 13:17:50 -0500 (CDT) Date: Mon, 15 May 2000 13:17:50 -0500 (CDT) Message-Id: <200005151817.NAA08936@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: where can you use \old( ) in JML? Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Mon, 15 May 2000 13:17:50 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: where can you use \old( ) in JML? Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, Where is \old( ) allowed to be used in JML? This hasn't been answered clearly in the documentation (such as it is). We believe the basic answer is that, whereever there are two states involved, \old( ) should be allowed to be used. There is some question, however, as to what constructs should be assertions about 2 states. So here is a table of our current thinking on the matter. Comments will be appreciated. There is some more discussion following the table. clause \old( ) allowed ------------------------------------------------------------- requires no when no expressions in measured_by no predicates following "if" in measured_by no store_refs in modifiable no predicates following "if" in modifiable no ensures yes signals/exsures yes diverges no axiom pragmas no represents clause no invariants no history constraints yes initially (on declaration) no readable_if (on declaration) no monitored_by (on declaration) no maintaining/loop_invariants yes decreasing/decreases (variant functions) yes assume statement yes assert statement yes because statement yes ----------------------------------------------------------------- These last 5 are probably the most interesting cases. It's nice when doing a proof by the intermittent assertion method, to be able to discuss the pre-state without having to explicitly introduce new variables for it, and this helps one also to relate the last assertion to the postcondition. Assume plays a similar role to assert, and "because" clauses would be giving reasons between assertions, so those seem to go the same way as assert. Similar remarks apply to loop invariants and variant functions. The use of \old( ) in these 5 places certainly complicates reasoning and the implementation of run-time checkers. However, my opinion is that we should support the use of \old in these places, if we want to follow Eiffel and use \old at all. (On the other hand, Eiffel itself is very pragmatic: it doesn't allow intermittent assertions at all, and doesn't allow "old" to be used anywhere but ensures clauses.) I'm also a bit unsure about the measured_by clause. Although it seems reasonable, I think that for the sake of simplicity (!) we should disallow \old there. I th