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 think it's fairly clear that we don't want old in axioms. Does that seem right? Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Wed May 17 17:09:10 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id RAA05538 for jml-interest-list-outgoing; Wed, 17 May 2000 17:08:53 -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 RAA05533; Wed, 17 May 2000 17:08:51 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id RAA01090; Wed, 17 May 2000 17:08:43 -0500 (CDT) Date: Wed, 17 May 2000 17:08:43 -0500 (CDT) Message-Id: <200005172208.RAA01090@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: bracket token for nested specifications in JML: {| and |}? Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Wed, 17 May 2000 17:08:43 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: bracket token for nested specifications in JML: {| and |}? Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, In debugging release 1.4, we've run across an example in the JDK that has an array intitializer that uses array elements. This means it has the characters ] and } next to each other, as in the following: public abstract class array_decl_initializer { public void f() { Object[] x = new Object[3]; x[0] = null; Object[] y = {x[0], x[1]}; // note the ]} return; } } Needless to say, this is most unplesant for the JML parser, which interprets the "]}" as the "end of nested specification" token, not as two separate tokens. While it's possible to recogize that only outside of JML specifications, that's not the most ideal solution. Raymie Stata, and others have expressed dislike of the brackets {[ and ]} in JML for nested specifications. We have tried a couple of times to use { and } for this, but run against parser problems due to the (non-static) initializers in Java, which also start with {. Since these can have arbitrary statements in them, there can be any number of '{' characters before some more distinguishing context might be found. But since the {[ and ]} choice wasn't very popular, it seems silly to try to go to great lengths to fix it, when perhaps something else might work and meet with wider approval for delimiting nested specifications. Suggestions are welcome. Clyde Ruby and I think that {| and |} might work. What do you think of that? Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Mon May 29 10:13:34 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id KAA00271 for jml-interest-list-outgoing; Mon, 29 May 2000 10:13:30 -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 KAA00264; Mon, 29 May 2000 10:12:55 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id KAA24986; Mon, 29 May 2000 10:12:49 -0500 (CDT) Date: Mon, 29 May 2000 10:12:49 -0500 (CDT) Message-Id: <200005291512.KAA24986@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.5 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Mon, 29 May 2000 10:12:49 -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.5 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, We've just made another release of JML, 1.5, which is available from the JML ftp site: ftp://ftp.cs.iastate.edu/pub/leavens/JML/ in the file JML.1.5.zip or from the JML web page (http://www.cs.iastate.edu/~leavens/JML.html). This release is purely a bug fix release, and doesn't yet have the change to move specifications in front of declarations. We hope to do that today, but if that doesn't happen, you'll have to wait until after June 20, as I'm off to ICSE and ECOOP tomorrow. New with release 1.5 (date: May 29, 2000) major improvements: - Privacy restrictions in JML specifications are now correctly (and much more vigorously) enforced. Lightweight method specifications now implicitly adopt the privacy level of the method being specified. - The HTML generation is much improved, and the top-level HTML file (now named JML.html) links to the specifications for the model directory (thanks to Arun Raghavan). Various options have been added to the checker to better support HTML generation. - The checker is much faster, and deals avoids unnecessary disk access and parsing of files (thanks to Clyde Ruby). pretty nice improvements: - Support for JDK 1.3 (modifier "strictfp" and javadoc tag "@docRoot"). - Various bug fixes (thanks to Clyde Ruby and Arun Raghavan). The runtime assertion generator doesn't die when run on various files. More test cases added to ensure the checker will pass the JDK (some are still documented as bugs in the shouldbegood or shouldbebad directory). - Used of nested classes doesn't cause the checker to die, although the handling of private attributes in nested class isn't fixed yet (thanks to Clyde Ruby) - The makefiles now check the "bad" specifications and compare the error output against what was expected. - Corrections to the NEWS.txt file, including a note that the previous release fixed the treatment of refinement files. - The Antlr file FileLineFormatter.class is included in the distribution's antlr.jar file (thanks to Erik Poll). - The Unix and cygwin shell scripts for jml now work properly. - The jmlstartfiles script gives the files that jml will start on in the current directory. - More shell scripts added for developers (jmldb*). - Remaining known bugs have been documented in the BUGS.txt file. incompatible changes: - The brackets for nested specifications have been changed from {[ and ]} to {| and |}. Please let us know your comments on JML, and if you find bugs. There are some already documented bugs in the BUGS.txt file. We believe it's fairly complete now. Special thanks to Arun Raghavan and Clyde Ruby for help with this release. See the preliminary design document for other acknowledgments. Gary  1, answered,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Mon Jun 5 11:04:22 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id LAA06020 for jml-interest-list-outgoing; Mon, 5 Jun 2000 11:04:10 -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 LAA06014; Mon, 5 Jun 2000 11:04:06 -0500 (CDT) Received: (from leavens@localhost) by ren.cs.iastate.edu (8.9.0/8.9.0) id LAA28972; Mon, 5 Jun 2000 11:04:04 -0500 (CDT) Date: Mon, 5 Jun 2000 11:04:04 -0500 (CDT) Message-Id: <200006051604.LAA28972@ren.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Wed, 31 May 2000 12:19:37 +0200 (MET DST)) Subject: Re: JML-Interest: New Release of JML, 1.5 References: Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Mon, 5 Jun 2000 11:04:04 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Wed, 31 May 2000 12:19:37 +0200 (MET DST)) Subject: Re: JML-Interest: New Release of JML, 1.5 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, Here's a report on the 1.5 release that you may need to use until we can fix it... > Date: Wed, 31 May 2000 12:19:37 +0200 (MET DST) > From: Erik Poll > Content-Type: TEXT/PLAIN; charset=US-ASCII > > I tried out the new jml-1.5. It's definitely a _lot_ faster. Also, I get > a lot more complaints about violation privacy restrictions - so I have > some work to do on the specs I wrote... > > Trying to run jml-1.5 I again ran into the problem that it needs > some antlr files which are not in antlr.jar. (Again, I solved the > problem by including my own antlr directory in CLASSPATH.) > One of the files that's missing is DefineGrammarSymbols - but there > might be others. Users of JML who have downloaded the 1.5 release should use this trick until we can get a reliable fix (which may not happen until I return from conferences on June 20). Sorry. You can get the antlr release from www.antlr.org. Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Tue Jun 27 14:12:37 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id OAA01130 for jml-interest-list-outgoing; Tue, 27 Jun 2000 14:12:28 -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 OAA01125; Tue, 27 Jun 2000 14:12:25 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id OAA08506; Tue, 27 Jun 2000 14:12:18 -0500 (CDT) Date: Tue, 27 Jun 2000 14:12:18 -0500 (CDT) Message-Id: <200006271912.OAA08506@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: questions about semantics changes proposed for JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Tue, 27 Jun 2000 14:12:18 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: questions about semantics changes proposed for JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hello, I have now returned from my travels to the ICSE and ECOOP conferences. Actually I came back last week, however, I have two master's students who are trying to finish, 2-3 papers, the usual after conference mail, a cold (better now), and jet lag that has kept me busy. (I started this email on Monday...) I apologize to those waiting for bug fixes on JML; I hope to get to those soon.... In the meantime I wanted to share with you some thoughts about semantic changes to JML, prompted in part by discussions at the various conferences. One interesting comment: Michael Ernst said that "JML is becoming a standard." When I expressed extreme surprise at this, he clarified that he meant "for researchers". :-) I've divided up the list into two parts, based on our current plans. THINGS WE PLAN TO CHANGE UNLESS SOMEONE COMPLAINS Doug Lea talked with me about the semantics of the modifiable clause. The current semantics allows temporary side effects to variables; that is, they can be assigned to and restored to their original value without being modified by a method. However, this causes problems for concurrency, and he urged us to change the sematics so that modifiable means permission to assign to a variable. As you know, it is difficult to check for the current semantics at run-time. It would be easy, on the other hand, to use static analysis to check the proposed semantics. Furthermore, Clyde Ruby and I have found that temporary side effects also cause problems for writing subclasses based on superclass specifications. Hence I think it's clear we should change the semantics as proposed. I discussed with Wolfgang Week and Martin Buechi their "greybox" approach to specification in the refinement calculus. The idea is that method calls to non-pure methods in model programs are part of the specification, and must appear in any refinement to be called in an equivalent state. Yesterday, Clyde Ruby and I noted that represents clauses shouldn't be allowed between two concrete variables. One should use an invariant instead. Because == and != are not equivalence relations on floating point numbers in Java, due to the IEEE standard and NaN, I think we should disallow the use of == and != on floating point numbers in JML assertions. The type checker could give errors for such uses. THINGS IN NEED OF MORE DISCUSSION Bart Jacobs and Joachim van den Berg and I discussed the semantics of expressions used in assertions in JML. The question is what to do about partial operators, i.e., about expressions that may throw exceptions. I had advocated a semantics in which a subexpression that throws an exception is replaced by an arbitrary value of the appropriate type. However, Bart pointed out to me that this could cause problems, especially in the preconditions. Bart and Joachim advocate an interpretation that gives assertions the value "false" in preconditions, and "true" elsewhere. John Boyland advocated static checking to ensure that assertions used in specifications are protective. There will be more discussion about this... Nearing the top of the list of things to do for JML is "purity checking". A basic problem for purity checking is what to do about classes with no specification annotations. My thoughts at this point by that we should trust the programmer for classes without specifications, although we need to provide a specification of most of the JDK ourselves. Of course, trusting the programmer gets rid of some of the teeth of purity checking; but the alternative of forcing some specifications for purity annotations does not seem practical. Locally, we have started using the next version of JML, which has declarations following the specifications of methods. This seems pretty ugly when the annotation markers /*@ ... @*/ are not used around specifications. I wonder if, in the interests of simplification, it would be best to drop the .jml file syntax, which doesn't require the annotation markers. We could still have .jml files, but with the annotation markers necessary. Comments and discussion of all of these points are welcome. Gary  1,, X-Coding-System: undecided-unix Mail-from: From Peter.Mueller@FernUni-Hagen.de Wed Jun 28 03:59:02 2000 Return-Path: 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 DAA13695; Wed, 28 Jun 2000 03:58:59 -0500 (CDT) Received: from sunpoet2.fernuni-hagen.de by oak.fernuni-hagen.de via local-channel with ESMTP; Wed, 28 Jun 2000 10:58:31 +0200 Received: (from mueller@localhost) by sunpoet2.fernuni-hagen.de (8.9.3+Sun/8.9.1) id KAA02748; Wed, 28 Jun 2000 10:58:16 +0200 (MET DST) Date: Wed, 28 Jun 2000 10:58:16 +0200 (MET DST) Message-Id: <200006280858.KAA02748@sunpoet2.fernuni-hagen.de> X-Authentication-Warning: sunpoet2.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: questions about semantics changes proposed for JML In-Reply-To: <200006271912.OAA08506@larch.cs.iastate.edu> References: <200006271912.OAA08506@larch.cs.iastate.edu> X-Mailer: VM 6.32 under Emacs 20.3.1 *** EOOH *** Date: Wed, 28 Jun 2000 10:58:16 +0200 (MET DST) X-Authentication-Warning: sunpoet2.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: questions about semantics changes proposed for JML In-Reply-To: <200006271912.OAA08506@larch.cs.iastate.edu> Hi, > Doug Lea talked with me about the semantics of the modifiable clause. > The current semantics allows temporary side effects to variables; > that is, they can be assigned to and restored to their original value > without being modified by a method. However, this causes problems for > concurrency, and he urged us to change the sematics so that modifiable > means permission to assign to a variable. As you know, it is difficult > to check for the current semantics at run-time. It would be easy, on > the other hand, to use static analysis to check the proposed semantics. > Furthermore, Clyde Ruby and I have found that temporary side effects > also cause problems for writing subclasses based on superclass > specifications. Hence I think it's clear we should change the semantics > as proposed. I just wanted to remark that the new semantics of modifiable-clauses cannot be expressed by pre-post-pairs. Thus, it is difficult to use classical Hoare logic for verification. But of course, one could use other static analysis techniques to check for this semantics. 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 Thu Jun 29 16:59:32 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id QAA19514 for jml-interest-list-outgoing; Thu, 29 Jun 2000 16:59:20 -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 QAA19508; Thu, 29 Jun 2000 16:59:13 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id QAA00616; Thu, 29 Jun 2000 16:59:05 -0500 (CDT) Date: Thu, 29 Jun 2000 16:59:05 -0500 (CDT) Message-Id: <200006292159.QAA00616@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: <200006280858.KAA02748@sunpoet2.fernuni-hagen.de> (message from Peter Mueller on Wed, 28 Jun 2000 10:58:16 +0200 (MET DST)) Subject: Re: JML-Interest: questions about semantics changes proposed for JML References: <200006271912.OAA08506@larch.cs.iastate.edu> <200006280858.KAA02748@sunpoet2.fernuni-hagen.de> Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Thu, 29 Jun 2000 16:59:05 -0500 (CDT) From: "Gary T. Leavens" To: Peter.Mueller@FernUni-Hagen.de CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: <200006280858.KAA02748@sunpoet2.fernuni-hagen.de> (message from Peter Mueller on Wed, 28 Jun 2000 10:58:16 +0200 (MET DST)) Subject: Re: JML-Interest: questions about semantics changes proposed for JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Peter, > Date: Wed, 28 Jun 2000 10:58:16 +0200 (MET DST) > From: Peter Mueller > > Hi, > > > Doug Lea talked with me about the semantics of the modifiable clause. > > The current semantics allows temporary side effects to variables; > > that is, they can be assigned to and restored to their original value > > without being modified by a method. However, this causes problems for > > concurrency, and he urged us to change the sematics so that modifiable > > means permission to assign to a variable. As you know, it is difficult > > to check for the current semantics at run-time. It would be easy, on > > the other hand, to use static analysis to check the proposed semantics. > > Furthermore, Clyde Ruby and I have found that temporary side effects > > also cause problems for writing subclasses based on superclass > > specifications. Hence I think it's clear we should change the semantics > > as proposed. > > I just wanted to remark that the new semantics of modifiable-clauses cannot > be expressed by pre-post-pairs. Thus, it is difficult to use classical Hoare > logic for verification. But of course, one could use other static analysis > techniques to check for this semantics. I think what you mean is that the semantics cannot be exactly captured by a Hoare logic. That is certainly true, since the intermediate states of a method aren't seen. However, I think that one can still use a consequence of such a specification, namely what we used to think the semantics was (no modification), in a Hoare triple and thus do verification based on this weaker notion, which is no different than the usual kind of verification with the usual frame axiom from the modifiable clauses. Is that right? Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Thu Jun 29 17:37:08 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id RAA20140 for jml-interest-list-outgoing; Thu, 29 Jun 2000 17:37:05 -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 RAA20132; Thu, 29 Jun 2000 17:37:01 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id RAA01253; Thu, 29 Jun 2000 17:36:52 -0500 (CDT) Date: Thu, 29 Jun 2000 17:36:52 -0500 (CDT) Message-Id: <200006292236.RAA01253@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu, ruby@cs.iastate.edu (Clyde_Ruby) Subject: JML-Interest: Comments on new draft of "Safely Creating Correct Subclasses ..."? Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Thu, 29 Jun 2000 17:36:52 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu, ruby@cs.iastate.edu (Clyde_Ruby) Subject: JML-Interest: Comments on new draft of "Safely Creating Correct Subclasses ..."? Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, If you have time to read and give us comments on a (revised) draft of the paper: Safely Creating Correct Subclasses without Seeing Superclass Code, by Clyde Ruby and Gary T. Leavens, which is to appear in OOPSLA 2000, we'd appreciate it greatly. The best time to give us comments in in the next 2 weeks. This paper uses JML and the subclassing contracts feature of JML. It also gives a preview of what the syntax looks like with the declarations following the specifications. If you're interested, you can get the paper from the following URL: ftp://ftp.cs.iastate.edu/pub/techreports/TR00-05/TR.ps.gz which is a gzipped postscript file. Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Fri Jun 30 02:59:29 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id CAA27952 for jml-interest-list-outgoing; Fri, 30 Jun 2000 02:59:27 -0500 (CDT) 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 CAA27947; Fri, 30 Jun 2000 02:59:23 -0500 (CDT) Received: from sunpoet2.fernuni-hagen.de by oak.fernuni-hagen.de via local-channel with ESMTP; Fri, 30 Jun 2000 09:59:14 +0200 Received: (from mueller@localhost) by sunpoet2.fernuni-hagen.de (8.9.3+Sun/8.9.1) id JAA09618; Fri, 30 Jun 2000 09:58:57 +0200 (MET DST) Date: Fri, 30 Jun 2000 09:58:57 +0200 (MET DST) Message-Id: <200006300758.JAA09618@sunpoet2.fernuni-hagen.de> X-Authentication-Warning: sunpoet2.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: questions about semantics changes proposed for JML In-Reply-To: <200006292159.QAA00616@larch.cs.iastate.edu> References: <200006271912.OAA08506@larch.cs.iastate.edu> <200006280858.KAA02748@sunpoet2.fernuni-hagen.de> <200006292159.QAA00616@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: Fri, 30 Jun 2000 09:58:57 +0200 (MET DST) X-Authentication-Warning: sunpoet2.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: questions about semantics changes proposed for JML In-Reply-To: <200006292159.QAA00616@larch.cs.iastate.edu> Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi again, > > I just wanted to remark that the new semantics of modifiable-clauses cannot > > be expressed by pre-post-pairs. Thus, it is difficult to use classical Hoare > > logic for verification. But of course, one could use other static analysis > > techniques to check for this semantics. > > I think what you mean is that the semantics cannot be exactly captured > by a Hoare logic. That is certainly true, since the intermediate states > of a method aren't seen. However, I think that one can still use a > consequence of such a specification, namely what we used to think the > semantics was (no modification), in a Hoare triple and thus do > verification based on this weaker notion, which is no different than the > usual kind of verification with the usual frame axiom from the > modifiable clauses. Is that right? Yes. If you want to use the specification of a method m to verify invocation sites, it is certainly possible to use a weaker semantics for the modifiable-clause. However, to verify that the implementation of m meets its specification, Hoare logic does not suffice since it cannot capture the strong semantics of the modifiable-clause. 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 Jun 30 16:47:30 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id QAA11363 for jml-interest-list-outgoing; Fri, 30 Jun 2000 16:47:26 -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 QAA11358; Fri, 30 Jun 2000 16:47:23 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id QAA11434; Fri, 30 Jun 2000 16:47:15 -0500 (CDT) Date: Fri, 30 Jun 2000 16:47:15 -0500 (CDT) Message-Id: <200006302147.QAA11434@larch.cs.iastate.edu> From: "Gary T. Leavens" To: leavens@cs.iastate.edu CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: <200006051604.LAA28972@ren.cs.iastate.edu> (leavens@cs.iastate.edu) Subject: Re: JML-Interest: New Release of JML, 1.5 References: <200006051604.LAA28972@ren.cs.iastate.edu> Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Fri, 30 Jun 2000 16:47:15 -0500 (CDT) From: "Gary T. Leavens" To: leavens@cs.iastate.edu CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: <200006051604.LAA28972@ren.cs.iastate.edu> (leavens@cs.iastate.edu) Subject: Re: JML-Interest: New Release of JML, 1.5 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, > Date: Mon, 5 Jun 2000 11:04:04 -0500 (CDT) > From: "Gary T. Leavens" > > Hi, > > Here's a report on the 1.5 release that you may need to use until we can > fix it... > > > Date: Wed, 31 May 2000 12:19:37 +0200 (MET DST) > > From: Erik Poll > > Content-Type: TEXT/PLAIN; charset=US-ASCII > > > > I tried out the new jml-1.5. It's definitely a _lot_ faster. Also, I get > > a lot more complaints about violation privacy restrictions - so I have > > some work to do on the specs I wrote... > > > > Trying to run jml-1.5 I again ran into the problem that it needs > > some antlr files which are not in antlr.jar. (Again, I solved the > > problem by including my own antlr directory in CLASSPATH.) > > One of the files that's missing is DefineGrammarSymbols - but there > > might be others. > > > Users of JML who have downloaded the 1.5 release should use this trick > until we can get a reliable fix (which may not happen until I return > from conferences on June 20). Sorry. > You can get the antlr release from www.antlr.org. I believe we have finally gotten all of the required files in the antlr.jar file, which I have retrofitted into the 1.5 release file. So now, if you fetch the 1.5 release, the antlr.jar file should work as it was supposed to. If you already have the 1.5 release, you can just download the antlr.jar file in the JML ftp directory (or from the web page for JML) and put that in the directory JML at the top of your copy. Sorry this has taken so long... it shouldn't happen again. Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Fri Jul 28 00:42:41 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id AAA03317 for jml-interest-list-outgoing; Fri, 28 Jul 2000 00:42:35 -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 AAA03290; Fri, 28 Jul 2000 00:41:42 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id AAA09439; Fri, 28 Jul 2000 00:41:36 -0500 (CDT) Date: Fri, 28 Jul 2000 00:41:36 -0500 (CDT) Message-Id: <200007280541.AAA09439@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), scmarney@home.com, htewis@curry.de (Holger_Tewis), Tom@OjodeAgua.COM (Tom_Shields), jhughes@mail.frostburg.edu (John_Hughes), kramer@acm.org (Reto_Kramer), abhay_b@hotmail.com (Abhay_Bhorkar), jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu, jml@cs.iastate.edu Subject: JML-Interest: New Release of JML, 2.0 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Fri, 28 Jul 2000 00:41:36 -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), scmarney@home.com, htewis@curry.de (Holger_Tewis), Tom@OjodeAgua.COM (Tom_Shields), jhughes@mail.frostburg.edu (John_Hughes), kramer@acm.org (Reto_Kramer), abhay_b@hotmail.com (Abhay_Bhorkar), jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu, jml@cs.iastate.edu Subject: JML-Interest: New Release of JML, 2.0 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, I've just made another release of JML, 2.0, which is available from the JML ftp site: ftp://ftp.cs.iastate.edu/pub/leavens/JML/ in the file JML.2.0.zip or from the JML web page (http://www.cs.iastate.edu/~leavens/JML.html). This release, finally, makes the big, incompatible syntax change that puts method specifications in front of the method header. I'm sorry this has taken so long, but various things going on prevented me from finishing this sooner. In any case, this completes the major syntactic merge with ESC/Java. There are also numerous bug fixes. Although improved, the run-time checker still has bugs that limit its usefulness for interesting specifications (e.g., with invariants, depends, and represents clauses) in this release. We hope to make bug fixes in the next release. However, the HTML document generation of the jml checker is working very well now. The changes are summarized below. New with release 2.0 (date: July 27, 2000) major improvements: - The syntax has been modified to put method specifications in front of the corresponding method declaration. This completes JML's integration with the syntax of ESC/Java. This is an incompatible change, however. - The modifiable clause has a semantics that prohibits assignment to other locations. This seems better for static enforcement, reasoning about concurrency, and avoiding temporary side effects. This is another incompatible change. - The HTML generation has been much improved, thanks to Arun Raghavan. - The unparser, which is used by the run-time assertion checker, now properly handles model constructs, and doesn't generate nested comments. It also does a better job of pretty-printing output. pretty nice improvements: - The JML checker now gives reasonable error messages when illegal characters appear in the input. - The antlr.jar file that ships with JML now has all the necessary class files in it. - The run-time checker now produces output that parses when used under Windows, because backslashes in filenames are escaped. - The checker now handles calls to synchronized methods properly. - The preliminary design document has been edited, and various sections clarified, especially the part about the modifiable clause. - The main documents and all specifications have been brought up to date with the new syntax. - The shell scripts now assume you have JDK 1.2.2 on Linux, and JDK 1.3 under Windows and cygwin. - The checker does a better job with inner classes, although it still has bugs in this area. incompatible changes: - The syntax has been changed to put method specifications in front of the corresponding method declaration. - The meaning of the modifiable clause has changed; it now has the more stringent requirement of only allowing assignment to the given locations and their dependents. Please let us know your comments on JML, and if you find bugs. There are some already documented bugs in the BUGS.txt file. It is fairly complete now. Again, thanks to Arun Raghavan and Clyde Ruby for help with this release. See the preliminary design document for other acknowledgments. 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,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Mon Jul 31 16:43:35 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id QAA12004 for jml-interest-list-outgoing; Mon, 31 Jul 2000 16:43:31 -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 QAA11986; Mon, 31 Jul 2000 16:43:03 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id QAA16965; Mon, 31 Jul 2000 16:42:53 -0500 (CDT) Date: Mon, 31 Jul 2000 16:42:53 -0500 (CDT) Message-Id: <200007312142.QAA16965@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), scmarney@home.com, htewis@curry.de (Holger_Tewis), Tom@OjodeAgua.COM (Tom_Shields), jhughes@mail.frostburg.edu (John_Hughes), kramer@acm.org (Reto_Kramer), abhay_b@hotmail.com (Abhay_Bhorkar), jml-interest-list@cs.iastate.edu CC: jml@cs.iastate.edu Subject: JML-Interest: New Release of JML, 2.1 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Mon, 31 Jul 2000 16:42:53 -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), scmarney@home.com, htewis@curry.de (Holger_Tewis), Tom@OjodeAgua.COM (Tom_Shields), jhughes@mail.frostburg.edu (John_Hughes), kramer@acm.org (Reto_Kramer), abhay_b@hotmail.com (Abhay_Bhorkar), jml-interest-list@cs.iastate.edu CC: jml@cs.iastate.edu Subject: JML-Interest: New Release of JML, 2.1 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, I've just made another release of JML, 2.1, which is available from the JML ftp site: ftp://ftp.cs.iastate.edu/pub/leavens/JML/ in the file JML.2.1.zip. You can also get it from the JML web page (http://www.cs.iastate.edu/~leavens/JML.html). I know this is soon after the 2.0 release of JML. However, the 2.0 release didn't run under JDK 1.1 and so I wanted to fix that. This has been done, and is the major minor improvement in the 2.1 release. The changes are summarized below. New with release 2.1 (date: July 31, 2000) minor improvements: - JML now runs again, and can also be compiled, under JDK 1.1. - The modifier "ghost" can be used on local declarations. - Small improvements in the formatting of the HTML output of jml --html. - Clarification of terminology in the preliminary design document for refering to locations on which another location depends, which are now called "dependees" (thanks to Peter Mueller). - Clarification of the context-sensitive constraints on depends and represents clauses in the preliminary design document. - The release zip file should be smaller than 2.0, as the generated HTML files for the test cases and samples are not included. Please let us know your comments on JML, and if you find bugs. See the BUGS.txt file for the ones we know about. See the preliminary design document for other acknowledgments. 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,, X-Coding-System: undecided-unix Mail-from: From fsdm@it.uq.edu.au Thu Aug 24 21:33:36 2000 Return-Path: Received: from wasabi.it.uq.edu.au (wasabi.it.uq.edu.au [130.102.192.56]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id VAA09855 for ; Thu, 24 Aug 2000 21:33:34 -0500 (CDT) Received: from isa.it.uq.edu.au (fsdm@isa.it.uq.edu.au [130.102.16.3]) by wasabi.it.uq.edu.au (8.8.7/8.8.7) with ESMTP id MAA29057 for ; Fri, 25 Aug 2000 12:33:28 +1000 (EST) Received: (from fsdm@localhost) by isa.it.uq.edu.au (8.8.8/8.8.8) id MAA23242 for leavens@cs.iastate.edu; Fri, 25 Aug 2000 12:33:24 +1000 (EST) Date: Fri, 25 Aug 2000 12:33:24 +1000 (EST) From: FSDM Mailing List Message-Id: <200008250233.MAA23242@isa.it.uq.edu.au> Subject: Product announcement: jMocha Precedence: bulk *** EOOH *** Date: Fri, 25 Aug 2000 12:33:24 +1000 (EST) From: FSDM Mailing List Subject: Product announcement: jMocha Precedence: bulk +--- Formal Software Development Methods (FSDM) mailing list ----+ | Submissions and (un)subscription requests to fsdm@it.uq.edu.au | | http://svrc.it.uq.edu.au/pages/FSDM_mailing_list.html | +------- Software Verification Research Centre, Australia -------+ *Release Announcement* THE MODEL CHECKER JMOCHA (Version 1.0) We are pleased to announce the release of the model checker jMocha. Like its predecessor Mocha, this tool offers the following capabilities: 1. System specification in the language of reactive modules. Reactive modules allow the formal specification of heterogeneous systems with synchronous and asynchronous components. Reactive Modules support modular and hierarchical structuring and reasoning. 2. System execution by randomized or manual trace generation. In the manual mode, the user may choose at each step one of the possible next states of the system. 3. Requirement verification by invariant checking. jMocha supports both symbolic and enumerative search. The symbolic model checker is based on BDD engines developed by the UC Berkeley VIS project. 4. Implementation verification by checking trace containment between implementation and specification modules. The check can be performed automatically if the specification module has no private variables, and otherwise, the user has to supply a witness module defining the refinement mapping. For decomposing refinement proofs, jMocha supports an assume-guarantee principle. jMocha is written in Java and uses native C-code BDD libraries from VIS. It provides the following improvements over Mocha: 1. A graphical user interface written in Java that looks familiar to Windows/Java users: it has a project window and a desktop, has a syntax directed editor, allows concurrent threads, and can be easily extended and debugged. 2. A new simulator with a graphical user interface that displays traces in a message sequence chart (MSC) fashion and shows the dependencies among variable updates. 3. A proof manager for managing verification proofs such as assume-guarantee proofs. 4. An enhanced enumerative checker for invariant checking as well as refinement checking with many new optimizations like hierarchical reduction. 5. A new scripting language called Slang for rapid and structured verification algorithm development. Slang provides primitive functions for the symbolic manipulation of transitions systems and state sets, which can be used to program algorithms (e.g. your own CTL model checker) by writing Slang scripts. The distribution, and more information about the tool, are available on the following sites: http://www.eecs.berkeley.edu/~mocha http://www.cis.upenn.edu/~mocha http://www.cs.sunysb.edu/~mocha  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Fri Aug 25 08:09:36 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id IAA19556 for jml-interest-list-outgoing; Fri, 25 Aug 2000 08:08:25 -0500 (CDT) 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 IAA19551; Fri, 25 Aug 2000 08:08:21 -0500 (CDT) Received: from localhost (joachim@localhost) by cicero.cs.kun.nl (8.9.3/8.9.3) with ESMTP id PAA19570; Fri, 25 Aug 2000 15:03:14 +0200 Date: Fri, 25 Aug 2000 15:03:10 +0200 (CEST) From: Joachim van den Berg To: "Gary T. Leavens" cc: jml-interest-list@cs.iastate.edu Subject: JML-Interest: 'bug' fix in the jml grammar 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, 25 Aug 2000 15:03:10 +0200 (CEST) From: Joachim van den Berg To: "Gary T. Leavens" cc: jml-interest-list@cs.iastate.edu Subject: JML-Interest: 'bug' fix in the jml grammar Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi Gary, I have safely returned from my holidays in France. Today I've just started to do some research again. Together with Bart I had a conversation about the discussion which was raised last weeks. I hope we can settle this problem as soon as possible. Today also, I tried to fix an ugly thing in the jml grammar, concerning the behavior, example, and model_program keywords. I was not happy (for you probably the same holds) about the explosion of these keywords. So, I fixed this problem. I've included a grammar where these keywords carry an access modifier, just as in Java. With this grammar specifications are of the form (if I am up-to-date. Didn't do JML for a while): /*@ public normal_behavior @ requires: P; @ ... @*/ public abstract void m(); where the access modifier in the specification is optional. The compiler should do some checks to guarantee that the modifiers are used in a proper way (just as the Java compiler does). I hope that you are happy with this solution and that we can implement this in JML. What do you think? Bye, Joachim -- _____________________________________________________________ Joachim van den Berg___________________tel. +31 24 36 52710 Computer Science Institute_________mailto:joachim@cs.kun.nl University of Nijmegen_______http://www.cs.kun.nl/~joachim/ -- diff /usr/local/JML-2.1/edu/iastate/cs/jml/checker/jml.y jml.y 735,738c735,744 < local_modifiers < : local_modifier < | local_modifiers local_modifier < ; --- > //local_modifiers > // : local_modifier > // | local_modifiers local_modifier > // ; > > //local_modifier > // : T_FINAL > // | MODEL // added for JML > // | GHOST // added for JML > // ; 740,744c746,747 < local_modifier < : T_FINAL < | MODEL // added for JML < | GHOST // added for JML < ; --- > // JvdB: the nonterminals local_modifiers and local_modifier have become > // obsolete. 749c752,757 < | local_modifiers type variable_declarator_list --- > > // I have replaced local_modifier into jml_modifier. Here we want > // to add a semantic check such that the jml_modifier is one of > // T_FINAL, MODEL, GHOST > > | jml_modifier type variable_declarator_list 1527,1530c1535 < : PUBLIC_EXAMPLE < | PRIVATE_EXAMPLE < | PROTECTED_EXAMPLE < | EXAMPLE --- > : modifiers_opt EXAMPLE 1534,1537c1539 < : PUBLIC_EXCEPTIONAL_EXAMPLE < | PRIVATE_EXCEPTIONAL_EXAMPLE < | PROTECTED_EXCEPTIONAL_EXAMPLE < | EXCEPTIONAL_EXAMPLE --- > : modifiers_opt EXCEPTIONAL_EXAMPLE 1541,1544c1543 < : PUBLIC_NORMAL_EXAMPLE < | PRIVATE_NORMAL_EXAMPLE < | PROTECTED_NORMAL_EXAMPLE < | NORMAL_EXAMPLE --- > : modifiers_opt NORMAL_EXAMPLE 1636,1639c1635 < : PUBLIC_BEHAVIOR < | PRIVATE_BEHAVIOR < | PROTECTED_BEHAVIOR < | BEHAVIOR --- > : modifiers_opt BEHAVIOR 1643,1646c1639 < : PUBLIC_EXCEPTIONAL_BEHAVIOR < | PRIVATE_EXCEPTIONAL_BEHAVIOR < | PROTECTED_EXCEPTIONAL_BEHAVIOR < | EXCEPTIONAL_BEHAVIOR --- > : modifiers_opt EXCEPTIONAL_BEHAVIOR 1650,1653c1643 < : PUBLIC_NORMAL_BEHAVIOR < | PRIVATE_NORMAL_BEHAVIOR < | PROTECTED_NORMAL_BEHAVIOR < | NORMAL_BEHAVIOR --- > : modifiers_opt NORMAL_BEHAVIOR 1711,1714c1701 < : PUBLIC_MODEL_PROGRAM < | PRIVATE_MODEL_PROGRAM < | PROTECTED_MODEL_PROGRAM < | MODEL_PROGRAM --- > : modifiers_opt MODEL_PROGRAM %{ // @(#)$Id: jml.y,v 1.47 2000/07/30 20:53:46 leavens Exp $ // Copyright (C) 1998, 1999 Iowa State University // This file is part of JML // JML is free software; you can redistribute it and/or modify // it under the terms of the GNU General Public License as published by // the Free Software Foundation; either version 2, or (at your option) // any later version. // JML is distributed in the hope that it will be useful, // but WITHOUT ANY WARRANTY; without even the implied warranty of // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the // GNU General Public License for more details. // You should have received a copy of the GNU General Public License // along with JML; see the file COPYING. If not, write to // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA. // The grammar below is adapted from the first edition of // "The Java Language Specification" by Gosling, Joy, and Steele. // The following is an LALR Parser grammar for JML. // // AUTHORS: Clyde Ruby, Gary T. Leavens // *********************************************************************** // This parser assumes that the lexer ignores documentation comments. %} %start goal /* JML Keywords and Tokens added from ESC/Java */ %token AXIOM %token DECREASES %token DECREASES_REDUNDANTLY %token ELEMTYPE /* \elemtype */ %token EXSURES %token EXSURES_REDUNDANTLY %token GHOST %token LBLNEG /* \lblneg */ %token LBLPOS /* \lblpos */ %token LOCKSET /* \lockset */ %token LOOP_INVARIANT %token LOOP_INVARIANT_REDUNDANTLY %token MONITORED %token MONITORED_BY %token NONNULLELEMENTS /* \nonnullelements */ %token READABLE_IF %token SET %token SPEC_PROTECTED %token SPEC_PUBLIC %token TYPE /* \type */ %token TYPEOF /* \typeof */ %token TYPEOFALLTYPES /* \TYPE */ %token UNINITIALIZED %token IS_SUBTYPE_OF /* <: */ /* JML Keywords */ %token ACCESSIBLE %token ACCESSIBLE_REDUNDANTLY %token ALSO %token AND %token ASSERT %token ASSERT_REDUNDANTLY %token ASSUME %token ASSUME_REDUNDANTLY %token BECAUSE %token BECAUSE_REDUNDANTLY %token BEHAVIOR %token CALLABLE %token CALLABLE_REDUNDANTLY %token CHOOSE %token CHOOSE_IF %token CONSTRAINT %token CONSTRAINT_REDUNDANTLY %token DECREASING %token DECREASING_REDUNDANTLY %token DEPENDS %token DEPENDS_REDUNDANTLY %token DIVERGES %token DIVERGES_REDUNDANTLY %token ENSURES %token ENSURES_REDUNDANTLY %token EXAMPLE %token EXCEPTIONAL_BEHAVIOR %token EXCEPTIONAL_EXAMPLE %token FOR_EXAMPLE %token IMPLIES_THAT %token INFORMAL_DESCRIPTION %token INITIALIZER %token INITIALLY %token INSTANCE %token INVARIANT %token INVARIANT_REDUNDANTLY %token LET %token MAINTAINING %token MAINTAINING_REDUNDANTLY %token MEASURED_BY %token MEASURED_BY_REDUNDANTLY %token MODEL %token MODEL_PROGRAM %token MODIFIABLE %token MODIFIABLE_REDUNDANTLY %token NORMAL_BEHAVIOR %token NORMAL_EXAMPLE %token OR %token PRIVATE_BEHAVIOR %token PRIVATE_EXAMPLE %token PRIVATE_EXCEPTIONAL_BEHAVIOR %token PRIVATE_EXCEPTIONAL_EXAMPLE %token PRIVATE_MODEL_PROGRAM %token PRIVATE_NORMAL_BEHAVIOR %token PRIVATE_NORMAL_EXAMPLE %token PROTECTED_BEHAVIOR %token PROTECTED_EXAMPLE %token PROTECTED_EXCEPTIONAL_BEHAVIOR %token PROTECTED_EXCEPTIONAL_EXAMPLE %token PROTECTED_MODEL_PROGRAM %token PROTECTED_NORMAL_BEHAVIOR %token PROTECTED_NORMAL_EXAMPLE %token PUBLIC_BEHAVIOR %token PUBLIC_EXAMPLE %token PUBLIC_EXCEPTIONAL_BEHAVIOR %token PUBLIC_EXCEPTIONAL_EXAMPLE %token PUBLIC_MODEL_PROGRAM %token PUBLIC_NORMAL_BEHAVIOR %token PUBLIC_NORMAL_EXAMPLE %token PURE %token REFINE %token REPRESENTS %token REPRESENTS_REDUNDANTLY %token REQUIRES %token REQUIRES_REDUNDANTLY %token SIGNALS %token SIGNALS_REDUNDANTLY %token STATIC_INITIALIZER %token SUBCLASSING_CONTRACT %token WEAKLY %token WHEN %token WHEN_REDUNDANTLY %token EVERYTHING /* \everything */ %token EXISTS /* \exists */ %token FIELDS_OF /* \fields_of */ %token FORALL /* \forall */ %token FRESH /* \fresh */ %token NOT_MODIFIED /* \not_modified */ %token NOT_SPECIFIED /* \not_specified */ %token NOTHING /* \nothing */ %token OLD /* \old */ %token OTHER /* \other */ %token REACH /* \reach */ %token RESULT /* \result */ %token SUCH_THAT /* \such_that */ %token L_EQUIV /* <==> */ %token L_IMPLIES /* ==> */ %token L_CONSEQUENCE /* <== */ %token L_ARROW /* <- */ %token R_ARROW /* -> */ %token T_DOT_DOT /* .. */ %token T_LCURLY_LBRACK T_RBRACK_RCURLY /* Java Keywords */ %token T_ABSTRACT %token T_BOOLEAN %token T_BREAK %token T_BYTE %token T_CASE %token T_CATCH %token T_CHAR %token T_CLASS %token T_CONTINUE %token T_DEFAULT %token T_DO %token T_DOUBLE %token T_ELSE %token T_EXTENDS %token T_FALSE %token T_FINAL %token T_FINALLY %token T_FLOAT %token T_FOR %token T_IF %token T_IMPLEMENTS %token T_IMPORT %token T_INT %token T_INTERFACE %token T_LONG %token T_NATIVE %token T_NEW %token T_NULL %token T_PACKAGE %token T_PRINT %token T_PRINTLN %token T_PRIVATE %token T_PROTECTED %token T_PUBLIC %token T_RETURN %token T_SHORT %token T_STATIC %token T_STRICTFP %token T_SUPER %token T_SWITCH %token T_SYNCHRONIZED %token T_THIS %token T_THREADSAFE %token T_THROW %token T_THROWS %token T_TRANSIENT %token T_TRUE %token T_TRY %token T_VOID %token T_VOLATILE %token T_WHILE %token T_SYNTAX_ERROR /* constants and identifiers */ %token T_IDENT %token T_CHAR_LITERAL %token T_FLOAT_LITERAL %token T_INT_LITERAL %token T_STRING_LITERAL /* miscellaneous operators */ %token T_COLON T_COMMA T_DOT T_SEMI %token T_LPAREN T_RPAREN %token T_LBRACK T_RBRACK %token T_LCURLY T_RCURLY /* operators, with precedence info */ %right T_ASSIGN T_PLUS_ASSIGN T_MINUS_ASSIGN T_MULT_ASSIGN T_DIV_ASSIGN T_MOD_ASSIGN T_SHL_ASSIGN T_SHR_ASSIGN T_USHR_ASSIGN T_BAND_ASSIGN T_BXOR_ASSIGN T_BOR_ASSIGN %right T_QUEST T_COLON %left T_LOR %left T_LAND %left T_BOR %left T_BXOR %left T_BAND %left T_EQ T_NE %nonassoc T_GT T_LT T_GE T_LE T_INSTANCEOF %left T_SHL T_SHR T_USHR %left T_PLUS T_MINUS %left T_MULT T_DIV T_MOD %right T_NOT T_BNOT %nonassoc T_PLUS_PLUS T_MINUS_MINUS %left T_DOT %nonassoc T_NEW %nonassoc T_LBRACK T_RBRACK T_LPAREN T_RPAREN %% goal : compilation_unit ; literal : T_INT_LITERAL | T_FLOAT_LITERAL | T_TRUE | T_FALSE | T_STRING_LITERAL | T_NULL | T_CHAR_LITERAL ; class_literal : primitive_type T_DOT T_CLASS // added in java 1.1 | T_VOID T_DOT T_CLASS // added in java 1.1 | name T_DOT T_CLASS // added in java 1.1 // (class_or_interface_name) ; // ******************** Types **************************************** type : primitive_type | reference_type | TYPEOFALLTYPES // added from ESC/Java ; primitive_type : numeric_type | T_BOOLEAN ; numeric_type : integral_type | floating_point_type ; integral_type : T_BYTE | T_SHORT | T_INT | T_LONG | T_CHAR ; floating_point_type : T_FLOAT | T_DOUBLE ; reference_type : class_or_interface_type | array_type ; class_or_interface_type : name ; class_type : name ; interface_type : name ; array_type : primitive_type T_LBRACK T_RBRACK | name T_LBRACK T_RBRACK | array_type T_LBRACK T_RBRACK ; // ******************** Names **************************************** name : simple_name | qualified_name ; simple_name : T_IDENT ; qualified_name : name T_DOT T_IDENT ; // ******************** Packages **************************************** compilation_unit : package_declaration_opt refine_prefix_opt // added for JML import_declaration_seq type_declaration_seq_opt | package_declaration_opt refine_prefix_opt // added for JML type_declaration_seq_opt | error ; import_declaration_seq : import_declaration | import_declaration_seq import_declaration ; type_declaration_seq_opt : | type_declaration_seq ; type_declaration_seq : type_declaration | type_declaration_seq type_declaration ; package_declaration_opt : | package_declaration ; package_declaration : T_PACKAGE package_name T_SEMI ; package_name : T_IDENT | package_name T_DOT T_IDENT ; import_declaration : model_opt T_IMPORT name T_SEMI | model_opt T_IMPORT name T_DOT T_MULT T_SEMI ; /* import_name : T_IDENT | import_name T_DOT T_IDENT ; */ type_declaration : class_declaration | interface_declaration | T_SEMI ; modifiers_opt : | modifiers ; modifiers : modifier | modifiers modifier ; modifier : T_PUBLIC | T_PROTECTED | T_PRIVATE | T_STATIC | T_ABSTRACT | T_FINAL | T_NATIVE | T_SYNCHRONIZED | T_TRANSIENT | T_VOLATILE | T_STRICTFP | T_THREADSAFE | jml_modifier // added for JML ; // ************************ Classes ************************************* class_declaration : class_header class_body ; class_header : modifiers_opt T_CLASS T_IDENT extends_clause_opt implements_clause_opt ; extends_clause_opt : | T_EXTENDS class_type weakly_opt ; implements_clause_opt : | T_IMPLEMENTS interface_type_list ; interface_type_list : interface_type weakly_opt | interface_type_list T_COMMA interface_type weakly_opt ; class_body : T_LCURLY class_body_declaration_seq_opt T_RCURLY ; class_body_declaration_seq_opt : | class_body_declaration_seq ; class_body_declaration_seq : class_body_declaration | class_body_declaration_seq class_body_declaration ; class_body_declaration : field_declaration | method_specification method_declaration | method_declaration | method_specification constructor_declaration | constructor_declaration | T_SEMI | method_specification STATIC_INITIALIZER | method_specification INITIALIZER | method_specification static_initializer | static_initializer | method_specification instance_initializer // added for JML | instance_initializer // added in java 1.1 | class_declaration // added in java 1.1 | interface_declaration // added in java 1.1 | jml_declaration // added for JML | error ; // ******************* Field Declarations ***************************** field_declaration : modifiers_opt type variable_declarator_list jml_var_assertion_opt // added for JML T_SEMI ; variable_declarator_list : variable_declarator | variable_declarator_list T_COMMA variable_declarator ; variable_declarator : T_IDENT dims_opt variable_initializer_opt | error ; dims_opt : | dims ; dims : T_LBRACK T_RBRACK | dims T_LBRACK T_RBRACK ; variable_initializer_opt : | T_ASSIGN variable_initializer ; variable_initializer : expression | array_initializer ; // ******************** Method Declarations *********************** method_declaration : method_header method_body ; method_header : modifiers_opt type method_declarator throws_clause_opt | modifiers_opt T_VOID method_declarator throws_clause_opt ; method_declarator : T_IDENT T_LPAREN formal_parameter_list_opt T_RPAREN dims_opt ; formal_parameter_list_opt : | formal_parameter_list ; formal_parameter_list : formal_parameter | formal_parameter_list T_COMMA formal_parameter ; formal_parameter : final_opt type T_IDENT dims_opt | error ; final_opt : | T_FINAL ; throws_clause_opt : | T_THROWS class_type_list ; class_type_list : class_type | class_type_list T_COMMA class_type ; method_body : block | T_SEMI ; // ******************** Class Initializers ************************* static_initializer : T_STATIC block ; instance_initializer // added in java 1.1 : block ; // ******************** Constructor Declarations ******************** constructor_declaration : constructor_header constructor_body ; constructor_header : modifiers_opt constructor_declarator throws_clause_opt ; constructor_declarator : simple_name T_LPAREN formal_parameter_list_opt T_RPAREN ; constructor_body : T_LCURLY explicit_constructor_invocation block_statement_seq_opt T_RCURLY | T_LCURLY block_statement_seq_opt T_RCURLY | T_SEMI ; explicit_constructor_invocation : T_THIS T_LPAREN argument_list_opt T_RPAREN T_SEMI | T_SUPER T_LPAREN argument_list_opt T_RPAREN T_SEMI ; // ******************** Interface Declarations ****************************** interface_declaration : interface_header interface_body ; interface_header : modifiers_opt T_INTERFACE T_IDENT extends_interfaces_opt ; extends_interfaces_opt : | T_EXTENDS interface_type_list ; interface_body : T_LCURLY interface_member_declaration_seq_opt T_RCURLY ; interface_member_declaration_seq_opt : | interface_member_declaration_seq_opt interface_member_declaration ; interface_member_declaration : constant_declaration | method_specification abstract_method_declaration | abstract_method_declaration | class_declaration // added in java 1.1 | interface_declaration // added in java 1.1 | jml_declaration // added for JML | error ; constant_declaration : field_declaration ; abstract_method_declaration : method_header T_SEMI ; // ******************** Arrays **************************************** array_initializer_opt : | array_initializer ; array_initializer : T_LCURLY variable_initializer_list_opt T_RCURLY ; variable_initializer_list_opt : | variable_initializer_list T_COMMA_opt ; variable_initializer_list : variable_initializer | variable_initializer_list T_COMMA variable_initializer ; T_COMMA_opt : | T_COMMA ; // ******************** Blocks and Statements ******************** block : T_LCURLY block_statement_seq_opt T_RCURLY ; block_statement_seq_opt : | block_statement_seq ; block_statement_seq : block_statement | block_statement_seq block_statement ; block_statement : local_variable_declaration T_SEMI | statement | jml_statement // added for JML | error ; //local_modifiers // : local_modifier // | local_modifiers local_modifier // ; //local_modifier // : T_FINAL // | MODEL // added for JML // | GHOST // added for JML // ; // JvdB: the nonterminals local_modifiers and local_modifier have become // obsolete. local_variable_declaration : type variable_declarator_list jml_var_assertion_opt // added for JML // I have replaced local_modifier into jml_modifier. Here we want // to add a semantic check such that the jml_modifier is one of // T_FINAL, MODEL, GHOST | jml_modifier type variable_declarator_list jml_var_assertion_opt // added for JML ; statement : statement_without_trailing_substatement | T_IDENT T_COLON statement | T_IF T_LPAREN expression T_RPAREN statement | T_IF T_LPAREN expression T_RPAREN statement_ns_if T_ELSE statement | loop_invariant_seq_opt variant_function_seq_opt T_WHILE T_LPAREN expression T_RPAREN statement | loop_invariant_seq_opt variant_function_seq_opt T_FOR T_LPAREN for_init_opt T_SEMI expression_opt T_SEMI for_update_opt T_RPAREN statement ; statement_ns_if : statement_without_trailing_substatement | T_IDENT T_COLON statement_ns_if | T_IF T_LPAREN expression T_RPAREN statement_ns_if T_ELSE statement_ns_if | loop_invariant_seq_opt variant_function_seq_opt T_WHILE T_LPAREN expression T_RPAREN statement_ns_if | loop_invariant_seq_opt variant_function_seq_opt T_FOR T_LPAREN for_init_opt T_SEMI expression_opt T_SEMI for_update_opt T_RPAREN statement_ns_if ; statement_without_trailing_substatement : block | T_SEMI | statement_expression T_SEMI | T_SWITCH T_LPAREN expression T_RPAREN switch_block | loop_invariant_seq_opt variant_function_seq_opt T_DO statement T_WHILE T_LPAREN expression T_RPAREN T_SEMI | T_BREAK ident_opt T_SEMI | T_CONTINUE ident_opt T_SEMI | T_RETURN expression_opt T_SEMI | T_SYNCHRONIZED T_LPAREN expression T_RPAREN block | T_THROW expression T_SEMI | try_statement //[[[incorrect]]] | T_PRINT T_LPAREN argument_list_opt T_RPAREN T_SEMI | T_PRINTLN T_LPAREN argument_list_opt T_RPAREN T_SEMI ; ident_opt : | T_IDENT ; statement_expression : assignment | pre_increment_expression | pre_decrement_expression | post_increment_expression | post_decrement_expression | method_invocation | class_instance_creation_expression ; switch_block : T_LCURLY switch_statement_group_seq_opt T_RCURLY ; switch_statement_group_seq_opt : | switch_statement_group_seq ; switch_statement_group_seq : switch_statement_group | switch_statement_group_seq switch_statement_group ; switch_statement_group : switch_label_seq block_statement_seq ; switch_label_seq : switch_label | switch_label_seq switch_label ; switch_label : T_CASE constant_expression T_COLON | T_DEFAULT T_COLON ; for_init_opt : | statement_expression_list | local_variable_declaration ; for_update_opt : | statement_expression_list ; statement_expression_list : statement_expression | statement_expression_list T_COMMA statement_expression ; try_statement : T_TRY block catch_clause_seq | T_TRY block catch_clause_seq_opt T_FINALLY block ; catch_clause_seq_opt : | catch_clause_seq ; catch_clause_seq : catch_clause | catch_clause_seq catch_clause ; catch_clause : T_CATCH T_LPAREN formal_parameter T_RPAREN block ; // ******************** Expressions ******************************** primary : primary_no_new_array | array_creation_expression array_initializer_opt | jml_primary // added for JML ; primary_no_new_array : literal | T_THIS | T_LPAREN expression T_RPAREN | class_instance_creation_expression | field_access | method_invocation | array_access | class_literal // added in java 1.1 // ******************** JML Expressions ***************************** | RESULT | OLD T_LPAREN spec_expression T_RPAREN // ******************** End JML Expressions ************************** ; class_instance_creation_expression : T_NEW class_type T_LPAREN argument_list T_RPAREN | T_NEW class_type T_LPAREN T_RPAREN | T_NEW class_type T_LPAREN T_RPAREN // (class_or_interface_name) anonymous class java 1.1 class_body | primary T_DOT T_NEW T_IDENT T_LPAREN argument_list T_RPAREN // java 1.1 | primary T_DOT T_NEW T_IDENT T_LPAREN T_RPAREN // java 1.1 | primary T_DOT T_NEW T_IDENT T_LPAREN T_RPAREN class_body // anonymous class java 1.1 // ******************** JML Set Comprehension *************************** | T_NEW class_type T_LCURLY type quantified_var_declarator T_BOR predicate T_RCURLY // ******************* End JML Set Comprehension ************************* ; argument_list_opt : | argument_list ; argument_list : expression | argument_list T_COMMA expression ; array_creation_expression : T_NEW primitive_type dim_exprs dims_opt | T_NEW primitive_type dims | T_NEW class_or_interface_type dim_exprs dims_opt | T_NEW class_or_interface_type dims ; dim_exprs : T_LBRACK expression T_RBRACK | dim_exprs T_LBRACK expression T_RBRACK ; field_access : primary T_DOT T_IDENT | T_SUPER T_DOT T_IDENT ; method_invocation : name T_LPAREN argument_list_opt T_RPAREN | primary T_DOT T_IDENT T_LPAREN argument_list_opt T_RPAREN | T_SUPER T_DOT T_IDENT T_LPAREN argument_list_opt T_RPAREN ; array_access : name T_LBRACK expression T_RBRACK | primary_no_new_array T_LBRACK expression T_RBRACK ; postfix_expression : primary | name | post_increment_expression | post_decrement_expression ; post_increment_expression : postfix_expression T_PLUS_PLUS ; post_decrement_expression : postfix_expression T_MINUS_MINUS ; unary_expression : pre_increment_expression | pre_decrement_expression | T_PLUS unary_expression | T_MINUS unary_expression | unary_expression_not_plus_minus ; pre_increment_expression : T_PLUS_PLUS postfix_expression ; pre_decrement_expression : T_MINUS_MINUS postfix_expression ; unary_expression_not_plus_minus : postfix_expression | T_BNOT unary_expression | T_NOT unary_expression | cast_expression ; cast_expression : T_LPAREN primitive_type dims_opt T_RPAREN unary_expression | T_LPAREN expression T_RPAREN unary_expression_not_plus_minus | T_LPAREN name dims T_RPAREN unary_expression_not_plus_minus ; multiplicative_expression : unary_expression | multiplicative_expression T_MULT unary_expression | multiplicative_expression T_DIV unary_expression | multiplicative_expression T_MOD unary_expression ; additive_expression : multiplicative_expression | additive_expression T_PLUS multiplicative_expression | additive_expression T_MINUS multiplicative_expression ; shift_expression : additive_expression | shift_expression T_SHL additive_expression | shift_expression T_SHR additive_expression | shift_expression T_USHR additive_expression ; relational_expression : shift_expression | relational_expression T_LT shift_expression | relational_expression T_GT shift_expression | relational_expression T_LE shift_expression | relational_expression T_GE shift_expression | relational_expression T_INSTANCEOF reference_type // added from ESC/Java | relational_expression IS_SUBTYPE_OF shift_expression ; equality_expression : relational_expression | equality_expression T_EQ relational_expression | equality_expression T_NE relational_expression ; and_expression : equality_expression | and_expression T_BAND equality_expression ; exclusive_or_expression : and_expression | exclusive_or_expression T_BXOR and_expression ; inclusive_or_expression : exclusive_or_expression | inclusive_or_expression T_BOR exclusive_or_expression ; conditional_and_expression : inclusive_or_expression | conditional_and_expression T_LAND inclusive_or_expression ; conditional_or_expression : conditional_and_expression | conditional_or_expression T_LOR conditional_and_expression ; // *************** JML Implication Expressions *************************** consequence_expression : conditional_or_expression | consequence_expression L_CONSEQUENCE conditional_or_expression // associates left ; implies_expression : conditional_or_expression L_IMPLIES conditional_or_expression | conditional_or_expression L_IMPLIES implies_expression // associates right ; implication_expression : implies_expression | consequence_expression ; equivalence_expression : implication_expression | equivalence_expression L_EQUIV implication_expression ; // **************** End JML Implication Expressions ********************** conditional_expression : equivalence_expression | equivalence_expression T_QUEST expression T_COLON conditional_expression ; assignment_expression : conditional_expression | assignment ; assignment : left_hand_side assignment_operator assignment_expression ; left_hand_side : name | field_access | array_access ; assignment_operator : T_ASSIGN | T_MULT_ASSIGN | T_DIV_ASSIGN | T_MOD_ASSIGN | T_PLUS_ASSIGN | T_MINUS_ASSIGN | T_SHL_ASSIGN | T_SHR_ASSIGN | T_USHR_ASSIGN | T_BAND_ASSIGN | T_BXOR_ASSIGN | T_BOR_ASSIGN ; expression_opt : | expression ; expression : assignment_expression | error ; constant_expression : expression ; //---------------------------------------------------------------------------- // *********************** JML Constructs *********************************** //---------------------------------------------------------------------------- COLON_opt : | T_COLON ; weakly_opt : | WEAKLY ; refine_prefix_opt : | REFINE COLON_opt simple_name_list L_ARROW T_STRING_LITERAL T_SEMI ; simple_name_list : simple_name | simple_name_list T_COMMA simple_name ; jml_var_assertion_opt : | INITIALLY COLON_opt predicate | READABLE_IF COLON_opt predicate // added from ESC/Java | monitored_by_clause // added from ESC/Java ; monitored_by_clause : MONITORED_BY COLON_opt argument_list ; predicate : expression ; spec_expression : expression ; // ******************** JML Modifiers ********************************* jml_modifier : MODEL | PURE | INSTANCE // added from ESC/Java | SPEC_PUBLIC | SPEC_PROTECTED | MONITORED | UNINITIALIZED | GHOST ; model_opt : | MODEL ; // ******************** JML Declarations ********************************* jml_declaration : modifiers_opt invariant | modifiers_opt history_constraint | modifiers_opt depends_decl | modifiers_opt represents_decl | axiom_pragma // added from ESC/Java ; invariant : invariant_keyword COLON_opt predicate T_SEMI ; invariant_keyword : INVARIANT | INVARIANT_REDUNDANTLY ; history_constraint : constraint_keyword COLON_opt predicate constrained_list_opt T_SEMI ; constraint_keyword : CONSTRAINT | CONSTRAINT_REDUNDANTLY ; depends_decl : depends_keyword COLON_opt store_ref R_ARROW store_references T_SEMI ; depends_keyword : DEPENDS | DEPENDS_REDUNDANTLY ; represents_decl : represents_keyword COLON_opt store_ref SUCH_THAT predicate T_SEMI | represents_keyword COLON_opt store_ref L_ARROW spec_expression T_SEMI ; represents_keyword : REPRESENTS | REPRESENTS_REDUNDANTLY ; // added from ESC/Java axiom_pragma : AXIOM COLON_opt predicate T_SEMI ; // ******************** JML constrained_list ************************* constrained_list_opt : | constrained_list ; constrained_list : T_FOR method_name_list | T_FOR EVERYTHING ; // ******************** JML method_name_list ************************* method_name_list : method_name | method_name_list T_COMMA method_name ; method_name : method_ref | method_ref T_LPAREN param_disambig_list_opt T_RPAREN | constructor_name ; method_ref : T_IDENT | T_THIS | T_SUPER | method_ref T_DOT T_IDENT ; constructor_name : T_NEW reference_type | T_NEW reference_type T_LPAREN param_disambig_list_opt T_RPAREN ; param_disambig_list_opt : | param_disambig_list ; param_disambig_list : param_disambig | param_disambig_list T_COMMA param_disambig ; param_disambig : type | type T_IDENT dims_opt ; // ********************** JML store_references *************************** conditional_store_references : conditional_store_ref_list ; conditional_store_ref_list : conditional_store_ref | conditional_store_ref_list T_COMMA conditional_store_ref ; conditional_store_ref : store_ref | store_ref T_IF predicate ; store_references : store_ref_list ; store_ref_list : store_ref | store_ref_list T_COMMA store_ref ; store_ref : store_ref_expression | FIELDS_OF T_LPAREN field_args T_RPAREN | INFORMAL_DESCRIPTION | store_ref_keyword ; store_ref_keyword : NOTHING | EVERYTHING | NOT_SPECIFIED ; store_ref_expression : store_ref_name | store_array_access ; store_ref_name : T_IDENT | T_THIS | T_SUPER | store_ref_expression T_DOT T_IDENT ; store_array_access : store_ref_expression T_LBRACK array_index_range T_RBRACK ; array_index_range : spec_expression | spec_expression T_DOT_DOT spec_expression | T_MULT ; field_args : T_SUPER | spec_expression | spec_expression T_COMMA reference_type | spec_expression T_COMMA reference_type T_COMMA store_ref_expression ; // *************** JML Primary Expressions ******************************* jml_primary : NOT_MODIFIED T_LPAREN store_ref_list T_RPAREN | FRESH T_LPAREN argument_list T_RPAREN | REACH T_LPAREN spec_expression T_RPAREN | quantified_expr | INFORMAL_DESCRIPTION // added from ESC/Java | NONNULLELEMENTS T_LPAREN spec_expression T_RPAREN | TYPEOF T_LPAREN spec_expression T_RPAREN | ELEMTYPE T_LPAREN spec_expression T_RPAREN | TYPE T_LPAREN type T_RPAREN | T_LPAREN LBLNEG T_IDENT spec_expression T_RPAREN | T_LPAREN LBLPOS T_IDENT spec_expression T_RPAREN | LOCKSET ; // ************** JML Quantified Expression ****************************** quantified_expr : T_LPAREN quantifier quantified_var_decls predicate T_RPAREN ; quantifier : FORALL | EXISTS ; quantified_var_decls : T_LPAREN quantified_var_decl_seq semi_opt T_RPAREN | type quantified_var_declarator_list semi_opt ; quantified_var_decl_seq : type quantified_var_declarator_list | quantified_var_decl_seq T_SEMI type quantified_var_declarator_list ; quantified_var_declarator_list : quantified_var_declarator | quantified_var_declarator_list T_COMMA quantified_var_declarator ; quantified_var_declarator : T_IDENT dims_opt | error ; semi_opt : | T_SEMI ; // ******************* JML method_specification *************************** method_specification : specification | extending_specification ; specification : spec_case_seq subclassing_contract_opt redundant_spec_opt | subclassing_contract redundant_spec_opt | redundant_spec ; extending_specification : ALSO specification | AND conjoinable_spec_seq subclassing_contract_opt redundant_spec_opt | AND conjoinable_spec_seq ALSO spec_case_seq subclassing_contract_opt redundant_spec_opt ; conjoinable_spec_seq : conjoinable_spec | conjoinable_spec_seq AND conjoinable_spec ; conjoinable_spec : generic_conjoinable_spec | behavior_conjoinable_spec ; generic_conjoinable_spec : model_var_decls_opt simple_spec_body ; behavior_conjoinable_spec : behavior_keyword model_var_decls_opt simple_spec_body | exceptional_behavior_keyword model_var_decls_opt exceptional_simple_spec_body | normal_behavior_keyword model_var_decls_opt normal_simple_spec_body ; exceptional_simple_spec_body : modifiable_clause_seq signals_clause_seq_opt diverges_clause_seq_opt | signals_clause_seq diverges_clause_seq_opt ; normal_simple_spec_body : modifiable_clause_seq ensures_clause_seq_opt diverges_clause_seq_opt | ensures_clause_seq diverges_clause_seq_opt ; // ********************* JML redundant_spec ******************************* redundant_spec_opt : | redundant_spec ; redundant_spec : implications examples_opt | examples ; examples_opt : | examples ; examples : FOR_EXAMPLE example_seq ; example_seq : example | example_seq ALSO example ; example : model_var_decls_opt spec_header_opt simple_spec_body | example_keyword model_var_decls_opt spec_header_opt simple_spec_body | exceptional_example_keyword simple_exceptional_spec | normal_example_keyword simple_normal_spec ; example_keyword : modifiers_opt EXAMPLE ; exceptional_example_keyword : modifiers_opt EXCEPTIONAL_EXAMPLE ; normal_example_keyword : modifiers_opt NORMAL_EXAMPLE ; implications : IMPLIES_THAT spec_case_seq ; // *********************** JML spec_case ********************************* spec_case_seq : spec_case | spec_case_seq ALSO spec_case ; spec_case : generic_spec_case | behavior_spec | model_program ; // ************************ JML subclassing contract ********************* subclassing_contract_opt : | subclassing_contract ; subclassing_contract : SUBCLASSING_CONTRACT accessible_seq_opt callable_seq | SUBCLASSING_CONTRACT accessible_seq ; accessible_seq_opt : | accessible_seq ; accessible_seq : accessible_clause | accessible_seq accessible_clause ; callable_seq : callable_clause | callable_seq callable_clause ; // ******************* JML generic_spec_case **************************** generic_spec_case : model_var_decls_opt spec_header_opt simple_spec_body | model_var_decls_opt spec_header_opt T_LCURLY_LBRACK generic_spec_case_seq T_RBRACK_RCURLY | model_var_decls_opt spec_header ; generic_spec_case_seq : generic_spec_case | generic_spec_case_seq ALSO generic_spec_case ; spec_header_opt : | spec_header ; spec_header : requires_clause_seq_opt when_clause_seq_opt measured_clause_seq | requires_clause_seq_opt when_clause_seq | requires_clause_seq ; simple_spec_body : modifiable_clause_seq_opt ensures_clause_seq_opt signals_clause_seq_opt diverges_clause_seq | modifiable_clause_seq_opt ensures_clause_seq_opt signals_clause_seq | modifiable_clause_seq_opt ensures_clause_seq | modifiable_clause_seq ; // ********************* JML behavior_spec ****************************** behavior_spec : behavior_keyword generic_spec_case | exceptional_behavior_keyword exceptional_spec_case | normal_behavior_keyword normal_spec_case ; behavior_keyword : modifiers_opt BEHAVIOR ; exceptional_behavior_keyword : modifiers_opt EXCEPTIONAL_BEHAVIOR ; normal_behavior_keyword : modifiers_opt NORMAL_BEHAVIOR ; // ****************** JML exceptional_spec_case ************************* exceptional_spec_case : simple_exceptional_spec | model_var_decls_opt spec_header_opt T_LCURLY_LBRACK exceptional_spec_case_seq T_RBRACK_RCURLY ; simple_exceptional_spec : model_var_decls_opt spec_header_opt modifiable_clause_seq_opt signals_clause_seq diverges_clause_seq_opt | model_var_decls_opt spec_header_opt modifiable_clause_seq diverges_clause_seq_opt | model_var_decls_opt spec_header diverges_clause_seq_opt ; exceptional_spec_case_seq : exceptional_spec_case | exceptional_spec_case_seq ALSO exceptional_spec_case ; // ******************** JML normal_spec_case **************************** normal_spec_case : simple_normal_spec | model_var_decls_opt spec_header_opt T_LCURLY_LBRACK normal_spec_case_seq T_RBRACK_RCURLY ; simple_normal_spec : model_var_decls_opt spec_header_opt modifiable_clause_seq_opt ensures_clause_seq diverges_clause_seq_opt | model_var_decls_opt spec_header_opt modifiable_clause_seq diverges_clause_seq_opt | model_var_decls_opt spec_header diverges_clause_seq_opt ; normal_spec_case_seq : normal_spec_case | normal_spec_case_seq ALSO normal_spec_case ; // ********************* JML model_program ******************************* model_program : model_program_keyword jml_compound_statement | model_program_keyword T_LCURLY explicit_constructor_invocation jml_block_statement_seq_opt T_RCURLY ; model_program_keyword : modifiers_opt MODEL_PROGRAM ; jml_compound_statement : T_LCURLY jml_block_statement_seq_opt T_RCURLY ; jml_block_statement_seq_opt : | jml_block_statement_seq ; jml_block_statement_seq : jml_block_statement | jml_block_statement_seq jml_block_statement ; jml_block_statement : block_statement | jml_spec_statement ; // *********************** JML Statements ******************************* jml_statement : because_statement // added for JML | assert_statement // added for JML | assume_statement // added for JML | set_statement // added from ESC/Java (JML) ; because_statement : because_keyword COLON_opt predicate T_SEMI ; because_keyword : BECAUSE | BECAUSE_REDUNDANTLY ; assert_statement : assert_keyword COLON_opt predicate T_SEMI ; assert_keyword : ASSERT | ASSERT_REDUNDANTLY ; assume_statement : assume_keyword COLON_opt predicate T_SEMI ; assume_keyword : ASSUME | ASSUME_REDUNDANTLY ; set_statement : SET COLON_opt assignment T_SEMI ; jml_spec_statement : nondeterministic_choice | nondeterministic_if | behavior_spec | invariant ; nondeterministic_choice : CHOOSE alternative_statements ; alternative_statements : jml_compound_statement | alternative_statements OR jml_compound_statement ; nondeterministic_if : CHOOSE_IF guarded_statements | CHOOSE_IF guarded_statements T_ELSE jml_compound_statement ; guarded_statements : guarded_statement | guarded_statements OR guarded_statement ; guarded_statement : T_LCURLY assume_statement jml_block_statement_seq_opt T_RCURLY ; // ******************** JML Loop Assertions ************************* loop_invariant_seq_opt : | loop_invariant_seq ; loop_invariant_seq : loop_invariant | loop_invariant_seq loop_invariant ; loop_invariant : loop_invariant_keyword COLON_opt predicate T_SEMI ; loop_invariant_keyword : MAINTAINING | MAINTAINING_REDUNDANTLY | LOOP_INVARIANT | LOOP_INVARIANT_REDUNDANTLY ; variant_function_seq_opt : | variant_function_seq ; variant_function_seq : variant_function | variant_function_seq variant_function ; variant_function : variant_keyword COLON_opt spec_expression T_SEMI ; variant_keyword : DECREASING | DECREASING_REDUNDANTLY | DECREASES | DECREASES_REDUNDANTLY ; // ******************** JML callable_clause ******************************* callable_clause : callable_keyword COLON_opt callable_methods T_SEMI ; callable_keyword : CALLABLE | CALLABLE_REDUNDANTLY ; callable_methods : callable_method_list | store_ref_keyword ; callable_method_list : callable_method | callable_method_list T_COMMA callable_method ; callable_method : method_name | other_ref_name | other_ref_name T_LPAREN param_disambig_list_opt T_RPAREN ; // ******************* JML accessible_clause ***************************** accessible_clause : accessible_keyword COLON_opt object_references T_SEMI ; accessible_keyword : ACCESSIBLE | ACCESSIBLE_REDUNDANTLY ; object_references : object_ref_list | store_ref_keyword ; object_ref_list : object_ref | object_ref_list T_COMMA object_ref ; object_ref : store_ref_expression | other_ref_expression ; other_ref_expression : other_array_access | other_ref_name ; other_ref_name : OTHER | other_ref_expression T_DOT T_IDENT ; other_array_access : other_ref_expression T_LBRACK array_index_range T_RBRACK ; // ******************** JML model_var_decls ****************************** model_var_decls_opt : | model_var_decls ; model_var_decls : LET model_var_decl_seq ; model_var_decl_seq : model_var_decl | model_var_decl_seq model_var_decl ; model_var_decl : MODEL type variable_declarator_list jml_var_assertion_opt // added for JML T_SEMI ; // ********************* JML requires_clause ***************************** requires_clause_seq_opt : | requires_clause_seq ; requires_clause_seq : requires_clause | requires_clause_seq requires_clause ; requires_clause : requires_keyword COLON_opt pre_cond T_SEMI ; requires_keyword : REQUIRES | REQUIRES_REDUNDANTLY ; pre_cond : predicate | NOT_SPECIFIED ; // ********************** JML when_clause ******************************* when_clause_seq_opt : | when_clause_seq ; when_clause_seq : when_clause | when_clause_seq when_clause ; when_clause : when_keyword COLON_opt predicate T_SEMI | when_keyword COLON_opt NOT_SPECIFIED T_SEMI ; when_keyword : WHEN | WHEN_REDUNDANTLY ; // ******************* JML measured_clause ****************************** measured_clause_seq : measured_clause | measured_clause_seq measured_clause ; measured_clause : measured_by_keyword COLON_opt spec_expression T_SEMI | measured_by_keyword COLON_opt spec_expression T_IF predicate T_SEMI | measured_by_keyword COLON_opt NOT_SPECIFIED T_SEMI ; measured_by_keyword : MEASURED_BY | MEASURED_BY_REDUNDANTLY ; // ***************** JML modifiable_clause ****************************** modifiable_clause_seq_opt : | modifiable_clause_seq ; modifiable_clause_seq : modifiable_clause | modifiable_clause_seq modifiable_clause ; modifiable_clause : modifiable_keyword COLON_opt conditional_store_references T_SEMI ; modifiable_keyword : MODIFIABLE | MODIFIABLE_REDUNDANTLY ; // ******************* JML ensures_clause ******************************* ensures_clause_seq_opt : | ensures_clause_seq ; ensures_clause_seq : ensures_clause | ensures_clause_seq ensures_clause ; ensures_clause : ensures_keyword COLON_opt post_cond T_SEMI ; ensures_keyword : ENSURES | ENSURES_REDUNDANTLY ; post_cond : predicate | NOT_SPECIFIED ; // ******************** JML signals_clause ****************************** signals_clause_seq_opt : | signals_clause_seq ; signals_clause_seq : signals_clause | signals_clause_seq signals_clause ; signals_clause : signals_keyword COLON_opt signals_exception_decl signals_predicate_opt T_SEMI ; signals_keyword : SIGNALS | SIGNALS_REDUNDANTLY | EXSURES | EXSURES_REDUNDANTLY ; signals_exception_decl : T_LPAREN reference_type ident_opt T_RPAREN ; signals_predicate_opt : | predicate | NOT_SPECIFIED ; // ******************** JML diverges_clause ****************************** diverges_clause_seq_opt : | diverges_clause_seq ; diverges_clause_seq : diverges_clause | diverges_clause_seq diverges_clause ; diverges_clause : diverges_keyword COLON_opt predicate T_SEMI | diverges_keyword COLON_opt NOT_SPECIFIED T_SEMI ; diverges_keyword : DIVERGES | DIVERGES_REDUNDANTLY ; %%  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Fri Aug 25 09:18:00 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id JAA21153 for jml-interest-list-outgoing; Fri, 25 Aug 2000 09:17:51 -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 JAA21140; Fri, 25 Aug 2000 09:17:40 -0500 (CDT) Received: (from leavens@localhost) by ren.cs.iastate.edu (8.9.0/8.9.0) id JAA04487; Fri, 25 Aug 2000 09:17:36 -0500 (CDT) Date: Fri, 25 Aug 2000 09:17:36 -0500 (CDT) Message-Id: <200008251417.JAA04487@ren.cs.iastate.edu> From: "Gary T. Leavens" To: joachim@cicero.cs.kun.nl Sent-via: joachim@cicero.cs.kun.nl CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu Sent-via: jml-interest-list@cs.iastate.edu, leavens In-reply-to: (message from Joachim van den Berg on Fri, 25 Aug 2000 15:03:10 +0200 (CEST)) Subject: JML-Interest: Re: 'bug' fix in the jml grammar References: Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Fri, 25 Aug 2000 09:17:36 -0500 (CDT) From: "Gary T. Leavens" To: joachim@cicero.cs.kun.nl Sent-via: joachim@cicero.cs.kun.nl CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu Sent-via: jml-interest-list@cs.iastate.edu, leavens In-reply-to: (message from Joachim van den Berg on Fri, 25 Aug 2000 15:03:10 +0200 (CEST)) Subject: JML-Interest: Re: 'bug' fix in the jml grammar Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Joachim, > Date: Fri, 25 Aug 2000 15:03:10 +0200 (CEST) > From: Joachim van den Berg > cc: jml-interest-list@cs.iastate.edu > Content-Type: TEXT/PLAIN; charset=US-ASCII > Today also, I tried to fix an ugly thing in the jml grammar, concerning the > behavior, example, and model_program keywords. I was not happy (for you > probably the same holds) about the explosion of these keywords. So, I fixed > this problem. I've included a grammar where these keywords carry an access > modifier, just as in Java. With this grammar specifications are of the form > (if I am up-to-date. Didn't do JML for a while): > > /*@ public normal_behavior > @ requires: P; > @ ... > @*/ > public abstract void m(); > > where the access modifier in the specification is optional. The compiler > should do some checks to guarantee that the modifiers are used in a proper > way (just as the Java compiler does). > > I hope that you are happy with this solution and that we can implement this > in JML. What do you think? We were able to get that to work in a LALR (bottom up) parser like yacc, as you have apparently, but not in our LL (top down) tool, ANTLR. Since we use ANTLR for the main tool, and since we want people to be able to use bottom up parsing techniques, Clyde and I thought that the public_ ... keywords were the only viable solution. But if you can get it to work in ANTLR, then I'd be happy to make that grammar change. Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Fri Aug 25 09:28:45 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id JAA21487 for jml-interest-list-outgoing; Fri, 25 Aug 2000 09:28:42 -0500 (CDT) 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 JAA21483 for ; Fri, 25 Aug 2000 09:28:39 -0500 (CDT) Received: from hera.cs.kun.nl by pandora.cs.kun.nl via hera.cs.kun.nl [131.174.33.2] with ESMTP for id QAA12952 (8.8.8/3.12); Fri, 25 Aug 2000 16:28:33 +0200 (MET DST) Message-Id: <200008251428.QAA12952@pandora.cs.kun.nl> X-Mailer: exmh version 2.1.1 10/15/1999 To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: Re: example and problems with partial expressions in JML? In-reply-to: Your message of "Tue, 15 Aug 2000 23:43:40 CDT." <200008160443.XAA23625@ren.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Fri, 25 Aug 2000 16:28:33 +0200 From: Bart Jacobs Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: Re: example and problems with partial expressions in JML? In-reply-to: Your message of "Tue, 15 Aug 2000 23:43:40 CDT." <200008160443.XAA23625@ren.cs.iastate.edu> Content-Type: text/plain; charset=us-ascii Date: Fri, 25 Aug 2000 16:28:33 +0200 From: Bart Jacobs Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi Gary, > > Well, the half-deep approach is intuitively quite clear: > > with it, JML's non-boolean computations are done as in Java, > > and JML's logic is as in ordinary logic. > > It's okay and makes sense to me, but I still worry a bit as before. > I guess if you can't find problems with it, then I shouldn't worry too > much :-). Fine, then we will start implementing this, and using it in our verifications. > We could perhaps side-step the issue if we could guarantee that the > formulas were protective in some sense. That would be essentially > adopting a different approach, however. Yes, and an approach with extra proof obligations, which does not make us happy (as verifiers). A slightly different topic. In our specification work we found it useful to have two extra keywords in JML. Something like: 1. \invariantof(a, A), expressing that the invariant of class A holds for the object a. 2. \isinitialized(A) expressing static initialization has taken place for class A. We are open to alternative syntax. The first predicate requires a typecheck: a must have a reference type, which can be converted (via widening or narrowing) to A. The second predicate is sometimes needed because the result of a computation can depend on whether static initialization still has to take place. Now this cannot be expressed in JML. The first predicate is needed in situations like the following. class A { B b; int i; //@ invariant: i >= 0 && \invariantof(b, B); //@ requires: o instanceof B ==> \invariantof(o, B); void m(Object o) { ... (B)o ... }; //@ ensures: \invariantof(\result, A); Object clone() { ... } } There is a subtle point because using \invariantof in an invariant clause might give loops, if there is an (indirect) use of \invariantof of A in the invariant of class A. It is not clear what this means then. The generated PVS code will give a typecheck error. Please let us know what you think about this. Best, Joachim & Bart.  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Fri Aug 25 10:39:16 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id KAA23574 for jml-interest-list-outgoing; Fri, 25 Aug 2000 10:39:08 -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 KAA23565; Fri, 25 Aug 2000 10:38:55 -0500 (CDT) Received: (from leavens@localhost) by ren.cs.iastate.edu (8.9.0/8.9.0) id KAA06586; Fri, 25 Aug 2000 10:38:51 -0500 (CDT) Date: Fri, 25 Aug 2000 10:38:51 -0500 (CDT) Message-Id: <200008251538.KAA06586@ren.cs.iastate.edu> From: "Gary T. Leavens" To: Bart.Jacobs@cs.kun.nl CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: <200008251428.QAA12952@pandora.cs.kun.nl> (message from Bart Jacobs on Fri, 25 Aug 2000 16:28:33 +0200) Subject: Re: JML-Interest: Re: example and problems with partial expressions in JML? References: <200008251428.QAA12952@pandora.cs.kun.nl> Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Fri, 25 Aug 2000 10:38:51 -0500 (CDT) From: "Gary T. Leavens" To: Bart.Jacobs@cs.kun.nl CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: <200008251428.QAA12952@pandora.cs.kun.nl> (message from Bart Jacobs on Fri, 25 Aug 2000 16:28:33 +0200) Subject: Re: JML-Interest: Re: example and problems with partial expressions in JML? Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Dear Bart, > Date: Fri, 25 Aug 2000 16:28:33 +0200 > From: Bart Jacobs > > > > Well, the half-deep approach is intuitively quite clear: > > > with it, JML's non-boolean computations are done as in Java, > > > and JML's logic is as in ordinary logic. > > > > It's okay and makes sense to me, but I still worry a bit as before. > > I guess if you can't find problems with it, then I shouldn't worry too > > much :-). > > Fine, then we will start implementing this, and using > it in our verifications. Ok. Let me know if problems appear... > > We could perhaps side-step the issue if we could guarantee that the > > formulas were protective in some sense. That would be essentially > > adopting a different approach, however. > > Yes, and an approach with extra proof obligations, which > does not make us happy (as verifiers). I think protection is a good idea for the specifier, even if makes more work in checking the validity of the specification. I think that after the specification has been certified as protective, to verify an implementation one would not need to verify its protection again. (Perhaps we need proof-carrying specifications. :-) So I see this extra proof obligation as not the responsibility of the person verifying an implementation. There are certainly other proof obligations that have such a flavor in JML, for example, all of the implies_that section is proof obligations for the specification, which don't impact the verification of an implementation. > A slightly different topic. In our specification work we > found it useful to have two extra keywords in JML. > Something like: > > 1. \invariantof(a, A), expressing that the invariant of class > A holds for the object a. > 2. \isinitialized(A) expressing static initialization has taken > place for class A. > > We are open to alternative syntax. The first predicate requires > a typecheck: a must have a reference type, which can be converted > (via widening or narrowing) to A. Wouldn't "a" have to be a subtype of A? I'm not sure I understand what you mean by "narrowing", but if you mean the equivalent of a downcast, I'd be against that; let the cast appear in the expression itself if need be. I don't think A needs to be a class type (interfaces may also have invariants). Which invariant are we refering to here? I presume this is the public invariant? Would we need the same for history constraints? > The first predicate is needed in situations like the following. > > class A { > > B b; > int i; > > //@ invariant: i >= 0 && \invariantof(b, B); > > //@ requires: o instanceof B ==> \invariantof(o, B); > void m(Object o) { > ... (B)o ... }; > > //@ ensures: \invariantof(\result, A); > Object clone() { ... } > > } I would rather write for the requires clause above: //@ requires: o instanceof B ==> \invariantof((B)o, B); so that the downcast is explicit. I've always thought of the public invariant of a class as something you can assume whenever you need it. (Formally, it's part of the theory you use to do proofs.) So that if o is an instance of B, then o does satisfy B's public invariant, unless we are inside one of the public operations of B. Hence this requires clause doesn't add any new information (and could thus be redundant). But perhaps it's helpful to make these explicit? I guess adding an axiom that says the invariant always holds may cause problems in verification of methods of the class itself, where the invariant won't always hold. Is that the problem? Rustan's work doesn't use invariants at all, but just has the programmer state the properties explicitly everyplace. > There is a subtle point because using \invariantof in an > invariant clause might give loops, if there is an (indirect) > use of \invariantof of A in the invariant of class A. It is not > clear what this means then. The generated PVS code will give > a typecheck error. That could be avoided using a type system like PVS's, i.e., by doing static checks. > The second predicate is sometimes needed because the result of > a computation can depend on whether static initialization > still has to take place. Now this cannot be expressed in > JML. Yes, I can see that I think \isinitialized is noncontroversial, and should be added to JML. Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Fri Aug 25 11:43:48 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id LAA25951 for jml-interest-list-outgoing; Fri, 25 Aug 2000 11:43:44 -0500 (CDT) 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 LAA25946; Fri, 25 Aug 2000 11:43:40 -0500 (CDT) Received: from localhost (joachim@localhost) by cicero.cs.kun.nl (8.9.3/8.9.3) with ESMTP id SAA22370; Fri, 25 Aug 2000 18:38:33 +0200 Date: Fri, 25 Aug 2000 18:38:30 +0200 (CEST) From: Joachim van den Berg To: "Gary T. Leavens" cc: Bart.Jacobs@cs.kun.nl, jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: Re: example and problems with partial expressions in JML? In-Reply-To: <200008251538.KAA06586@ren.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: Fri, 25 Aug 2000 18:38:30 +0200 (CEST) From: Joachim van den Berg To: "Gary T. Leavens" cc: Bart.Jacobs@cs.kun.nl, jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: Re: example and problems with partial expressions in JML? In-Reply-To: <200008251538.KAA06586@ren.cs.iastate.edu> Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Dear Gary, > > A slightly different topic. In our specification work we > > found it useful to have two extra keywords in JML. > > Something like: > > > > 1. \invariantof(a, A), expressing that the invariant of class > > A holds for the object a. > > 2. \isinitialized(A) expressing static initialization has taken > > place for class A. > > > > We are open to alternative syntax. The first predicate requires > > a typecheck: a must have a reference type, which can be converted > > (via widening or narrowing) to A. > > Wouldn't "a" have to be a subtype of A? I'm not sure I understand what > you mean by "narrowing", but if you mean the equivalent of a downcast, > I'd be against that; let the cast appear in the expression itself if > need be. > Narrowing is not completely equivalent to downcasting. Narrowing only says something about whether a type can be narrowed to another type (and will never raise an exception, whereas downcasting might do so). More on this below... > I don't think A needs to be a class type (interfaces may also have > invariants). Yes, you're right. 'A' should be a class type or an interface. > > Which invariant are we refering to here? I presume this is the public > invariant? Would we need the same for history constraints? I think we should implement the same strategy Java uses to determine accessibility (described on page 99, JLS 1st edition). I guess that we need something similar for history constraints. > I would rather write for the requires clause above: > > //@ requires: o instanceof B ==> \invariantof((B)o, B); > > so that the downcast is explicit. Ok, this is also a possibility. But in this case I would say that \invariantof only has one parameter, namely ((B)o) . The invariant can then be determined from the static type of its parameter. I believe that is even better. (One cannot write nonsense anymore, such as \invariantof((B)o, C), where B and C have no relation at all) So my proposal would be: //@ requires: o instanceof B ==> \invariantof((B)o); > > I've always thought of the public invariant of a class as something you > can assume whenever you need it. (Formally, it's part of the theory you > use to do proofs.) So that if o is an instance of B, then o does > satisfy B's public invariant, unless we are inside one of the public > operations of B. Hence this requires clause doesn't add any new > information (and could thus be redundant). But perhaps it's helpful to > make these explicit? I guess adding an axiom that says the invariant > always holds may cause problems in verification of methods of the class > itself, where the invariant won't always hold. Is that the problem? Addition of such an axiom indeed causes trouble. I'm sure Bart doesn't like this :) Ofcourse you want to assume that the invariant of "o" holds. But if you use a specification with such an assumption you also have to prove that your assumption holds. And that causes again a lot of trouble. > > There is a subtle point because using \invariantof in an > > invariant clause might give loops, if there is an (indirect) > > use of \invariantof of A in the invariant of class A. It is not > > clear what this means then. The generated PVS code will give > > a typecheck error. > > That could be avoided using a type system like PVS's, i.e., by doing > static checks. I hope so, but I still have some bad feelings about this. > > The second predicate is sometimes needed because the result of > > a computation can depend on whether static initialization > > still has to take place. Now this cannot be expressed in > > JML. > > Yes, I can see that I think \isinitialized is noncontroversial, and should be > added to JML. Ok, thanks! Best, Joachim  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Wed Dec 13 04:45:49 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id EAA05141 for jml-interest-list-outgoing; Wed, 13 Dec 2000 04:45:26 -0600 (CST) Received: from plato.cs.kun.nl (plato.cs.kun.nl [131.174.33.246]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id EAA05137 for ; Wed, 13 Dec 2000 04:45:23 -0600 (CST) Received: from localhost (erikpoll@localhost) by plato.cs.kun.nl (8.9.3/8.9.3) with ESMTP id LAA06088 for ; Wed, 13 Dec 2000 11:44:58 +0100 X-Authentication-Warning: plato.cs.kun.nl: erikpoll owned process doing -bs Date: Wed, 13 Dec 2000 11:44:58 +0100 (CET) From: Erik Poll To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: private methods that temporarily invalidate invariants Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** X-Authentication-Warning: plato.cs.kun.nl: erikpoll owned process doing -bs Date: Wed, 13 Dec 2000 11:44:58 +0100 (CET) From: Erik Poll To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: private methods that temporarily invalidate invariants Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi all, A bit quiet on the JML mailing list lately, so I thought I'd stir up some controversy... When writing some JML specs I came across classes with private methods that violate some of the invariants. A simple example: public class Example{ private int x,y; //@ invariant: x <= y; //@ ensures: x == n; private void setX(int n) { x = n; } //@ ensures: y == n; private void setY(int n) { y = n; } //@ ensures: \result => 0; public void changeXY(int n) { setX(x+n); setY(y+n); return(y-x); } } Clearly setX and setY do not preserve the invariant. So the JML specification of Example is incorrect. But it is also clear that, since setX and setY are private and only invoked in changeXY, there is not really a problem, and the invariant _will_ be preserved. The invariant will only be invalidated temporarily. The question is how to deal with such situations in JML. The only solution I see that is currently possible in JML is - removing the invariant, and - adding it to the pre and postconditions of the methods that preserve it (ie. changeXY) However, this is not a satisfactory solution, because (a) clients of Example suddenly have the obligation of establishing the precondition x <= y when they want to invoke changeXY, even though we know that this will also be true. (b) a more practical problem is that there may be dozens of invariants and dozens of public methods that preserve them, in which case we end up with hundreds of lines of JML specification. Problem (b) can be alleviated by introducing a boolean model variable // @ public model boolean invariantHolds; with an invariant // @ private invariant: invariantHolds <==> ( x <= y ) and using this model variable as abbreviation in the pre- and post- conditions. (Also, that way x and y don't have to be made spec_public.) Still, this doesn't really solve (a), and code using the class Example will be littered with assertions that invariantHolds for objects of this class. Dealing with the problem in a satisfactory way seems to require an extension of JML, namely a way to specify that some (private) method neither requires nor ensures the invariant. NB JML already offers the possibility of specifying that constraints are only respected by certain methods! (See B.1.4 of the Preliminary Design of JML) We could extend this to invariants, eg. invariant x==y for setXY; (i) Of course, the JML checker should complain if any public (or package) method is not listed here. Or these methods could be implicitly included by deafualt. We could also for list the methods that do _not_ preserve an invariant, eg. invariant x==y except for setX, setY; (ii) I'd strongly prefer (ii) over (i), because (ii) explicitly mentions the "dangerous" methods that require extra care. For larger source files it will be a pain figuring out which methods are _not_ mentioned in all clauses of form (i). Another option would be to say in a method specification that invariants may be violated, eg. //@ ensures y == n; //@ violates_invariants; (iii) private void setY(int n) { y = n; } Option (iii) might be easier to oversee than (ii), because the proof obligations for a method are not spread around in the source code to wherever invariants are written. Of course, the question is how often this problem of private methods violating invariants will occur and whether we should bother with special JML constructs for it. I noticed the problem in a couple of classes so far. Or rather, I didn't notice it at all, but ESC/Java noticed it for me :-) It were always private set-methods causing the problem. Given that typical OO code contains many set- and get-methods, I think the problem may not be rare. I'd be interested to know if anyone else ran into this problem, or if anyone can think of ways to handle it. Cheers, Erik  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Wed Dec 13 14:04:35 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id OAA17555 for jml-interest-list-outgoing; Wed, 13 Dec 2000 14:04:32 -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 OAA17550; Wed, 13 Dec 2000 14:04:27 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id OAA21987; Wed, 13 Dec 2000 14:04:20 -0600 (CST) Date: Wed, 13 Dec 2000 14:04:20 -0600 (CST) Message-Id: <200012132004.OAA21987@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, 13 Dec 2000 11:44:58 +0100 (CET)) Subject: Re: JML-Interest: private methods that temporarily invalidate invariants References: Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Wed, 13 Dec 2000 14:04:20 -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, 13 Dec 2000 11:44:58 +0100 (CET)) Subject: Re: JML-Interest: private methods that temporarily invalidate invariants Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Erik, > Date: Wed, 13 Dec 2000 11:44:58 +0100 (CET) > From: Erik Poll > > When writing some JML specs I came across classes with private > methods that violate some of the invariants. A simple example: > > public class Example{ > > private int x,y; > > //@ invariant: x <= y; > > //@ ensures: x == n; > private void setX(int n) { x = n; } > > //@ ensures: y == n; > private void setY(int n) { y = n; } > > //@ ensures: \result => 0; > public void changeXY(int n) { setX(x+n); setY(y+n); return(y-x); } > } I think that the invariant clause should read: //@ private invariant: x <= y; since private variables shouldn't be visible to default (package) protected assertions. > Clearly setX and setY do not preserve the invariant. So the JML > specification of Example is incorrect. But it is also clear that, > since setX and setY are private and only invoked in changeXY, there > is not really a problem, and the invariant _will_ be preserved. > The invariant will only be invalidated temporarily. > > The question is how to deal with such situations in JML. > > The only solution I see that is currently possible in JML is > - removing the invariant, and > - adding it to the pre and postconditions of the methods that > preserve it (ie. changeXY) My understanding of invariants (of whatever privacy level) is that they only apply to the *public* methods of a class. This follows, for example, Eiffel which also only assumes invariants holds at calls and returns to public methods. So, you would really need to add it to the pre- and postconditions of any non-public methods that need to preserve it. However, in your example, only changeXY is a public method, and so the semantics does what you want. > Of course, the question is how often this problem of private methods > violating invariants will occur and whether we should bother with > special JML constructs for it. > I noticed the problem in a couple of classes so far. Or rather, I didn't > notice it at all, but ESC/Java noticed it for me :-) It were always > private set-methods causing the problem. Given that typical OO code > contains many set- and get-methods, I think the problem may not be rare. > I'd be interested to know if anyone else ran into this problem, or if > anyone can think of ways to handle it. Sounds like ESC/Java has a different semantics for invariants than we intend for JML. Rustan, et al., would you consider changing your semantics to only enforce/assume invariants around public methods? Or is there some good reason not to? My reasoning for doing so is that private methods are "helpers" and should be able to encapsulate any useful state transformation, as the above examples Erik gives demonstrate. > NB JML already offers the possibility of specifying that constraints > are only respected by certain methods! (See B.1.4 of the Preliminary > Design of JML) We could extend this to invariants, eg. > > invariant x==y for setXY; (i) > > Of course, the JML checker should complain if any public (or package) > method is not listed here. Or these methods could be implicitly included > by deafualt. > > We could also for list the methods that do _not_ preserve an invariant, > eg. > invariant x==y except for setX, setY; (ii) > > I'd strongly prefer (ii) over (i), because (ii) explicitly mentions > the "dangerous" methods that require extra care. For larger source > files it will be a pain figuring out which methods are _not_ mentioned > in all clauses of form (i). That is an interesting extension, but I don't see compelling examples for it yet. Do you have any? Barring strong examples, I'm not inclined to add yet more syntax :->... Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Thu Dec 14 03:03:54 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id DAA04209 for jml-interest-list-outgoing; Thu, 14 Dec 2000 03:03:40 -0600 (CST) Received: from plato.cs.kun.nl (plato.cs.kun.nl [131.174.33.246]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id DAA04205 for ; Thu, 14 Dec 2000 03:03:37 -0600 (CST) Received: from localhost (erikpoll@localhost) by plato.cs.kun.nl (8.9.3/8.9.3) with ESMTP id KAA19356 for ; Thu, 14 Dec 2000 10:03:05 +0100 X-Authentication-Warning: plato.cs.kun.nl: erikpoll owned process doing -bs Date: Thu, 14 Dec 2000 10:03:05 +0100 (CET) From: Erik Poll To: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: private methods that temporarily invalidate invariants In-Reply-To: <200012132004.OAA21987@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 *** X-Authentication-Warning: plato.cs.kun.nl: erikpoll owned process doing -bs Date: Thu, 14 Dec 2000 10:03:05 +0100 (CET) From: Erik Poll To: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: private methods that temporarily invalidate invariants In-Reply-To: <200012132004.OAA21987@larch.cs.iastate.edu> Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk On Wed, 13 Dec 2000, Gary T. Leavens wrote: Gary wrote > My understanding of invariants (of whatever privacy level) is that they > only apply to the *public* methods of a class. This follows, for > example, Eiffel which also only assumes invariants holds at calls and > returns to public methods. So, you would really need to add it to the > pre- and postconditions of any non-public methods that need to preserve > it. OK, that solves the whole problem for me. Please forget any suggestions I made for yet more syntax :-) Looks like another entry in esc-jml-diffs.txt. I'd be interested to know the reasons for the ESC/Java semantics of invariants, ie. also requiring & ensuring invariants around non-public methods. I can imagine that in practice this stronger semantics is much nicer to work with (... until you run into a private method that violates an invariant) Erik  1,, X-Coding-System: undecided-unix Mail-from: From Peter.Mueller@FernUni-Hagen.de Thu Dec 14 10:20:22 2000 Return-Path: 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 KAA11395 for ; Thu, 14 Dec 2000 10:20:20 -0600 (CST) Received: from sunpoet2.fernuni-hagen.de by oak.fernuni-hagen.de via local-channel with ESMTP; Thu, 14 Dec 2000 17:20:07 +0100 Received: (from mueller@localhost) by sunpoet2.fernuni-hagen.de (8.9.3+Sun/8.9.1) id RAA01834; Thu, 14 Dec 2000 17:19:18 +0100 (MET) Date: Thu, 14 Dec 2000 17:19:18 +0100 (MET) Message-Id: <200012141619.RAA01834@sunpoet2.fernuni-hagen.de> X-Authentication-Warning: sunpoet2.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" Subject: Re: JML-Interest: private methods that temporarily invalidate invariants In-Reply-To: <200012132004.OAA21987@larch.cs.iastate.edu> References: <200012132004.OAA21987@larch.cs.iastate.edu> X-Mailer: VM 6.32 under Emacs 20.3.1 *** EOOH *** Date: Thu, 14 Dec 2000 17:19:18 +0100 (MET) X-Authentication-Warning: sunpoet2.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" Subject: Re: JML-Interest: private methods that temporarily invalidate invariants In-Reply-To: <200012132004.OAA21987@larch.cs.iastate.edu> Hi, > My understanding of invariants (of whatever privacy level) is that they > only apply to the *public* methods of a class. This follows, for > example, Eiffel which also only assumes invariants holds at calls and > returns to public methods. So, you would really need to add it to the > pre- and postconditions of any non-public methods that need to preserve > it. I agree that invariants must not be preserved by private methods. However, I think that in modular settings, it is necessary that all non-private methods (i.e., not only the public methods) preserve the invariants. Consider the following example: package P1; class Super { protected void m() {...} ... } package P2; class Sub extends P1.Super { public void n() { ... m(); ... } } In the general case, it is not possible to prove that n preserves the invariants if the verifier cannot rely on m preserving the invariants. However, to have this property of m available for the verification of n, (1) the semantics of invariants must force m to preserve the invariants or (2) the verifier of n must prove appropriate properties about the implementation of m. However, in a modular setting, the verifier of n does not have access to the implementation of m (due to information hiding). Therefore, only (1) is an option here. The situation is different for private methods: A private method m can only be invoked from within the class it is declared in. Thus, the caller of m can be assumed to have access to the implementation of m. Thus, he can prove any property of m he is interested in. 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 leavens@cs.iastate.edu Thu Dec 14 23:40:43 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 XAA00157; Thu, 14 Dec 2000 23:40:42 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id XAA05763; Thu, 14 Dec 2000 23:40:30 -0600 (CST) Date: Thu, 14 Dec 2000 23:40:30 -0600 (CST) Message-Id: <200012150540.XAA05763@larch.cs.iastate.edu> From: "Gary T. Leavens" To: Peter.Mueller@FernUni-Hagen.de CC: leavens@cs.iastate.edu In-reply-to: <200012141619.RAA01834@sunpoet2.fernuni-hagen.de> (Peter.Mueller@FernUni-Hagen.de) Subject: Re: JML-Interest: protected methods and invariants References: <200012132004.OAA21987@larch.cs.iastate.edu> <200012141619.RAA01834@sunpoet2.fernuni-hagen.de> *** EOOH *** Date: Thu, 14 Dec 2000 23:40:30 -0600 (CST) From: "Gary T. Leavens" To: Peter.Mueller@FernUni-Hagen.de CC: leavens@cs.iastate.edu In-reply-to: <200012141619.RAA01834@sunpoet2.fernuni-hagen.de> (Peter.Mueller@FernUni-Hagen.de) Subject: Re: JML-Interest: protected methods and invariants Dear Peter, I hate to disagree with you, but... > Date: Thu, 14 Dec 2000 17:19:18 +0100 (MET) > From: "Peter.Mueller" > > > My understanding of invariants (of whatever privacy level) is that they > > only apply to the *public* methods of a class. This follows, for > > example, Eiffel which also only assumes invariants holds at calls and > > returns to public methods. So, you would really need to add it to the > > pre- and postconditions of any non-public methods that need to preserve > > it. > > I agree that invariants must not be preserved by private methods. However, I > think that in modular settings, it is necessary that all non-private methods > (i.e., not only the public methods) preserve the invariants. Consider the > following example: > > package P1; > > class Super { > protected void m() {...} > ... > } > > > package P2; > > class Sub extends P1.Super { > public void n() { > ... > m(); > ... > } > } > > In the general case, it is not possible to prove that n preserves the > invariants if the verifier cannot rely on m preserving the > invariants. I don't see why that would be the case. You just need to know that the pre- and postcondition of m make the necessary state transformation. Why should the invariant hold in the middle of n? Do you have any concrete examples? This one is too abstract to be convincing either way. > However, to have this property of m available for the verification of n, > (1) the semantics of invariants must force m to preserve the invariants or > (2) the verifier of n must prove appropriate properties about the > implementation of m. > However, in a modular setting, the verifier of n does not have access to the > implementation of m (due to information hiding). Therefore, only (1) is an > option here. So in the work that Clyde Ruby and I have been doing, we give a protected specification of protected methods. One could easily include the (protected) invariant as a conjunct in the pre- and postcondition if that is desired. I don't see any advantage in forcing the invarant to hold for all protected methods, because they can't be called directly by clients. Only when a client can observe an object should the state of the object be required to satisfy the invariant, I believe, since otherwise you can't make protected methods that are helpers. The situation is complicated in Java because there can be other clients in the same package that are not subclasses, which can call protected methods. But I think the reasoning for such clients isn't hurt by making it more difficult and the same argument about "helping methods" applies to protected methods intended to be used by code in the same package and not called by outside clients. I think the same remarks apply to default package protected methods, although they can, in Java, be called by clients in the same package. > The situation is different for private methods: A private method m can only be > invoked from within the class it is declared in. Thus, the caller of m can be > assumed to have access to the implementation of m. Thus, he can prove any > property of m he is interested in. Ack, don't we want to prove the properties of private methods from their specifications as well, even if we can see the code? So I don't see the situation being different at all for private vs. protected methods. We always want to reason modularly about methods based on their specifications. Gary  1, filed,, X-Coding-System: undecided-unix Mail-from: From Peter.Mueller@FernUni-Hagen.de Mon Dec 18 08:59:51 2000 Return-Path: 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 IAA11876 for ; Mon, 18 Dec 2000 08:59:49 -0600 (CST) Received: from sunpoet2.fernuni-hagen.de by oak.fernuni-hagen.de via local-channel with ESMTP; Mon, 18 Dec 2000 15:59:45 +0100 Received: (from mueller@localhost) by sunpoet2.fernuni-hagen.de (8.9.3+Sun/8.9.1) id PAA04008; Mon, 18 Dec 2000 15:58:55 +0100 (MET) Date: Mon, 18 Dec 2000 15:58:55 +0100 (MET) Message-Id: <200012181458.PAA04008@sunpoet2.fernuni-hagen.de> X-Authentication-Warning: sunpoet2.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" Subject: Re: JML-Interest: protected methods and invariants In-Reply-To: <200012150540.XAA05763@larch.cs.iastate.edu> References: <200012132004.OAA21987@larch.cs.iastate.edu> <200012141619.RAA01834@sunpoet2.fernuni-hagen.de> <200012150540.XAA05763@larch.cs.iastate.edu> X-Mailer: VM 6.32 under Emacs 20.3.1 *** EOOH *** Date: Mon, 18 Dec 2000 15:58:55 +0100 (MET) X-Authentication-Warning: sunpoet2.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" Subject: Re: JML-Interest: protected methods and invariants In-Reply-To: <200012150540.XAA05763@larch.cs.iastate.edu> Dear Gary, I admit, that my example was not very convincing (not even to me when I read it again), sorry :) The problem described in the example occurs when invariants are not regarded as abstract fields and must therefore not occur in modifiable-clauses when they are broken. However, in our setting, method n can be verified by referring to the modifiable-clause of m. Here is a more pricipled approach to the topic. There are two extreme positions for the semantics of invariants: 1. One can require every method of a program to preserve all invariants. Furthermore, every method can assume that the invariants of all objects hold in its prestate. This meaning of invariants has the advantage that it clearly defines in which execution states the invariants hold. However, it is too restrictive for helper methods. 2. One can allow every method to break invariants. If a method m breaks an invariant, this invariant has to be mentioned in m's modifiable-clause. This way, callers of m can use m's specification to conclude which invariants hold after execution of m. With this semantics, it is less clear in which states which invariants hold. One has to refer to the modifiable-clause of the single methods to conclude in which states which invariants hold. Consequently, one should not assume that all invariants hold in the prestates of methods. Instead, the invariants that are required to hold for the execution of method m have to be listed in the precondition of m. This semantics is for instance used in Rustan's thesis. Both variants have certain advantages: Variant 1 allows one to assume that the invariants of all allocated objects hold in method prestates, which simplifies preconditions at lot. Variant 2 allows one to temporarily break invariants, for instance in helper methods. In practice, one will usually want to have a semantics that lies somewhere in the middle between these extremes: At least for public methods, we want to support the notion of visible states and follow variant 1. To support helper methods, we follow variant 2 for private methods. For me, the right choice for protected and default access methods is not obvious. 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 leavens@cs.iastate.edu Tue Dec 19 02:20:24 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 CAA29401; Tue, 19 Dec 2000 02:20:23 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id CAA12491; Tue, 19 Dec 2000 02:20:21 -0600 (CST) Date: Tue, 19 Dec 2000 02:20:21 -0600 (CST) Message-Id: <200012190820.CAA12491@larch.cs.iastate.edu> From: "Gary T. Leavens" To: Peter.Mueller@FernUni-Hagen.de CC: leavens@cs.iastate.edu In-reply-to: <200012181458.PAA04008@sunpoet2.fernuni-hagen.de> (Peter.Mueller@FernUni-Hagen.de) Subject: Re: JML-Interest: protected methods and invariants References: <200012132004.OAA21987@larch.cs.iastate.edu> <200012141619.RAA01834@sunpoet2.fernuni-hagen.de> <200012150540.XAA05763@larch.cs.iastate.edu> <200012181458.PAA04008@sunpoet2.fernuni-hagen.de> *** EOOH *** Date: Tue, 19 Dec 2000 02:20:21 -0600 (CST) From: "Gary T. Leavens" To: Peter.Mueller@FernUni-Hagen.de CC: leavens@cs.iastate.edu In-reply-to: <200012181458.PAA04008@sunpoet2.fernuni-hagen.de> (Peter.Mueller@FernUni-Hagen.de) Subject: Re: JML-Interest: protected methods and invariants Dear Peter, > Date: Mon, 18 Dec 2000 15:58:55 +0100 (MET) > From: "Peter.Mueller" > > Dear Gary, > > I admit, that my example was not very convincing (not even to me when I read > it again), sorry :) Oh well, at least we agree we need better examples. > Here is a more pricipled approach to the topic. There are two extreme > positions for the semantics of invariants: > > 1. One can require every method of a program to preserve all invariants. > Furthermore, every method can assume that the invariants of all objects > hold in its prestate. This meaning of invariants has the advantage that it > clearly defines in which execution states the invariants hold. However, > it is too restrictive for helper methods. > > 2. One can allow every method to break invariants. If a method m breaks an > invariant, this invariant has to be mentioned in m's > modifiable-clause. This way, callers of m can use m's specification to > conclude which invariants hold after execution of m. With this semantics, > it is less clear in which states which invariants hold. One has to refer to > the modifiable-clause of the single methods to conclude in which states > which invariants hold. Consequently, one should not assume that all > invariants hold in the prestates of methods. Instead, the invariants that > are required to hold for the execution of method m have to be listed in the > precondition of m. This semantics is for instance used in Rustan's thesis. > > Both variants have certain advantages: Variant 1 allows one to assume that the > invariants of all allocated objects hold in method prestates, which simplifies > preconditions at lot. Variant 2 allows one to temporarily break invariants, > for instance in helper methods. > > In practice, one will usually want to have a semantics that lies somewhere in > the middle between these extremes: At least for public methods, we want to > support the notion of visible states and follow variant 1. Yes, we agree on that. > To support helper > methods, we follow variant 2 for private methods. Yes, I also agree on that. > For me, the right choice for > protected and default access methods is not obvious. Yes, I agree it's not so obvious. We'll have to look at more examples. However, I would suggest that one common practice is to make all helper methods protected (instead of private), since one never knows when a subclass will need to override them. In this case the argument for private methods goes through for protected ones too. Have you seen the examples found in the paper that Clyde Ruby and I did for OOPSLA this year? There we assume that invariants don't hold for protected methods, and have several more reasonable examples. It's also available from the JML web page. I have little experience or intuition with default access methods... It would be interesting to find a good example for that case. Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Tue Dec 19 21:08:39 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id VAA17810 for jml-interest-list-outgoing; Tue, 19 Dec 2000 21:08:32 -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 VAA17796; Tue, 19 Dec 2000 21:08:27 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id VAA20199; Tue, 19 Dec 2000 21:08:17 -0600 (CST) Date: Tue, 19 Dec 2000 21:08:17 -0600 (CST) Message-Id: <200012200308.VAA20199@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: want your opinion about minor syntax changes to JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Tue, 19 Dec 2000 21:08:17 -0600 (CST) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: want your opinion about minor syntax changes to JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi all, I am thinking that perhaps we should either get ESC/Java to allow colons in the syntax as optional, or that JML should take out the optional colons it currently has. The way things are, it's difficult for someone to use ESC/Java after using JML. And probably needlessly so. I also wonder if we should change the direction of the arrow in the depends clause. Several students at a recent talk thought it would be less confusing to write: depends abstract_variable <- concrete_variable; instead of the current depends abstract_variable -> concrete_variable; This would also have the direction in the depends clause match that in the represents clause. For example: depends size <- theStack; represents size <- theStack.length(); instead of the current: depends size -> theStack; represents size <- theStack.length(); We'd also have one less token if we change both arrows to go the same way, but that's a minor point. I'm sorry to have been slow in making new releases of JML last semester. I will try to make improvements soon... Gary  1,, X-Coding-System: undecided-unix Mail-from: From owner-jml-interest-list Thu Dec 21 20:33:42 2000 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id UAA02389 for jml-interest-list-outgoing; Thu, 21 Dec 2000 20:33:34 -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 UAA02342; Thu, 21 Dec 2000 20:31:59 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id UAA10651; Thu, 21 Dec 2000 20:31:31 -0600 (CST) Date: Thu, 21 Dec 2000 20:31:31 -0600 (CST) Message-Id: <200012220231.UAA10651@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu 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), scmarney@home.com, htewis@curry.de (Holger_Tewis), Tom@OjodeAgua.COM (Tom_Shields), jhughes@mail.frostburg.edu (John_Hughes), kramer@acm.org (Reto_Kramer), abhay_b@hotmail.com (Abhay_Bhorkar), Arno.Hasse@COODEX.de, asuncionarias@terra.es (Pilar_Arias), mernst@lcs.mit.edu (Michael_Ernst) CC: jml@cs.iastate.edu Subject: JML-Interest: New Release of JML, 2.2 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Date: Thu, 21 Dec 2000 20:31:31 -0600 (CST) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu 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), scmarney@home.com, htewis@curry.de (Holger_Tewis), Tom@OjodeAgua.COM (Tom_Shields), jhughes@mail.frostburg.edu (John_Hughes), kramer@acm.org (Reto_Kramer), abhay_b@hotmail.com (Abhay_Bhorkar), Arno.Hasse@COODEX.de, asuncionarias@terra.es (Pilar_Arias), mernst@lcs.mit.edu (Michael_Ernst) CC: jml@cs.iastate.edu Subject: JML-Interest: New Release of JML, 2.2 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, I've just made another release of JML, 2.2, which is available from the JML ftp site: ftp://ftp.cs.iastate.edu/pub/leavens/JML/ in the file JML.2.2.zip. You can also get it from the JML web page (http://www.cs.iastate.edu/~leavens/JML.html). This release is mostly to gain better compatability with ESC/Java and to make several minor tweaks to the syntax. In particular, we changed the keywords from using public_, protected_, and private_ to have separate modifiers public, protected, and private. We also added some new syntax that the group in Nijmegen wanted for doing verification. I expect to make another release with bug fixes to the run-time, hopefully soon. However, fixing these bugs will take more time, so I thought it would be wise to make this release available now. The changes are summarized below. New with release 2.2 (date: December 21, 2000) major improvements: - More compatability with the current version of ESC/Java. One can now use "modifies" as a synonym for "modifiable". The modifier "non_null" has been added. Also the statement "unreachable" has been added. minor improvements: - Various corrections and clarifications to the preliminary design document (thanks especially to Michael Ernst). - New syntax added to help verification: the primitive expressions \is_initialized() and \invariant_for() (as suggested by the group at the Univ. of Nijmegen). - In a "depends" clause one can now use either a left or right arrow (<- or ->). The samples have been changed to use left arrows, and right arrows will be deprecated in a future release and eventually removed. - The bug where the runtime assertion checker left "==>" in invariant methods has been fixed. - The exception name used in the runtime assertion checker, while still not fresh, is less likely to cause clashes. - The type checker now uses the right type for \lockset. incompatible changes - The syntax has been changed so "public_normal_behavior" is now "public normal_behavior", and in general all uses of public_, protected_, and private_ are eliminated, replacing the "_" with whitespace. (Thanks to Joachim van den Berg for insisting on this.) Please let us know your comments on JML, and if you find bugs. See the BUGS.txt file for the ones we know about. See the preliminary design document for other acknowledgments. 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 Gary