From owner-jml-interest-list Fri Jan 12 06:44:28 2001 MIME-Version: 1.0 To: jml-interest@cs.iastate.edu cc: Bart.Jacobs@cs.kun.nl Subject: JML-Interest: late binding in JML specifications? Content-Type: text/plain; charset=us-ascii Date: Fri, 12 Jan 2001 13:44:01 +0100 From: Bart Jacobs Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, In developing a semantics for JML we came across the issue of late binding in specifications. An example: class A { //@ invariant: i > min(); int i; //@ ensures: \result >= 0; /* pure */ int min() { .. } } class B extends A { //@ ensures: \result >= 10; /* pure */ int min() { .. } } Note that the method min is overridden in B, and has a stronger spec. And since it is pure, it may be used in specifications. All this should be OK. The question now is: if we have an object b belonging to class B, should we have * b.i > 10 This amounts to late binding, because the invariant of A, intepreted in B uses the B-version of min. * b.i > 0 In this case the occurrence of min in the A-invariant is statically bound to the min method in A. What should be use here? Are there clear opinions about this, or references? Your help is appreciated, Bart. PS. The JML Logic paper of Erik and me will appear at FASE 2001 (at ETAPS in Genova in early april). From owner-jml-interest-list Sat Jan 13 12:41:41 2001 Date: Sat, 13 Jan 2001 12:40:49 -0600 (CST) From: "Gary T. Leavens" To: Bart.Jacobs@cs.kun.nl CC: jml-interest@cs.iastate.edu, Bart.Jacobs@cs.kun.nl, leavens@cs.iastate.edu In-reply-to: <200101121244.NAA26431@pandora.cs.kun.nl> (message from Bart Jacobs on Fri, 12 Jan 2001 13:44:01 +0100) Subject: Re: JML-Interest: late binding in JML specifications? Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Bart, > Date: Fri, 12 Jan 2001 13:44:01 +0100 > From: Bart Jacobs > In developing a semantics for JML we came across the issue > of late binding in specifications. An example: > > class A { > > //@ invariant: i > min(); > > int i; > > //@ ensures: \result >= 0; > /* pure */ int min() { .. } > > } > > class B extends A { > > //@ ensures: \result >= 10; > /* pure */ int min() { .. } > > } > > Note that the method min is overridden in B, and has a stronger > spec. And since it is pure, it may be used in specifications. > All this should be OK. > > The question now is: if we have an object b belonging to class B, > should we have > > * b.i > 10 This amounts to late binding, because the invariant of A, > intepreted in B uses the B-version of min. > > * b.i > 0 In this case the occurrence of min in the A-invariant is > statically bound to the min method in A. > > What should be use here? Are there clear opinions about this, > or references? That's a very interesting question. I think that b.i > 10 is what is intended. In my dissertation, and the Acta Informatica paper with Bill Weihl, I used a logic which had something like a notion of late binding like this, and would have used this interpretation. This has the advantage that, if you happen to know that b has dynamic type b, then you know more about it than if you are doing verification assuming that b has type A. From the point of view of clients, who think they have an object of type A, this works out, and fits in with the general idea of behavioral subtyping. (Indeed, it seems to mesh pretty well, since in a subtype, the specification of the method min can be strengthened, which leads to a strengthening of the invariant, which means that clients reasoning about b as if it were an object of type A won't be surprised.) However, I've started thinking about what this means for verification of implementations, especially of subclasses that use inheritance now, and the implications aren't completely clear to me. Clyde Ruby and I didn't think much about this when we were working on our paper that appeared in OOPSLA 2000... Maybe Clyde has some ideas, however. It seems to bear further thought. Congratulations on your paper being accepted. Gary From owner-jml-interest-list Wed Jan 17 12:59:01 2001 Date: Wed, 17 Jan 2001 12:58:35 -0600 (CST) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: "assignable" as synonym for "modifiable" and other JML syntax additions Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, The next release of JML will be mostly bug fixes (getting the run-time checker working better). But I'd also like to get in some minor syntax additions. The purpose of this email is to see if anyone objects to the additions I'm proposing below (in particular, the folks at Compaq SRC). The first, is the addition of the keyword "assignable" as a synonym for "modifiable". This corresponds to the semantics of JML better than "modifiable" does. Because of that, the advantage of "assignable" is that it would convey the meaning more directly to readers. (Note that in the last release we made "modifies" a synonym for "modifiable" also, for backwards compatability with ESC/Java, so one more synonym shouldn't hurt much. :-) Second are forms of expressions that will support idioms that are found in various books on calculational proofs in the Gries/Schneider/Dijkstra school. I'm teaching a course based on Cohen's book "Programming in the 1990s" (Springer-Verlag, 1990) this semester, which uses this style, and I'd like to be able to translate this style fairly directly into JML. The easy addition is an operator for the negation of <==> (i.e., non-equivalence for booleans), for which I propose the symbol <=!=>. It would have the same precedence as <==>. The idea of the syntax is that "!" means "not", more or less, in Java, and putting it in the middle looks something like the crossing out with a vertical line that you see in normal printed mathematics. The others are more complex, and may cause more potential difficulty for parsing. They are all forms of generalized quantifier. To review, currently our syntax for quantifiers is (where [X] is an optional X and X... means O or more X's): spec-quantified-expr ::= ( quantifier ( quantified-vars ) predicate ) | ( quantifier quantified-var-decl [ ; ] predicate ) quantifier ::= \forall | \exists quantified-vars ::= quantified-var-decl [ ; quantified-var-decl ] ... quantified-var-decl ::= type-spec quantified-var-declarator [ , quantified-var-declarator ] ... quantified-var-declarator ::= ident [ dims ] Of the two forms of spec-quantified-expr, only the second is supported currently by ESC/Java, I believe. One addition I'd like to make is to allow one to (optionally) distinguish the range predicate from the rest of the predicate, this is necessary for the first four generalized quantifiers that I'd like to add, which are: \sum - for summation (repeated addition) \product - for (repeated multiplication0 \max - for the maximum \min - for the minimum \num_of - for the cardinality. The reason the range is necessary can be seen by trying \sum, for example. We would like to write some expression to sum up the numbers 1 through 4, but without a way to distinguish the expression from the range we would have: (\sum int i; 0 < i && i < 5) which doesn't make it clear what we're summing (presumably "i"). I suggest we use something like: (\sum int i; 0 < i && i < 5; i) where I'm using semicolons instead of the usual Gries/Schneider/Dijkstra colons because we are already using semicolons in the syntax for one kind of separator, and because C/C++/Java for loops already use semicolons for something similar. So I'm proposing the following syntax: spec-quantified-expr ::= ( quantifier ( quantified-vars ) [ [ range ] ; ] qexp ) | ( quantifier quantified-var-decl [ ; ] [ [ range ] ; ] qexp ) quantifier ::= \forall | \exists | \sum | \product | \max | \min | \num_of quantified-vars ::= quantified-var-decl [ ; quantified-var-decl ] ... quantified-var-decl ::= type-spec quantified-var-declarator [ , quantified-var-declarator ] ... quantified-var-declarator ::= ident [ dims ] range ::= predicate qexp ::= spec-expression (Recall that the only difference between a predicate and a spec-expression is that the former must be of type boolean.) In the case of \forall, \exists, and \num_of, the qexp must be of type boolean. For all the others it must be a numeric type (int, short, long, float, double, I would say, but maybe we should include the types Integer, ..., Double). The type of a \num_of quantified expression is long, and the type of a \sum_of, \product, \max, and \min expression is the type of the qexp in its body. The meaning of an omitted range is "true". The meaning of the optional range for the quantifiers \forall and \exists is given by the following (the usual "trading rule"): (\forall qvd; R; QE) <==> (\forall qvd; R ==> QE) (\exists qvd; R; QE) <==> (\exists qvd; R && QE) Something simlar holds for \num_of: (\num_of qvd; R; QE) <==> (\num_of qvd; R && QE) The meaning of the proposed new quantifiers can be illustrated by example: (\num_of int i; 0 < i && i < 5) == 4 (\num_of int i; 0 < i && i < 5; false) == 0 (\sum int i; 0 < i && i < 5; i) == 1 + 2 + 3 + 4 == 10 (\sum int i; false; i) == 0 (\product int i; 0 < i && i < 5; i) == 1 * 2 * 3 * 4 == 24 (\product int i; false; i) == 1 (\max int i; 0 < i && i < 5; i) == 4 (\min int i; 0 < i && i < 5; i) == 1 The definition of \num_of is (\num_of qvd; R ; QE) == (\sum qvd; R && QE; 1) Cohen gives various laws for defining the meaning of the other quantifiers. I illustrate the laws for \sum below: dummy transformation rule : (\sum T i; R(i); P(i)) == (\sum T j; R(f(j)); P(f(j))) provided f is invertible and j doesn't appear in R(i) or P(i) nesting rule: (\sum T i,j; R1(i) && R2(i,j); Q(i,j)) == (\sum T i; R1(i); (\sum T j; R2(i,j); Q(i,j))) where j doesn't occur free in R1(i) one-point rule: (\sum T i; i == N; Q(i)) == Q(N) provided i doesn't occur free in N and Q(N) is defined The nesting rule is the reason for distinguishing the range and the qexp syntactically. There also some rules that depend on the operator that the quantifier is repeating and its unit. These are defined for the quantifiers (except \num_of) as follows. quantifier repeated op unit -------------------------------- \forall && true \exists || false \sum + 0 \product * 1 \max max -inf \min min +inf Of course, in Java, we don't have -inf and +inf for integer-like types, only for floating point types. The operator specific rules are: empty range rule: (\sum qvd; false; P) == 0 term rule: (\sum qvd; R; P + Q) == (\sum qvd; R; P) + (\sum qvd; R; Q) When the repeated operator is also idempotent (as it is for \forall, \exists, \min, and \max), we also have range rule: (\max T i; P(i) || Q(i); T(i)) == max((\max T i; P(i); T(i)), (\max T i; Q(i); T(i))) provided P(i) <=!=> Q(i) for all i constant term rule: (\max T i; R(i); N) == N provided i does not occur free in N and the range is not empty There is also a distributivity rule, which doesn't seem essential for defining the meaning of the quantifiers. This has been a long discussion of the new quantifiers, which are probably the most controversial part of the proposal. I wouldn't expect that ESC/Java would support them, although syntactically distinguishing the range might have some advantages in static checking (if people used it consistently). Some might like some of the quantifiers but not others. Comments? Also is there any objection to the addition of "assignable" or <=!=> to JML? Gary From owner-jml-interest-list Fri Feb 23 23:32:29 2001 Date: Fri, 23 Feb 2001 23:29:08 -0600 (CST) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: 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), asuncionarias@terra.es (Pilar_Arias), mernst@lcs.mit.edu (Michael_Ernst), sqi6834@ksu.edu (Sheng_Qiang), pbj@dcs.ed.ac.uk (Paul_Jackson), dwyer@cis.ksu.edu (Matt_Dwyer), david.cok@kodak.com (David_Cok), leavens@cs.iastate.edu Subject: JML-Interest: New Release of JML, 2.3 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, I've just made another release of JML, 2.3, which is available from the JML ftp site: ftp://ftp.cs.iastate.edu/pub/leavens/JML/ in the file JML.2.3.zip. You can also get it from the JML web page (http://www.cs.iastate.edu/~leavens/JML.html). This release is again just changes to the syntax (sorry), some to gain better compatability with ESC/Java. The changes are summarized below. New with release 2.3 (date: February 24, 2001) major improvements: - An extended syntax for quantifiers, along with the generalized quantifiers \min, \max, \sum, \product, and \num_of have been added to JML. The extended syntax for quantifiers permits one to explicitly specify a range. - The grammar for specifications occurring as statements (in model programs) has been generalized to permit one to specify statements that terminate "abruptly" by continuing or breaking out of a loop, or by returning. minor improvements: - The keyword "assignable" has been added as another synonym for "modifiable" (and "modifies"). - A new operator for expressions, <=!=> was added to allow one to specify inequality. It has the same precedence as <==>. - Various small improvements to the preliminary design document, thanks to comments by Tim Wahls. - The JML tool's lexer now properly switches between modes for specifications that involve quantifiers. - The perl script in bin/nocolons will take out the deprecated colons in all the files you give it. It also changes uses of "modifiable" to "assignable". - The parser driver now tells about warnings, instead of saying "no problems detected" for a fiel with warnings. deprecated syntax: - Use of colons (:) following the main clause keywords (like ensures), is now deprecated. - The quantifier syntax with parentheses around the variable declarations is now deprecated. - Use of right arrows (->) in depends clauses is now deprecated, in favor of left arrows (<-). 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 From owner-jml-interest-list Mon Mar 5 11:22:29 2001 Date: Mon, 5 Mar 2001 11:21:50 -0600 (CST) From: "Gary T. Leavens" To: david.cok@kodak.com CC: leavens@cs.iastate.edu, jml-interest-list@cs.iastate.edu In-reply-to: <85256A06.004F7813.00@knotes.kodak.com> (david.cok@kodak.com) Subject: JML-Interest: Re: JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk David, > Here is a wish list item: I'd like the ability to flag some annotations as > JML but seen as comments by ESC. Otherwise I have to maintain two versions > of source code - one that ESC will run on and one that includes more JML > stuff. Or is there a way to use refinement for this? As to making ESC work on JML stuff, it would be okay if ESC could parse and ignore the JML things it doesn't understand. But you should ask Rustan Leino's ESC group for that :-). As a workaround, you can put the JML annotations in refinement files that refine the ESC specs or code files, as follows. foo.java // java code with ESC annotations | foo.refines-java // file with JML annotations The file foo.refines-java would include the declaration: //@ refines foo <- "foo.java"; Then you could use ESC/Java on foo.java, and JML could work on foo.refines-java, which would automatically read the foo.java file as part of the process of checking foo.refines-java. Let me know if that doesn't work. Gary From owner-jml-interest-list Mon Mar 5 14:13:11 2001 Date: Mon, 5 Mar 2001 14:12:30 -0600 (CST) From: "Gary T. Leavens" To: david.cok@kodak.com CC: leavens@cs.iastate.edu, jml-interest-list@cs.iastate.edu In-reply-to: <85256A06.0068A0CE.00@knotes.kodak.com> (david.cok@kodak.com) Subject: JML-Interest: Re: JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk David, you worte: > >>> The file foo.refines-java would include the declaration: > > //@ refines foo <- "foo.java"; > > This worked, when (a) I used refine instead of refines and (b) put the > statement at the beginning of the file. Oops, yes, of course it's "refine" not refines, I keep making that mistake. > But it still requires that I keep > the declarations in the two files in sync. Yes, it would be better to have ESC parse and ignore the JML constructs it doesn't understand. > My immediate work around for > what I really need is to hack the JML lexer to treat //JML@ and /*JML@ like > //@ and /*@ in JML (but they will be comments in esc). Not sure what to do > long term... It's not pretty, but we could support that if others would like it. Gary From owner-jml-interest-list Tue Mar 6 09:46:31 2001 Date: Tue, 6 Mar 2001 09:44:45 -0600 (CST) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: 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), asuncionarias@terra.es (Pilar_Arias), mernst@lcs.mit.edu (Michael_Ernst), sqi6834@ksu.edu (Sheng_Qiang), pbj@dcs.ed.ac.uk (Paul_Jackson), dwyer@cis.ksu.edu (Matt_Dwyer), david.cok@kodak.com (David_Cok), wahls@trex.hbg.psu.edu (Tim_Wahls), hxl190@psu.edu (Hung-Yu_Lin), leavens@cs.iastate.edu Subject: JML-Interest: New Release of JML, 2.4 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, I've just made another release of JML, 2.4, which is available from the JML ftp site: ftp://ftp.cs.iastate.edu/pub/leavens/JML/ in the file JML.2.4.zip. You can also get it from the JML web page (http://www.cs.iastate.edu/~leavens/JML.html). This release is a bug fix realease. The changes are summarized below. New with release 2.4 (date: March 6, 2001) minor improvements: - The JML checker now correctly parses and type checks \TYPE, \typeof, \type, and <:. Thanks to David Cok for pointing out the bugs and helping with fixes. - The syntax for model programs now allows jml-statements to be nested within other statements (such as while loops). - Arrays of \TYPE can be declared. - The preliminary design document now correctly documents non_null and \TYPE. - Test cases have been added for \TYPE, \typeof, \type, <:, and extended forms of specification statement in model programs. 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 From owner-jml-interest-list Fri Mar 23 18:01:10 2001 Date: Fri, 23 Mar 2001 18:00:26 -0600 (CST) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu, david.cok@kodak.com Subject: JML-Interest: Paper on Weak Behavioral Subtyping available Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi all, Krishna Kishore Dhara and I have been working on the following paper which we recently submitted to a conference (guess which one!). It's available from the following URLs ftp://ftp.cs.iastate.edu/pub/techreports/TR01-02/TR.ps.gz ftp://ftp.cs.iastate.edu/pub/techreports/TR01-02/TR.pdf Comments would be appreciated. (I hope to return to working on JML shortly. David Cok has been finding bugs and even giving me some fixes, and I have been making progress in finding other bugs and making other fixes also. So we'll have a bug fix release shortly...) Gary -------------------------------------------------------------------- Mutation, Aliasing, Viewpoints, Modular Reasoning, and Weak Behavioral Subtyping by Krishna Kishore Dhara and Gary T. Leavens Abstract Existing work on behavioral subtyping either ignores aliasing or restricts the behavior of additional methods in a subtype and only allows one to use invariants and history constraints in reasoning. This prevents many useful subtype relationships; for example, a type with immutable objects (e.g., immutable sequences), cannot have a behavioral subtype with mutable objects (e.g., mutable arrays). Furthermore, the associated reasoning principle is not very useful, since one cannot use the pre- and postconditions of methods. Weak behavioral subtyping permits more behavioral subtype relationships, does not restrict the behavior of additional methods in subtypes, and allows the use of pre- and postconditions in reasoning. The only cost is the need to restrict aliases so that objects cannot be manipulated through the view of more than one type. Keywords: Weak behavioral subtyping, strong behavioral subtyping, viewpoint, aliasing, mutation, modularity, specification, verification, Java language, JML language. From owner-jml-interest-list Fri Apr 6 11:51:08 2001 Date: Fri, 6 Apr 2001 11:50:32 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: Some possible changes to JML, comments Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, I have had somewhat extensive discussions with Robert Findler, Matthias Felleisen, and their group at Rice (soon to be Northeastern), and also with Michael Ernst at MIT. Both groups are considering using JML's syntax and more or less joing the JML effort. Both are in the business of building various tools. They each asked for some extensions and changes to JML's syntax. The one change both want, which I think we should adopt if there are no objections, is to allow method specifications to come after the method header if there is a method body. This would also be compatible with ESC/Java. Findler, Felleisen, and their group would like to see us allow "pre" as a synonym for "requires" and "post" for "ensures". I have argued that it complicates the syntax some, but it doesn't cause much difficulty to allow it if others would like that. Rustan, et al, would it be a problem for ESC/Java to support such synonyms? It would just be a matter of changing the parser (perhaps even just the lexer). Michael Ernst wants to allow \old() to be able to appear inside \old(), since he's mechanically generating such annnotations. The meaning would just ignore the inner occurrences of \old. I don't see any semantic problem with that, and propose that we accept it. Anyone object? Michael also suggests a kind of implicit quantification syntax, at least for arrays. He would like: E0(\every(E1)) where E0 is a spec-expression and E1 is a spec-expression that denotes an object of an array type (e.g., char[]) to mean (\forall int i; 0 <= i && i < (E1).length; E0(E1[i])) where i is a fresh variable (not free in E0 or E1). Similarly E0(\each(E1)) should mean (\exists int i; 0 <= i && i < (E1).length; E0(E1[i])) (where again i is fresh, and E1 has an array type). For example, \every(chars) < 'z' means (\forall int i; 0 <= i && i < chars.length; chars[i] < 'z') Michael would like these for machine generation of invariants, but also argues that the notations increase readability. Some alternatives are to use different keywords: \every_element() (or \each_element or \any_element) and \some_element(), or even \every() and \some(). Another possibility, which I think I may like better, is to use this kind of pointwise when the array index has a form like E1..E2 or *, which we already permit in store-refs (e.g., in assignable clauses). For example, chars[*] < 'z' and chars[0..10] < 'z'. The disadvantage of this is that it doesn't support the existential form, but perhaps that's less important? Gary From owner-jml-interest-list Sun Apr 15 20:19:44 2001 Date: Sun, 15 Apr 2001 20:18:32 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: 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), asuncionarias@terra.es (Pilar_Arias), mernst@lcs.mit.edu (Michael_Ernst), sqi6834@ksu.edu (Sheng_Qiang), pbj@dcs.ed.ac.uk (Paul_Jackson), dwyer@cis.ksu.edu (Matt_Dwyer), david.cok@kodak.com (David_Cok), wahls@trex.hbg.psu.edu (Tim_Wahls), hxl190@psu.edu (Hung-Yu_Lin), A.A.Hamie@bton.ac.uk (Ali_Hamie), leavens@cs.iastate.edu Subject: JML-Interest: New Release of JML, 2.5 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, I've just made another release of JML, 2.5, which is available from the JML ftp site: ftp://ftp.cs.iastate.edu/pub/leavens/JML/ in the file JML.2.5.zip. You can also get it from the JML web page (http://www.cs.iastate.edu/~leavens/JML.html). This release is a bug fix release, but a *lot* of bugs have been fixed. Thanks very much to David R. Cok for many bug reports, test cases, and several pieces of code with various fixes. Thanks to Clyde Ruby for help with the revised jml.y file. The changes are summarized below. New with release 2.5 (date: April 15, 2001) major improvements - Thanks to David Cok, several fixes to the treatment of nested and inner classes (InnerType*.java). Nested classes with private members are now handled better, and the scope of nested classes is handled better. The "Access denied as member is private" error no longer occurs (WindowManager.java). - The \reach syntax has been extended to allow limiting the types of the reachable objects and the fields through which objects can be reached. - Fixed the grammar so that it properly parses local nested classes (as statements), array declarators before .class, gives instanceof the proper precedence, has the right grammar for cast expressions, and checks properly for octal character escapes. Thanks to Clyde Ruby for corresponding fixes to the jml.y grammar file. - Unknown paragraph tags in documentation comments are now ignored, and no longer cause errors. - JML now parses and ignores ESC/Java's nowarn pragmas (Thanks to David R. Cok for help with this). - Method specification can now also appear between the method header and the method body (which is considered to be the semicolon for an abstract method). This allows better compatability with ESC/Java, and was requested by other groups. - The modifier non_null now works as a modifier on local variable declarations. - The scope of a declaration in the initializer of a for loop now properly includes the loop invariant and variant function. - One can now declare free variables whose scope is a whole specification case (i.e., that are universally quantified over a whole specification case), using the syntax "forall T x;" as documented in the grammar under spec_var_decls. incompatible changes: - The "because" and "because_redundantly" keywords (used in making annotation proofs) have been replaced by "hence_by" and "hence_by_redundantly". These indicate the correct direction of implication. Thanks to Jeff Mohar and students in 22C:181 at the University of Iowa for this suggestion. - Development now requires Anltr 2.7.1 or higher. There is a long list of minor improvements also, but see the NEWS.txt file in the release for their details. 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 Subject: JML-Interest: New Release of JML, 2.6 Date: Mon, 21 May 2001 01:24:13 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Hi, I've just made another release of JML, 2.6, which is available from the JML ftp site: ftp://ftp.cs.iastate.edu/pub/leavens/JML/ in the file JML.2.6.zip. You can also get it from the JML web page (http://www.cs.iastate.edu/~leavens/JML.html). This release is a bug fix release. Nothing extermely significant, but the preliminary design document should be much easier to use. More thanks to David R. Cok are due for more help finding bugs. Thanks also to Clyde Ruby for help with the revised jml.y and jml.l files. The changes are summarized below. New with release 2.6 (date: 21 May, 2001) major improvements - The preliminary design document now has useful indexes. - The syntax in the preliminary design document's appendix B now has hyperlinks, so that one can click on the use of a nonterminal, and jump to its definition. - The checker now makes sure that only model variables can be used on the left hand sides of depends and represents clauses. It now checks the types of represents clauses that use the <- form. (concrete_represents.java) - JML now ignores multiple asterisks (*) at the beginning and end of documentation comments, and at the beginning of each line of a documentation comment. This gives better conformance to Java's standard for documentation comments. - Similarly, JML now ignores multiple at-signs (@) at the beginning and end of annotations, and at the beginning of each line of an annotation. This gives better compatability with ESC/Java version 1.2.4. minor improvements - The file esc-jml-diffs.txt has been updated to reflect the current differences between ESC/Java and JML. - The LALR(1) grammar for JML, and its lexical counterpart, (jml.y and jml.l in edu/iastate/cs/jml/checker/) have been corrected, thanks to Clyde Ruby. Also included in the release is source for a C++ program that tests the LALR(1) grammar. - The JML parser handles documentation comments that are out of place slightly better than before. - The treatment of at-signs after paragraph tags in HTML output has been improved. - Overrides of methods from nested classes no longer give null pointer exceptions (see OverrideNestedClassMethod.java). - Unresolved "PlaceHolder"s no longer occur when the first reference to a type is an array element (UnresolvedPlaceholder.java). - The checker no longer complains about methods inherited from interfaces that are not implemented in non-.java files (which is okay if one is writing a file to be refinement). - Unparsing with --unparse no longer throws away a type's documentation comments. - The search for files that are JML files in a directory, and the jmlstartfiles utility, now correctly deal with files with class names that are prefixes of other class names in the same directory. - The various filename suffixes are now documented in the preliminary design document. - Slightly better documentation for the model classes, including an entry in the index for JMLModelObjectSet and JMLModelValueSet. - Added new model interface edu.iastate.cs.jml.models.JMLComparable. - Added compareTo methods to many of the model types. - The DOS batch files in bin now restore the CLASSPATH, so that they don't use up all the environment space. incompatible changes: - Misspelled methods in the implementation of edu.iastate.cs.jml.models.JMLValueBag and JMLObjectBag have been deprecated in favor of the correctly spelled methods. - The interface edu.iastate.cs.jml.models.JMLOrderedType has been deprecated in favor of JMLComparable. JMLOrderedType doesn't follow the naming conventions of the other model classes for its methods. 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 From - Mon Jun 25 18:01:53 2001 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id RAA20005 for jml-interest-list-outgoing; Mon, 25 Jun 2001 17:55:40 -0500 (CDT) Received: from cs.iastate.edu (leavens.cs.iastate.edu [129.186.3.47]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id RAA19975; Mon, 25 Jun 2001 17:55:28 -0500 (CDT) Message-ID: <3B37C0EC.6B01BB21@cs.iastate.edu> Date: Mon, 25 Jun 2001 17:53:32 -0500 From: "Gary T. Leavens" Organization: Department of Computer Science, Iowa State University X-Mailer: Mozilla 4.77 [en] (Win98; U) X-Accept-Language: en MIME-Version: 1.0 To: Erik Poll CC: jml-interest-list@cs.iastate.edu, Nestor Catano , Marieke Huisman Subject: Re: JML-Interest: \fields_of(a) if a is an array References: Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Erik, et al., Erik Poll wrote: > Hi all, > > A small question about the semantics of \fields_of. Maybe other > people realised this before, but it's new to me. > > Consider the example > > //@ assignable \fields_of(\reach(this)) > public void m() { this.a[1] = 5} > > Strictly speaking this.a[1] is not a "field" of an object reachable > from this. Still, I would say that the method above repects its > modifies clause. You agree ? Yes, I agree. I think we can consider the elements of an array to be fields of an array object (with strange names), as you suggest... > If so, this suggests that the meaning of \fields_of should subsume > that of [*], as follows > > \fields_of(a) is - a[*], if a is an array > - the set of fields of a, otherwise > > ie. array entries are regarded as the fields of array-objects. > This should then be mentioned in Section 3.2 of the JML design paper. Yes, that all sounds right to me. > I noticed this issue looking at the work of Nestor Catano, a student > doing his Master thesis with Marieke Huisman at Sophia-Antipolis. He's > is looking at the semantics of modifiable clauses, and trying to come > up with some rules for deriving that a statement satisfies some > modifies-clause (insofar as that is possible with purely syntactic > derivation rules, of course.) Yes, Marieke mentiond this work to me. I'm interested, of course in it. In this area I'm also interested in getting reaction to the proposal set forth in the paper: Peter Müller, Arnd Poetzsch-Heffter, and Gary T. Leavens. Modular Specification of Frame Properties in JML. In Formal Techniques for Java Programs 2001, workshop at ECOOP 2001. Also Department of Computer Science, Iowa State University, TR #01-03, April 2001. ftp://ftp.cs.iastate.edu/pub/techreports/TR01-03/TR.ps.gz ftp://ftp.cs.iastate.edu/pub/techreports/TR01-03/TR.pdf -- Gary T. 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 http://www.cs.iastate.edu/~leavens From - Tue Jun 26 18:55:19 2001 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id SAA16030 for jml-interest-list-outgoing; Tue, 26 Jun 2001 18:53:52 -0500 (CDT) Received: from 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 SAA15996; Tue, 26 Jun 2001 18:53:47 -0500 (CDT) Message-ID: <3B392082.CAF491F@cs.iastate.edu> Date: Tue, 26 Jun 2001 18:53:39 -0500 From: "Gary T. Leavens" Organization: Department of Computer Science, Iowa State University X-Mailer: Mozilla 4.77 [en] (X11; U; HP-UX B.10.20 9000/735) X-Accept-Language: de,fr MIME-Version: 1.0 To: JML Interest List Subject: JML-Interest: Public specifications of private methods? Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi all, Yoonsik Cheon brings up an interesting question. Is there some reasonable example of when you'd like to have a specification with visibility that is more public than the method it specifies? For example, an example of a public specification of a private method? I can think of reasons for the converse, but not for this. So we are proposing to rule it out. Any objections? -- Gary T. 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 http://www.cs.iastate.edu/~leavens From - Thu Jul 12 17:34:33 2001 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id RAA22422 for jml-interest-list-outgoing; Thu, 12 Jul 2001 17:32:27 -0500 (CDT) Received: from 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 RAA22392; Thu, 12 Jul 2001 17:32:20 -0500 (CDT) Message-ID: <3B4E256C.F3E79BDF@cs.iastate.edu> Date: Thu, 12 Jul 2001 17:32:12 -0500 From: "Gary T. Leavens" Organization: Department of Computer Science, Iowa State University X-Mailer: Mozilla 4.77 [en] (X11; U; HP-UX B.10.20 9000/735) X-Accept-Language: de,fr MIME-Version: 1.0 To: JML Interest List Subject: JML-Interest: preconditions for constructors in JML, semantics of "let" Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, Here are a couple of questions regarding the semantics of JML I'd like to get your opinion on. These came up in discussions with Yoonsik Cheon about run-time checking of assertions. 1. The precondition of a constructor is different than most method preconditions in that one can't necessarily guarantee that the fields of the object being constructed are already initialized. Of course, that's the main purpose of most constructors -- to initialize the instance fields. So should a constructor's precondition be allowed to refer to instance fields of the this object? We think it's simpliest to just say "no" here. While there are some cases in which this is well-defined (when there is an initializer of some sort), it seems simpler to just prohibit preconditions in constructors from refering to instance fields of "this". (The same seems to apply to the specification of instance initializers, and similar considerations apply to static initializers.) Any objections to restricting preconditions of constructors (and intializers) in this way? 2. The semantics of the "let" clauses in JML method specifications isn't really set forward in the preliminary design document. However, the Larch/C++ manual describes the semantics of "let" as a syntactic sugar, so that the definition of the variables is substituted for each occurrence in the body of the spec-case that the let is in. One would have to take care to avoid variable capture (from quantifiers, for example). We think this is the appropriate semantics for "let" in JML also. This semantics has a consequence that the meaning of a let-bound variable can change between the pre-state and the post-state of a method. For example, one couldn't explain "\old" using "let". But you can use "\old" in a let definition with this semantics, which is perhaps clearer. Comments? -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1040 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From - Fri Jul 13 10:58:35 2001 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id IAA07197 for jml-interest-list-outgoing; Fri, 13 Jul 2001 08:33:14 -0500 (CDT) Received: from mailgate3.cinetic.de (mailgate3.cinetic.de [212.227.116.80]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id IAA07193 for ; Fri, 13 Jul 2001 08:33:11 -0500 (CDT) Received: from smtp.web.de (smtp01.web.de [194.45.170.210]) by mailgate3.cinetic.de (8.11.2/8.11.2/SuSE Linux 8.11.0-0.4) with SMTP id f6DDX9g28713 for ; Fri, 13 Jul 2001 15:33:09 +0200 Received: from web.de by smtp.web.de with smtp (freemail 4.2.2.2 #11) id m15L349-007oE6C; Fri, 13 Jul 2001 15:33 +0200 Message-ID: <3B4EF89C.7B108F31@web.de> Date: Fri, 13 Jul 2001 15:33:16 +0200 From: Roland Zumkeller X-Mailer: Mozilla 4.77 [en] (X11; U; Linux 2.4.3-20mdk i686) X-Accept-Language: en MIME-Version: 1.0 To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: Re: preconditions for constructors in JML References: <3B4E256C.F3E79BDF@cs.iastate.edu> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk > So should a constructor's precondition be allowed to refer to > instance fields of the this object? I agree that not all fields of "this" should be accessible from the precondition. But what about constructor chaining, i.e. when a constructor invokes another one with "super(...)" (or even "this(...)")? If access is restricted to the fields of "super" then the meaning of the precondition is well-defined. The following example shows an utilization: class Employee { String title, firstName, lastName; Employee(String name) { ...parse the full name and split it into title, firstName and lastName... } } class Professor extends Employee { // only people with a PhD can become professors: /*@ public normal_behavior @ requires super.title.equals("PhD"); @*/ Professor(String name) { super(name); } } But it makes only sense to mention "super" after the execution of the first constructor. So the question is: Is the precondition evalueated before or after the execution of the super-call? If it's evaluated before, one takes the user's point of view because if the precondition is met, things go well. The example doesn't work then, though. Evaluating it afterwards let's one express more, since it makes sense to speak of "super" (as the example shows). Furthermore the constructor's pre-condition is evaluated before the constructor itself and not before the whole chain, so it seems to be textually in the right place. I don't know which option is to be given preference. A third approach would be to include a third "intercondition" which is evaluated between the two call or a keyword similar to \old. - Roland From - Fri Jul 13 11:04:51 2001 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id KAA09968 for jml-interest-list-outgoing; Fri, 13 Jul 2001 10:54:47 -0500 (CDT) Received: from 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 KAA09934; Fri, 13 Jul 2001 10:54:39 -0500 (CDT) Message-ID: <3B4F19BA.4E53B75A@cs.iastate.edu> Date: Fri, 13 Jul 2001 10:54:35 -0500 From: "Gary T. Leavens" Organization: Department of Computer Science, Iowa State University X-Mailer: Mozilla 4.77 [en] (X11; U; HP-UX B.10.20 9000/735) X-Accept-Language: de,fr MIME-Version: 1.0 To: Roland Zumkeller CC: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: Re: preconditions for constructors in JML References: <3B4E256C.F3E79BDF@cs.iastate.edu> <3B4EF89C.7B108F31@web.de> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Roland, et al., Roland Zumkeller wrote: > > So should a constructor's precondition be allowed to refer to > > instance fields of the this object? > > I agree that not all fields of "this" should be accessible from the > precondition. But what about constructor chaining, i.e. when a > constructor invokes another one with "super(...)" (or even "this(...)")? > If access is restricted to the fields of "super" then the meaning of the > precondition is well-defined. The following example shows an > utilization: > > class Employee { > String title, firstName, lastName; > > Employee(String name) { > ...parse the full name and split it into title, firstName and > lastName... > } > } > > class Professor extends Employee { > // only people with a PhD can become professors: > /*@ public normal_behavior > @ requires super.title.equals("PhD"); > @*/ > Professor(String name) { > super(name); > } > } Technically, super.title should be illegal in a public precondition, since it has default (package) access. However, I see that the JML checker doesn't catch this error. (I'm making a bug report out of it, sigh). But let's assume it was declared as spec_public. (Also it could just be written as title, I guess, again, no matter.) > But it makes only sense to mention "super" after the execution of the > first constructor. So the question is: Is the precondition evalueated > before or after the execution of the super-call? The precondition is supposed to hold at after parameter passing, but before any code is executed. So it's before, technically. > If it's evaluated before, one takes the user's point of view because if > the precondition is met, things go well. The example doesn't work then, > though. Yes, the idea is to take the user's point of view, and the example doesn't work as intended. > Evaluating it afterwards let's one express more, since it makes sense to > speak of "super" (as the example shows). Furthermore the constructor's > pre-condition is evaluated before the constructor itself and not before > the whole chain, so it seems to be textually in the right place. > > I don't know which option is to be given preference. A third approach > would be to include a third "intercondition" which is evaluated between > the two call or a keyword similar to \old. That's an interesting idea. But let's see if it's really necessary. First, note that trying to just use an assert statement doesn't work well: class Professor extends Employee { // only people with a PhD can become professors: Professor(String name) { super(name); //@ assert title.equals("Ph.D."); } } The problem is that the assert statement just looks like an internal constraint. We can do better if we have a model method to find the title from the name. This also lets us specify the superclass constructor: class Employee { protected /*@ spec_public @*/ String title, firstName, lastName; /*@ public normal_behavior @ requires name != null; @ ensures (* \result is the title found in name, if any, and "" otherwise *); @ public model String findTitle(String name); @ @ public normal_behavior @ requires name != null; @ ensures (* \result is the first name of name, @ if properly formatted, and "" otherwise *); @ public model String findFirstName(String name); @ @ public normal_behavior @ requires name != null; @ ensures (* \result is the last name of name, @ if properly formatted, and "" otherwise *); @ public model String findLastName(String name); @*/ /*@ public normal_behavior @ requires name != null; @ assignable title, firstName, lastName; @ ensures title.equals(findTitle(name) @ && firstName.equals(findFirstName(name)) @ && lastName.equals(findLastName(name)); Employee(String name) { // ...parse the full name and split it into parts... } } class Professor extends Employee { // only people with a PhD can become professors: /*@ public normal_behavior @ requires name != null @ && findTitle(name).equals("Ph.D."); @*/ Professor(String name) { super(name); } } This seems to express what is intended, without use of any of the fields in the precondition of th constructor. My conclusion is thus that there's no need (at least in this example) to deviate from the simplest rule, which is just to not let preconditions refer to instance variables. My guess is that other examples could be treated similarly. But it would be interesting to examine more examples in real programs. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1040 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From - Mon Jul 16 11:33:47 2001 Return-Path: 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 HAA27711; Mon, 16 Jul 2001 07:15:05 -0500 (CDT) Received: from localhost (erikpoll@localhost) by plato.cs.kun.nl (8.9.3/8.9.3) with ESMTP id OAA27244; Mon, 16 Jul 2001 14:11:45 +0200 X-Authentication-Warning: plato.cs.kun.nl: erikpoll owned process doing -bs Date: Mon, 16 Jul 2001 14:11:45 +0200 (CEST) From: Erik Poll To: "Gary T. Leavens" cc: JML Interest List Subject: Re: JML-Interest: semantics of "let" In-Reply-To: <3B4E256C.F3E79BDF@cs.iastate.edu> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Hi all, > 1. The precondition of a constructor is different than most method > preconditions in that one can't necessarily guarantee that the fields of > the object being constructed are already initialized. I agree with Gary that not allowing the constructor's precondition to refer to the instance fields of "this" seems to be the sensible thing to do. > 2. The semantics of the "let" clauses in JML method specifications isn't > really set forward in the preliminary design document. However, the > Larch/C++ manual describes the semantics of "let" as a syntactic sugar, > so that the definition of the variables is substituted for each > occurrence in the body of the spec-case that the let is in. One would > have to take care to avoid variable capture (from quantifiers, for > example). We think this is the appropriate semantics for "let" in > JML also. > This semantics has a consequence that the meaning of a let-bound > variable can change between the pre-state and the post-state of a > method. For example, one couldn't explain "\old" using "let". But you > can use "\old" in a let definition with this semantics, which is perhaps > clearer. So it seems that there are two possible semantics for the let expressions: (i) syntactic sugar, ie essentially a macros (ii) binding a value to a variable I have never used the let clause so far, so I have no clue which of these two would one would be more useful in programs. And anyway, for many examples choosing (i) or (ii) as the semantics for let will not make a difference. This is the case with the example in the JML design paper (Sect 2.3.2) and seems to be the case with all the uses of "let" in edu/iastate/cs/jml/* My only objection to Gary's proposal to treat "let" as syntactic sugar is that a let-clause _looks_ like an ordinary Java assignment. This would lead me to expect that its semantics is (ii) rather than (i). I would be very surprised that after //@ let model int x = y + z; the value of x changes whenever y or z changes! The most important global design decision for JML has been that it should look like & behave as normal Java as much as possible. Choosing "let" to be syntactic sugar goes against this principle, and I think it could seriously confuse the unsuspecting user of JML. A possible way to alleviate this would be to choose a different syntax for let assignments. Eg if the syntax was #define x (y+z) I would not be surpised that x is just an abbreviation. I'm not seriously proposing to include #define as JML syntax, but I hope you see my point. Erik From - Mon Jul 16 11:34:07 2001 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id LAA02478 for jml-interest-list-outgoing; Mon, 16 Jul 2001 11:11:10 -0500 (CDT) Received: from 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 LAA02448; Mon, 16 Jul 2001 11:11:01 -0500 (CDT) Message-ID: <3B531210.9F5436D5@cs.iastate.edu> Date: Mon, 16 Jul 2001 11:10:56 -0500 From: "Gary T. Leavens" Organization: Department of Computer Science, Iowa State University X-Mailer: Mozilla 4.77 [en] (X11; U; HP-UX B.10.20 9000/735) X-Accept-Language: de,fr MIME-Version: 1.0 To: Erik Poll CC: JML Interest List Subject: Re: JML-Interest: semantics of "let" References: Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Erik, et al., It seems that the semantics of "let" clauses is still pretty much up in the air... Erik Poll wrote: > > 2. The semantics of the "let" clauses in JML method specifications isn't > > really set forward in the preliminary design document. However, the > > Larch/C++ manual describes the semantics of "let" as a syntactic sugar, > > so that the definition of the variables is substituted for each > > occurrence in the body of the spec-case that the let is in. One would > > have to take care to avoid variable capture (from quantifiers, for > > example). We think this is the appropriate semantics for "let" in > > JML also. > > This semantics has a consequence that the meaning of a let-bound > > variable can change between the pre-state and the post-state of a > > method. For example, one couldn't explain "\old" using "let". But you > > can use "\old" in a let definition with this semantics, which is perhaps > > clearer. > > So it seems that there are two possible semantics for the let expressions: > > (i) syntactic sugar, ie essentially a macros > (ii) binding a value to a variable > > I have never used the let clause so far, so I have no clue which of > these two would one would be more useful in programs. > > And anyway, for many examples choosing (i) or (ii) as the semantics for > let will not make a difference. This is the case with the example in > the JML design paper (Sect 2.3.2) and seems to be the case with all the > uses of "let" in edu/iastate/cs/jml/* > > My only objection to Gary's proposal to treat "let" as syntactic sugar > is that a let-clause _looks_ like an ordinary Java assignment. This would > lead me to expect that its semantics is (ii) rather than (i). > I would be very surprised that after > > //@ let model int x = y + z; > > the value of x changes whenever y or z changes! > The most important global design decision for JML has been that it should > look like & behave as normal Java as much as possible. Choosing "let" to be > syntactic sugar goes against this principle, and I think it could seriously > confuse the unsuspecting user of JML. > > A possible way to alleviate this would be to choose a different syntax > for let assignments. Eg if the syntax was > > #define x (y+z) > > I would not be surpised that x is just an abbreviation. I'm not seriously > proposing to include #define as JML syntax, but I hope you see my point. I tend to agree with Erik's point on this. Also in support of this are Joseph Kiniry, who wrote: > Of course, most uses of such let clauses do not have this semantics, > (e.g. ML, Lisp, CCS derivatives), if I'm interpreting you properly. If you > adopt the non-syntactic sugar semantics, you promote the let variable to a > real ghost variable, thus its operational semantics are no longer syntactic > replacement but pre-state assignment. > > Personally, I am more used to, and comfortable with, such a semantics. > And Michael Ernst wrote: > > the > > Larch/C++ manual describes the semantics of "let" as a syntactic sugar, > > ... We think this is the appropriate semantics for "let" in > > JML also. > > I am ambivalent about this. it violates my intuitions about "let" from > programming languages, but given no side effects, it seems fine. > > I tend to agree with these arguments. So we probably should not use the semantics of "let" as a syntactic sugar that I proposed. This leaves several alternative designs for "let". 1. Keep the current syntax, but evaluate the variable's defining expression in the pre-state, bind it to a location there, and use the value of that location when it is referenced. (This location couldn't be changed by a method program, so it would have the same value in both the pre-state and the post-state.) The disadvantage of this is that there's no easy way to abbreviate expressions that are to be evaluated in the post-state of a method. 2. Drop the current syntax completely, but add let-expressions, which are evaluated in whatever state they occur in (e.g., the pre-state if they occur in the requires or assignable clauses), the post-state if they occur in ensures or signals clauses. The disadvantage of this is that there's no easy way to abbreviate expressions that are used in both the pre- and postcondition of a method. However, one can use model methods to do this, although that's not very good for ESC/Java and other tools that don't want to use model methods. My preference is for alternative 1, since it seems more expressive, and alternative 2 doesn't have compelling disadvantages to me. Comments? -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1040 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From - Mon Jul 16 11:38:39 2001 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id LAA03382 for jml-interest-list-outgoing; Mon, 16 Jul 2001 11:37:43 -0500 (CDT) Received: from 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 LAA03350; Mon, 16 Jul 2001 11:37:37 -0500 (CDT) Message-ID: <3B53184B.1EF69AE3@cs.iastate.edu> Date: Mon, 16 Jul 2001 11:37:32 -0500 From: "Gary T. Leavens" Organization: Department of Computer Science, Iowa State University X-Mailer: Mozilla 4.77 [en] (X11; U; HP-UX B.10.20 9000/735) X-Accept-Language: de,fr MIME-Version: 1.0 To: Erik Poll , JML Interest List Subject: Re: JML-Interest: semantics of "let" References: <3B531210.9F5436D5@cs.iastate.edu> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi all, Sorry, but my conclusion in the last email I sent was off by one. I wrote: > I tend to agree with these arguments [by Erik, Michael, and Joeseph]. So we > probably should not use the > semantics of "let" as a syntactic sugar that I proposed. This leaves several > alternative designs for "let". > > 1. Keep the current syntax, but evaluate the variable's defining expression in > the pre-state, bind it to a location there, and use the value of that location > when it is referenced. (This location couldn't be changed by a method program, > so it would have the same value in both the pre-state and the post-state.) > > The disadvantage of this is that there's no easy way to abbreviate expressions > that are to be evaluated in the post-state of a method. > > 2. Drop the current syntax completely, but add let-expressions, which are > evaluated in whatever state they occur in (e.g., the pre-state if they occur in > the requires or assignable clauses), the post-state if they occur in ensures or > signals clauses. > > The disadvantage of this is that there's no easy way to abbreviate expressions > that are used in both the pre- and postcondition of a method. However, one can > use model methods to do this, although that's not very good for ESC/Java and > other tools that don't want to use model methods. > > My preference is for alternative 1, since it seems more expressive, and > alternative 2 doesn't have compelling disadvantages to me. Comments? I meant to say my preference is for alternative 2 (i.e., adding let-expressions) since it seems more expressive, and since it doesn't have any compelling disadvantages. (Sorry for the confusion.) -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1040 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From - Wed Jul 18 18:29:31 2001 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id SAA25923 for jml-interest-list-outgoing; Wed, 18 Jul 2001 18:23:03 -0500 (CDT) Received: from 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 SAA25892; Wed, 18 Jul 2001 18:22:56 -0500 (CDT) Message-ID: <3B561A48.9B87CC31@cs.iastate.edu> Date: Wed, 18 Jul 2001 18:22:48 -0500 From: "Gary T. Leavens" Organization: Department of Computer Science, Iowa State University X-Mailer: Mozilla 4.77 [en] (X11; U; HP-UX B.10.20 9000/735) X-Accept-Language: de,fr MIME-Version: 1.0 To: JML Interest List Subject: Re: JML-Interest: semantics of "let" References: <3B531210.9F5436D5@cs.iastate.edu> <3B53184B.1EF69AE3@cs.iastate.edu> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi all, Perhaps it's slow becuase it's summer. But here at ISU, Yoonsik Cheon and I are still thinking about the semantics of let clauses in JML. Here's an expanded list of alternatives: 0. No let-like clauses or expressions. 1. The current let-clause syntax, let which has scope over remainder of the spec-case in which they occur (e.g., including requires and ensures clauses). Its semantics would be that it evaluates the variable's initializer expression in the pre-state, binds it to a location there, and uses the value of that location when it is referenced. (This location couldn't be changed by a method program, so it would have the same value in both the pre-state and the post-state.) 2. Let-expressions, with a syntax like (\let ) which have scope over just the predicate in their body. The semantics is that the initializer would be evaluated in whatever state they occur in (e.g., the pre-state if they occur in the requires or assignable clauses), the post-state if they occur in ensures or signals clauses. 3. Two similar let-like clauses, with the following syntax. let_pre ; let_post ; These would appear in the same place in the syntax where let-clauses occur now. The scope of the declared variables would be the remainder of the spec-case for let_pre, and all of the postconditions (including exceptional postconditions) in the remainder of the spec-case for let_post. For let_pre, the initializers are evaluated in the pre-state. For let_post the initializers are evaluated in the post-state. There are other possibilities (such as let-clauses nested inside requires, ensures, etc.) which I don't currently favor. The alternatives above can be taken in various combinations also. For example, we could have 1 and 2 or 3 and 2. Since let-clauses are little used, alternative 0 (eliminate them) has a lot to recommend it. For one thing it would simplify tool support for JML. One can use model methods instead of let clauses to abbreviate things if one needs abbreviation. Does anyone really want let-clauses in JML so much they can't live without them? Please speak up if you do! If we do want something like let, alternatives 1 and 3 have the advantage that they allow definitions to be made over an entire spec-case (and nested spec-cases). Alternative 3 seems to be marginally clearer than 1 in the sense that tthe syntax tries to say what state initializers are evaluated in. We think alternative 2 has something to recommend it in terms of expressiveness as well. For example, you could use let-expressions in invariants, history constraints, etc., not just in spec-cases. Yoonsik prefers 1 and 2; this seems to be the most expressive. I'm leaning to 0... Comments? -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1040 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From - Thu Jul 19 09:55:20 2001 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id IAA07155 for jml-interest-list-outgoing; Thu, 19 Jul 2001 08:24:07 -0500 (CDT) 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 IAA07151 for ; Thu, 19 Jul 2001 08:24:04 -0500 (CDT) Received: from localhost (erikpoll@localhost) by plato.cs.kun.nl (8.9.3/8.9.3) with ESMTP id PAA10091 for ; Thu, 19 Jul 2001 15:20:08 +0200 X-Authentication-Warning: plato.cs.kun.nl: erikpoll owned process doing -bs Date: Thu, 19 Jul 2001 15:20:08 +0200 (CEST) From: Erik Poll To: JML Interest List Subject: Re: JML-Interest: semantics of "let" In-Reply-To: <3B561A48.9B87CC31@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 Hi all, > Here's an expanded list of alternatives: > > 0. No let-like clauses or expressions. I could certainly live with this. I've never used any let-clauses in JML specs I wrote, but then I haven't actively considered using them. A quick grep -r "let " reveals that it's not heavily used in any of specs that come with JML distribution either. A definite advantage of not having let's it that it rules out any possible misunderstandings about the state in which they are evaluated :-) Just to get some perspective on how often let-expressions are used: the JML specifications that come with the JML distribution in the directories ../JML/edu/iastate/cs/jml/models ../JML/JDK/java/* contain - about 9000 lines of JML specification - 1068 behavior specifications - 21 let-expressions Of these 21, I can find only one example where evaluation in pre- or post- state would actually makes any difference, and only one example of an abbreviation that is used both in more than one require/ensures clause. Of course, I don't know how representative these files are. Has anybody written JML specs that make heavier use of let-clauses ? > 1. The current let-clause syntax, > let > which has scope over remainder of the spec-case in which they occur (e.g., > including requires and ensures clauses). Its semantics would be that it > evaluates the variable's initializer expression in the pre-state, binds it > to a location there, and uses the value of that location when it is > referenced. > 2. Let-expressions, with a syntax like > (\let ) > which have scope over just the predicate in their body. The semantics is that > the initializer would be evaluated in whatever state they occur in If we go for let-expressions, either of these alternatives seems fine. With both of these alternatives initializers are evaluated at the place where the occur, which is, as the earlier discussion showed, what most people intuitively feel it should be. If I had to choose between these options, my preference is for 2 because here it's clearer in which state let-clauses are evaluated. Option 1 lets people to write let model x = e; ensures ... and they might mistakingly think that e is evaluated in the post-state. > 3. Two similar let-like clauses, with the following syntax. > let_pre ; > let_post ; > > For let_pre, the initializers are evaluated in the pre-state. For let_post > the initializers are evaluated in the post-state. I'm strongly against this. Instead of 3 it would be better to have both 1 and 2, which give the same exressivity, without the need for extra keywords. Let-clauses seem to be fairly rare, and let-clauses where evaluation in pre- or post-state actually makes a difference will be rarer still. Introducing 2 new keywords for this seems ridiculous to me. Best, Erik From - Thu Jul 26 18:51:50 2001 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id SAA17450 for jml-interest-list-outgoing; Thu, 26 Jul 2001 18:47:59 -0500 (CDT) Received: from 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 SAA17420; Thu, 26 Jul 2001 18:47:52 -0500 (CDT) Message-ID: <3B60AC1E.1A3E3343@cs.iastate.edu> Date: Thu, 26 Jul 2001 18:47:43 -0500 From: "Gary T. Leavens" Organization: Department of Computer Science, Iowa State University X-Mailer: Mozilla 4.77 [en] (X11; U; HP-UX B.10.20 9000/735) X-Accept-Language: de,fr MIME-Version: 1.0 To: JML Interest List Subject: JML-Interest: Preconditions of constructors, .jml files, any more opinions on "let"? Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, We're in the midst of moving the ISU tools for JML to a different software base (Curt Clifton's MultiJava compiler, based on the Kopi Java compiler). In doing this we're wondering if anyone really wants to have files in the .jml file format, with no annotation markers. The advantage of getting rid of it would be some minor gain in simplicity. Comments? Another issue is what fields can one refer to in the preconditions of constructors. Recall that the problem is that a blank final field (i.e., one whose declaration doesn't have an initialization), causes problems for run-time checking. Indeed the problem is even worse than this technical issue, since it seems impossible in a Java constructor to check anything until after the call to the superclass's constructor. To get around the technical problem, we had originally proposed the following rule: (constructor rule 1) a constructor's precondition may not refer to instance fields of the "this" object. However, Yoonsik Cheon came up with an example along the following lines, which shows that this rule may not be good. public class Container { public final int MAX_SIZE = 10000; //@ requires size <= MAX_SIZE; public Container (int size) { /*... */ } } In such an example, it seems reasonable to refer to the instance field MAX_SIZE (although perhaps it should be a static field, but never mind that). Returning to the problem, it seems that the real issue is not just if we can do run-time checking of preconditions, but whether the semantics of preconditions for constructors can allow checks at all, and whether it's consistent with the checking done for other methods. Recall that a precondition is supposed to hold just after parameter passing, not after a call to the superclass constructor. So to me, this analysis of the problem suggests that we should relax the rule to say that (constructor rule 2) disallow references to assignable locations in the preconditions of a constructor. This would, in particular, mean that one cannot refer to the values of blank final instance fields in a constructor, since those fields must be definitely assigned by the constructor, and hence must be assignable by it. This solves the technical problem that originally motivated this discussion. Another consequence is that the run-time checker can check the precondition after the call to the superclass constructor, since anything that call could assign to must be assignable. Comments? Finally, we are still looking for input on the "let" issue. More opinions? If you like you can send them to me personally. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1040 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From - Wed Aug 8 10:28:35 2001 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id RAA22729 for jml-interest-list-outgoing; Tue, 7 Aug 2001 17:36:51 -0500 (CDT) Received: from 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 RAA22699; Tue, 7 Aug 2001 17:36:44 -0500 (CDT) Message-ID: <3B706D74.39590281@cs.iastate.edu> Date: Tue, 07 Aug 2001 17:36:36 -0500 From: "Gary T. Leavens" Organization: Department of Computer Science, Iowa State University X-Mailer: Mozilla 4.77 [en] (X11; U; HP-UX B.10.20 9000/735) X-Accept-Language: de,fr MIME-Version: 1.0 To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: New Release of JML, 2.7 and 2.8 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, I've just made another release of JML, 2.8, which is available from the JML ftp site: ftp://ftp.cs.iastate.edu/pub/leavens/JML/ in the file JML.2.8.zip. You can also get it from the JML web page (http://www.cs.iastate.edu/~leavens/JML.html). If you only hear about releases from jml-interest-list, then you may not have heard about releases 2.7, which was a few days ago, and 2.8, which was made on Monday; I had a local problem with sending out the mail. Sorry about that. So this mail describes both releases. Release 2.7 is a bug fix release, but the major bug fixed is that runtime checking of assertions now works to a large extent. Yoonsik Cheon at Iowa State is primarily responsible for the improvements to the runtime assertion checking. Also the release is compatible with JDK 1.4. Some highlights of the changes are summarized below. See the NEWS.txt file in the release for other changes, including several bug fixes. New with release 2.7 (date: 2 August, 2001) major improvements - The runtime assertion checker now works for preconditions, invariants, and even for postconditions, These work with inherited and refined specifications as well, and model variables work, except for model variables that come from other files. (Thanks to Yoonsik Cheon for this.) - The checker now does renaming properly for the --html and --assertc options, thanks to Yoonsik Cheon. This seems to also fix the differences between running the checker on "." versus various named files. - A new model type, JMLDataGroup has been added to the edu.iastate.cs.jml.models package, for use in declaring "data groups" (a la Rustan Leino's OOPSLA '98 paper). - The checker now parses Java's new (in JDK 1.4) assert statement. These are treated as JML assertions if they are within annotations. JML's assume statements now have a similar syntax to the assert statement. minor improvements - The type checker now properly does checking of casts between interface types (see the good test AbstractTransactedMemory.java, thanks to Erik Poll for pointing out the bug). - An option has been added to the checker to supress the date on the --html output. This may be helpful in regression testing (Thanks to David R. Cok). - The type checker now treats assignment expressions correctly (see assignment_in_expression.java). - The README.txt file has a more extensive troubleshooting section. - Fixed specification errors in JML/JDK/java/lang/System.jml arraycopy (Thanks to Erik Poll). - Made JML compile under JDK 1.4. - The word "threadsafe", which is no longer reserved in Java, is no longer reserved in JML's checker (Thanks to Curtis Clifton.) incompatible changes: - Previously deprecated syntax has now been removed. Release 2.8 is also a bug fix release. The only change is various things to make JML run under JDK 1.1. If you don't care about running under JDK 1.1, then there is no special reason to get this release, although some other very small fixes are included. It also works under JDK 1.2.2, 1.3.1, and 1.4.0. Thanks to Yoonsik Cheon of Iowa State for his help on this. (By the way, this is the last release we plan to worry about 1.1 compatability. For future releases we will assume at least JDK 1.2, i.e., Java 2. Please let me know if this is a problem for you.) The changes are summarized below. New with release 2.8 (date: 6 August 2001) major improvements - This release both compiles and passes almost all of our tests under JDK 1.1.8 (the failures are invalid page faults, which may be problems in the 1.1.8 version of the JDK's gc). However, it does so by including some specifications of the JDK (e.g., java.util.Iterator) that are not part of JDK 1.1, in JML/JDK/java/lang. Hence, the JML checker will permit calls to operations that are not actually part of JDK 1.1. On the other hand, if you also type check using javac, this is not a problem. minor improvements - The "instance" modifier can be combined with "ghost" (in interfaces) - More of the builtin types of the JDK are specified, including Iterator and ListIterator. - Some corrections to the specification of java.util.Vector, which has been brought up to JDK 1.4 standards. - A .spec file for BigInteger is included to work around a bug in JML in the JDK 1.1 sources for BigInteger.java. 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 From - Wed Aug 8 12:34:01 2001 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id MAA08736 for jml-interest-list-outgoing; Wed, 8 Aug 2001 12:32:39 -0500 (CDT) Received: from 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 MAA08705; Wed, 8 Aug 2001 12:31:26 -0500 (CDT) Message-ID: <3B717768.1782F34@cs.iastate.edu> Date: Wed, 08 Aug 2001 12:31:20 -0500 From: "Gary T. Leavens" Organization: Department of Computer Science, Iowa State University X-Mailer: Mozilla 4.77 [en] (X11; U; HP-UX B.10.20 9000/735) X-Accept-Language: de,fr MIME-Version: 1.0 To: JML Interest List Subject: JML-Interest: Miscellaneous syntactic and semantic issues in JML Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, Here are some semantic items about JML that I would like to get your opinion about. Please let us know your thoughts about them. 1. JML has a "when" clause that can be used in the specification of concurrency. The basic idea is that, if a method's requires clause is true, then the method can be called, but will wait until it's "when" clause is true. Currently, the order of the clauses in a method specification is given by the following grammar: generic-spec-case ::= [ spec-var-decls ] spec-header [ generic-spec-body ] | [ spec-var-decls ] generic-spec-body spec-header ::= requires-clause [ requires-clause ] ... [ when-clause ] ... [ measured-clause ] ... | when-clause [ when-clause ] ... [ measured-clause ] ... | measured-clause [ measured-clause ] ... simple-spec-body ::= assignable-clause [ assignable-clause ] ... [ ensures-clause ] ... [ signals-clause ] ... [ diverges-clause ] ... | ensures-clause [ ensures-clause ] ... [ signals-clause ] ... [ diverges-clause ] ... | signals-clause [ signals-clause ] ... [ diverges-clause ] ... | diverges-clause [ diverges-clause ] ... In the spec-header we have the "requires", "when", and "measured_by" clauses. The purpose of the spec-header is to distinguish various specification cases (for case analysis). However, I believe that only the requires clause should be used to distinguish between different specification cases, and whether a thread waits and the way that one measures termination shouldn't be used to distinguish between the various cases. Therefore, I think that we should move the "when" and "measured_by" clauses into the "body" of the specification. Furthermore, because the "when" clause describes the action of the method, I believe that it should be moved after the "assignable" clause, which would put it just before the "ensures" clause, which also describes part of the method's action. This would change this part of the grammar to be the following, with corresponding changes elsewhere. generic-spec-case ::= [ spec-var-decls ] spec-header [ generic-spec-body ] | [ spec-var-decls ] generic-spec-body spec-header ::= requires-clause [ requires-clause ] ... simple-spec-body ::= measured-clause [ measured-clause ] ... [ assignable-clause ] ... [ when-clause ] ... [ ensures-clause ] ... [ signals-clause ] ... [ diverges-clause ] ... | assignable-clause [ assignable-clause ] ... [ when-clause ] ... [ ensures-clause ] ... [ signals-clause ] ... [ diverges-clause ] ... | when-clause [ when-clause ] ... ensures-clause [ ensures-clause ] ... [ signals-clause ] ... [ diverges-clause ] ... | ensures-clause [ ensures-clause ] ... [ signals-clause ] ... [ diverges-clause ] ... | signals-clause [ signals-clause ] ... [ diverges-clause ] ... | diverges-clause [ diverges-clause ] ... I don't believe that too many people are currently using the "when" and the "measured_by" clauses currently. So I don't think that there's much of a compatibility problem. It's also of likely that we will need to revise the syntax for concurrency support in the future. However, I think the above changes are reasonable. 1(a). While we are on this subject, JML's current subclassing-contract has two clauses: an accessible clause and a callable clause. It seems pretty clear that the "callable" clause is really only useful in the context of a subclassing contract (in the sense of our OOPSLA 2000 paper). However, at the Formal Techniques for Java Programs workshop this year, and also in conversations with John Boyland, and others, it seems clear that various kinds of static analysis would also like to know what locations a method may read from as well as write to. The locations a method may write to are captured by JML's assignable clause (which has "modifies" and "modifiable" as synonyms). It seems like it might be reasonable to move the "accessible" clause, which describes what locations a method may read from, out of a subclassing_contract section and into the normal method specification. I would suggest that it should go just before the "assignable" clause. The "accessible" clause has a semantics that is similar to the semantics of the "assignable" clause. In particular, it takes into account dependencies. However, instead of having its default for heavyweight specifications be "\nothing", the default would be "\everything". Thus a heavyweight (behavior) specification that omits the "accessible" clause would be thought of implicitly having the clause "accessible \everything;". 2. A somewhat related issue is the difficulty of using the "and" form of a to extending-specifications (i.e., conjoinable-specifications) when the specification being inherited or refined includes a model-program as one of its specification cases. I think that we should simply forbid the use of the conjoinable-specifications when the inherited or refined specification includes a model-program. 3. A completely different issue is where one can put files that are refinements. For example, if one has two files: "Stack.java" and "Stack.java-refined", and if "Stack.java" says that it refines "Stack.java-refined", do they have to appear in the same package? Yes, because I think that they would have to have the same package declaration, otherwise they would be specifying different classes. However, I don't think we need to require them to actually be in the same directory in directory-based implementations. The advantages not requiring them to be in the same directory is that we could, for example, specify parts of the JDK using refinements, leaving the source files for the JDK and one directory, and the refinements in another, both directories being on the "class path". 4. Another question is what to do about model fields and concrete fields with the same name. For example, suppose one declares in an interface and model instance field "theStack" and in an implementation of that interface, one wants to use the same variable name for the concrete variable. We've tried to avoid such things in our examples, but a reference for JML needs to say what to do about them. The semantics I prefer is for the concrete variable to hide the model variable, just following the usual scoping rules of Java. However, this makes it impossible to refer to the model variable in this situation in a "depends" or "represents" clause, and thus are really forces one to choose a different name for the concrete variable. An alternative, suggested by Curt Clifton, is to have a modifier that was the opposite of "spec_public" to deal with such situations. To explain this idea, recall that if one specifies a concrete field such as the following: private /*@ spec_public @*/ int x; Then this can be considered to be syntactic sugar for something like: //@ public model int x; private int _x; //@ private depends x <- _x; //@ private represents x <- _x; where one replaces all occurrences of this "x" in the implementation with "_x". Curt's idea is that when a model instance field, such as "theStack" is already declared in scope, one could write a declaration such as private int[] theStack /*@ representing theStack <- f(theStack) @*/; // (*) As syntactic sugar for something like: private int[] _theStack; //@ private depends theStack <- _theStack; //@ private represents theStack <- f(theStack); In working through this idea, I can see that I'm not really happy with it. The line (*) above that we're desugaring seems pretty unclear because it's referring to different variables that have the same name. Unless there's a great outcry for this sort of thing, I suggest that we just use the normal Java scope rules, which will force people to choose different names for their concrete variables that represent model variables with names that they would otherwise like to use. This seems both the simplest alternative, and the one that produces the clearest specifications. 5. The following question is about the use of Java's "final" modifier with JML's "model" modifier. Normally in Java, one requires that final variables declared without initializer (so-called blank final variables) be "definitely assigned". We should extend this check to model variables by requiring that the concrete variables that they depend on be definitely assigned. 6. The ESC/Java manual says about the "<:" operator that: "An expression of the form S <: T where S and T are specification expressions of type \TYPE is a specification expression of type boolean. It denotes that S is a subtype of T (including the case where S is equal to T). ..." The problem is that Java doesn't explicitly define a notion of "subtype". However, it's pretty clear what "subtype" means for reference types in Java. We propose that JML only allow comparison with <: for reference types. 7. The JML preliminary design document has a grammar that allows documentation comments before jml-declarations, such as invariants and history constraints. There seems to be no good reason for it allowing documentation comments in this spot. We propose deleting them from the grammar. 8. The syntax "\is_initialized" is part of JML on request of the Nijmegen folks. The preliminary design document says that "\is_initialized, which is true just when its reference-type argument is a class that has finished its static initialization." Is there ever in the need for knowing when an object has finished its initialization? For now, I don't plan to make any changes to this unless there is some need for it. 9. It seems that the implicit quantification syntax proposal that Michael Ernst wanted with arrays is dead, due to difficulties in defining it precisely (especially with more than one array involved). Michael, did you want to take this up anymore? Thanks to Curt Clifton for it discussions about many of these points (especially 3-8). Comments on these issues are welcome. I hope it's clear what our decisions will be on most of them if I don't get any comments otherwise. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1040 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From - Tue Aug 28 11:35:57 2001 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id LAA09899 for jml-interest-list-outgoing; Tue, 28 Aug 2001 11:30:21 -0500 (CDT) Received: from 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 LAA09869; Tue, 28 Aug 2001 11:30:16 -0500 (CDT) Message-ID: <3B8BC712.D4717F91@cs.iastate.edu> Date: Tue, 28 Aug 2001 11:30:10 -0500 From: "Gary T. Leavens" Organization: Department of Computer Science, Iowa State University X-Mailer: Mozilla 4.77 [en] (X11; U; HP-UX B.10.20 9000/735) X-Accept-Language: de,fr MIME-Version: 1.0 To: JML Interest List Subject: JML-Interest: Re: Miscellaneous syntactic and semantic issues in JML References: <3B717768.1782F34@cs.iastate.edu> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, So far, all I've heard back from people about these issues (see below) was that John Boyland is happy to have the "accessible" clause being included in method specifications with the suggested default (\everything). I assume this means that either everyone is happy with the ideas, or that everyone is on vacation. So if you're returning from vacation, please let me know if you're unhappy with anything... :-) In implementing the parser for our new version of the JML checker, Curtis Clifton has found that all of the ordering of clauses in method specifications makes the grammar larger than it needs to be. He suggests, and I agree, that we should allow the clauses in the main body of the method specification to occur in any order. We'd still have "forall", "old" (i.e., the old let), and requires (aka pre) in the specification header, but the other clauses (assignable (aka modifies and modifiable), ensures (aka post), signals (aka exsures), diverges, accessible, when, and measured_by) in the body. This has the advantage of making JML more compatible with ESC/Java as well, since I believe ESC/Java doesn't enforce an ordering. We would have warnings (that you could turn off) if the ordering isn't the recommended one. Any objections to that? "Gary T. Leavens" wrote: > > Hi, > > Here are some semantic items about JML that I would like to get your > opinion about. Please let us know your thoughts about them. > > 1. JML has a "when" clause that can be used in the specification of > concurrency. The basic idea is that, if a method's requires clause > is true, then the method can be called, but will wait until it's > "when" clause is true. Currently, the order of the clauses in a > method specification is given by the following grammar: > > generic-spec-case ::= [ spec-var-decls ] spec-header [ generic-spec-body > ] > | [ spec-var-decls ] generic-spec-body > spec-header ::= requires-clause [ requires-clause ] ... > [ when-clause ] ... > [ measured-clause ] ... > | when-clause [ when-clause ] ... > [ measured-clause ] ... > | measured-clause [ measured-clause ] ... > simple-spec-body ::= assignable-clause [ assignable-clause ] ... > [ ensures-clause ] ... > [ signals-clause ] ... > [ diverges-clause ] ... > | ensures-clause [ ensures-clause ] ... > [ signals-clause ] ... > [ diverges-clause ] ... > | signals-clause [ signals-clause ] ... > [ diverges-clause ] ... > | diverges-clause [ diverges-clause ] ... > > In the spec-header we have the "requires", "when", and "measured_by" > clauses. The purpose of the spec-header is to distinguish various > specification cases (for case analysis). However, I believe that only > the requires clause should be used to distinguish between different > specification cases, and whether a thread waits and the way that one > measures termination shouldn't be used to distinguish between the > various cases. Therefore, I think that we should move the "when" and > "measured_by" clauses into the "body" of the specification. > Furthermore, because the "when" clause describes the action of the > method, I believe that it should be moved after the "assignable" > clause, which would put it just before the "ensures" clause, which > also describes part of the method's action. This would change this > part of the grammar to be the following, with corresponding changes > elsewhere. > > generic-spec-case ::= [ spec-var-decls ] spec-header [ generic-spec-body > ] > | [ spec-var-decls ] generic-spec-body > spec-header ::= requires-clause [ requires-clause ] ... > simple-spec-body ::= measured-clause [ measured-clause ] ... > [ assignable-clause ] ... > [ when-clause ] ... > [ ensures-clause ] ... > [ signals-clause ] ... > [ diverges-clause ] ... > | assignable-clause [ assignable-clause ] ... > [ when-clause ] ... > [ ensures-clause ] ... > [ signals-clause ] ... > [ diverges-clause ] ... > | when-clause [ when-clause ] ... > ensures-clause [ ensures-clause ] ... > [ signals-clause ] ... > [ diverges-clause ] ... > | ensures-clause [ ensures-clause ] ... > [ signals-clause ] ... > [ diverges-clause ] ... > | signals-clause [ signals-clause ] ... > [ diverges-clause ] ... > | diverges-clause [ diverges-clause ] ... > > I don't believe that too many people are currently using the "when" > and the "measured_by" clauses currently. So I don't think that > there's much of a compatibility problem. It's also of likely that we > will need to revise the syntax for concurrency support in the future. > However, I think the above changes are reasonable. > > 1(a). While we are on this subject, JML's current > subclassing-contract has two clauses: an accessible clause and a > callable clause. It seems pretty clear that the "callable" clause is > really only useful in the context of a subclassing contract (in the > sense of our OOPSLA 2000 paper). However, at the Formal Techniques > for Java Programs workshop this year, and also in conversations with > John Boyland, and others, it seems clear that various kinds of static > analysis would also like to know what locations a method may read from > as well as write to. The locations a method may write to are captured > by JML's assignable clause (which has "modifies" and "modifiable" as > synonyms). It seems like it might be reasonable to move the > "accessible" clause, which describes what locations a method may read > from, out of a subclassing_contract section and into the normal method > specification. I would suggest that it should go just before the > "assignable" clause. > > The "accessible" clause has a semantics that is similar to the > semantics of the "assignable" clause. In particular, it takes into > account dependencies. However, instead of having its default for > heavyweight specifications be "\nothing", the default would be > "\everything". Thus a heavyweight (behavior) specification that omits > the "accessible" clause would be thought of implicitly having the > clause "accessible \everything;". > > 2. A somewhat related issue is the difficulty of using the "and" form > of a to extending-specifications (i.e., conjoinable-specifications) > when the specification being inherited or refined includes a > model-program as one of its specification cases. I think that we > should simply forbid the use of the conjoinable-specifications when > the inherited or refined specification includes a model-program. > > 3. A completely different issue is where one can put files that are > refinements. For example, if one has two files: "Stack.java" and > "Stack.java-refined", and if "Stack.java" says that it refines > "Stack.java-refined", do they have to appear in the same package? > Yes, because I think that they would have to have the same package > declaration, otherwise they would be specifying different classes. > > However, I don't think we need to require them to actually be in the > same directory in directory-based implementations. The advantages not > requiring them to be in the same directory is that we could, for > example, specify parts of the JDK using refinements, leaving the > source files for the JDK and one directory, and the refinements in > another, both directories being on the "class path". > > 4. Another question is what to do about model fields and concrete > fields with the same name. For example, suppose one declares in an > interface and model instance field "theStack" and in an implementation > of that interface, one wants to use the same variable name for the > concrete variable. We've tried to avoid such things in our examples, > but a reference for JML needs to say what to do about them. The > semantics I prefer is for the concrete variable to hide the model > variable, just following the usual scoping rules of Java. However, > this makes it impossible to refer to the model variable in this > situation in a "depends" or "represents" clause, and thus are really > forces one to choose a different name for the concrete variable. > > An alternative, suggested by Curt Clifton, is to have a modifier that > was the opposite of "spec_public" to deal with such situations. To > explain this idea, recall that if one specifies a concrete field such > as the following: > > private /*@ spec_public @*/ int x; > > Then this can be considered to be syntactic sugar for something like: > > //@ public model int x; > private int _x; > //@ private depends x <- _x; > //@ private represents x <- _x; > > where one replaces all occurrences of this "x" in the implementation > with "_x". > > Curt's idea is that when a model instance field, such as "theStack" is > already declared in scope, one could write a declaration such as > > private int[] theStack /*@ representing theStack <- f(theStack) @*/; > // (*) > > As syntactic sugar for something like: > > private int[] _theStack; > //@ private depends theStack <- _theStack; > //@ private represents theStack <- f(theStack); > > In working through this idea, I can see that I'm not really happy with > it. The line (*) above that we're desugaring seems pretty unclear > because it's referring to different variables that have the same name. > Unless there's a great outcry for this sort of thing, I suggest that > we just use the normal Java scope rules, which will force people to > choose different names for their concrete variables that represent > model variables with names that they would otherwise like to use. > This seems both the simplest alternative, and the one that produces > the clearest specifications. > > 5. The following question is about the use of Java's "final" modifier > with JML's "model" modifier. Normally in Java, one requires that final > variables declared without initializer (so-called blank final variables) > be "definitely assigned". We should extend this check to model > variables by requiring that the concrete variables that they depend on > be definitely assigned. > > 6. The ESC/Java manual says about the "<:" operator that: > "An expression of the form S <: T where S and T are specification > expressions of type \TYPE is a specification expression of type > boolean. It denotes that S is a subtype of T (including the case > where S is equal to T). ..." > The problem is that Java doesn't explicitly define a notion of > "subtype". However, it's pretty clear what "subtype" means for > reference types in Java. We propose that JML only allow comparison > with <: for reference types. > > 7. The JML preliminary design document has a grammar that allows > documentation comments before jml-declarations, such as invariants and > history constraints. There seems to be no good reason for it allowing > documentation comments in this spot. We propose deleting them from the > grammar. > > 8. The syntax "\is_initialized" is part of JML on request of the > Nijmegen folks. The preliminary design document says that > "\is_initialized, which is true just when its reference-type argument > is a class that has finished its static initialization." Is there > ever in the need for knowing when an object has finished its > initialization? For now, I don't plan to make any changes to this > unless there is some need for it. > > 9. It seems that the implicit quantification syntax proposal that > Michael Ernst wanted with arrays is dead, due to difficulties in > defining it precisely (especially with more than one array involved). > Michael, did you want to take this up anymore? > > Thanks to Curt Clifton for it discussions about many of these points > (especially 3-8). > > Comments on these issues are welcome. I hope it's clear what our > decisions will be on most of them if I don't get any comments > otherwise. > -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1040 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From leavens@cs.iastate.edu Mon Dec 17 17:14:13 2001 Date: Mon, 17 Dec 2001 17:04:51 -0600 From: Gary T. Leavens To: JML Interest List Subject: JML-Interest: Re: Miscellaneous syntactic and semantic issues in JML Hi, There hasn't been much traffic on the JML interest mailing list since August. At Iowa State, we have been busy reimplementing the JML checker based on Curtis Clifton's MultiJava compiler. This is going quite well, and we have most of the type checker and some of the runtime assertion checking working. David Cok of Kodak has been generously helping us out with the implementation of the HTML output option. (If you'd like to look at what we're doing with the MultiJava version, you can grab a snapshot from http://www.multijava.org/downloads.html. However, for people who are just interested in using JML, currently we don't recommend using this version.) Also, Yoonsik Cheon has made significant progress on the runtime assertion checker, and we have an interesting how come with the JUnit unit testing framework. This is available in the old version of JML, in a prerelease file that you can get from ftp://ftp.cs.iastate.edu/pub/leavens/JML/JML.zip . In the rest of this note to review some older decisions, and highlight some new outstanding issues. In terms of new issues, were thinking of the leading some of the existing syntax that perhaps you may not be using. So please let me know if you're not using it. OLD/RESOLVED ISSUES We have taken the decisions discussed in the JML interest list in August. These are: 1. To not require much in the way of ordering between clauses in a method specification. we hope to have this in a release, which will be the last, of the old JML soon. > We'd still have > "forall", "old" (i.e., the old let), and requires (aka pre) in the > specification header, but the other clauses (assignable (aka modifies > and modifiable), ensures (aka post), signals (aka exsures), diverges, > accessible, when, and measured_by) in the body. This has the advantage > of making JML more compatible with ESC/Java as well, since I believe > ESC/Java doesn't enforce an ordering. We would have warnings (that you > could turn off) if the ordering isn't the recommended one. 2. To moved the when and measured_by clauses out of the spec-header. This is also not in the implementation yet. 3. To allow the accessible clause both in method specifications and in subclassing_contracts. Again this is not implemented yet. 4. To only use the "<:" operator between reference types in expressions. 5. Can to disallow documentation comments before jml-declarations in a class, such as invariants and history constraints. 6. Cannot and any syntax at this time for saying when an object is initialized. Recall that the current \is_initialized refers to a class having finished its static initialization. 7. Cannot and any implicit complications syntax, such as that discussed with Michael Ernst. (We could never agree on a precise semantics, and the proposal seems to have died.) 8. To require that refinements of a class or interface all be in the same package. However, the files containing these refinements would not have to be in the same directory and directory-based implementations of JML. 9. To use the normal Java scope rules for model variables, which will force people to choose different names for their concrete variables that represent model variables with names that they would otherwise like to use. 10. To require that the concrete variables that a final model variable (i.e., a model variable declared as "final") depends on be definitely assigned. Further comments on these issues are, of course, welcome. NEW/UNRESOLVED ISSUES We had also raised some points earlier which I still think are not completely resolved. > [11 was 2]. A somewhat related issue is the difficulty of using the "and" form > of a to extending-specifications (i.e., conjoinable-specifications) > when the specification being inherited or refined includes a > model-program as one of its specification cases. I think that we > should simply forbid the use of the conjoinable-specifications when > the inherited or refined specification includes a model-program. The problem with this is that the idea isn't modular. It makes me wonder whether the whole idea of the "and" for motivating extending specification is really modular. Perhaps we should abandon it? ESC/Java has never really implemented this. The idea was supposed to be that it's a convenience for the specifier to not have to repeat the precondition; but perhaps it would be better for the reader just have to be repeated? Do you make heavy use of the "and" form of extending specifications? would be okay to abandon it? The following are new issues. 12. Should JML keep the notion of refining files? Currently in JML, one can spread a specification out among several files using refinements. For example, one might have a specification in Foo.refines-java, an implementation in Foo.java, and another specification in Foo.java-refined. This is done using the syntax: refine Foo <- "Foo.java-refined"; for example. The question is, how useful is this? That should be pretty useful, because it really complicates tool support. If we could get by with just putting all the specifications in one file, that would be a significant advantage for tools. (Currently, tools must find all the refinement and combine them before doing semantic analysis.) Because of that, the first MultiJava-based implementation of JML will probably not support refine clauses. The main advantages of refine clauses is that they (i) allow you to split the specification up into several levels among different files, and (ii) that they also let you give a specification to software written by someone else without changing the source files. To handle this second problem, without refine clauses, you have to use some notion like a JMLSRCPATH, and have the version with the specification found first in this path, which probably means copying some of the interface information. That does work, however, the connection between the two files is nowhere apparent in the files. Still, it seems like it may be workable... I had some discussion with Erik Poll about this topic. He actually uses refinements fairly often and would like to retain them in JML. However he's not fond of the current syntax. In our discussions we came up with something along the following lines for a revised syntax: public class Foo /*@ refines "Foo.java-refined" @*/ extends ... implements ... I'm quite interested in (a) whether you use refine clauses, (b) whether you would be willing to do without them, and (c) whether he prefers the new syntax proposed above to the current syntax. I'm undecided but lean towards retaining refine clauses. 13. Should class invariants and history constraints apply to all methods by default, or just to the public methods? Currently our position has been that invariants and history constraints only apply to public methods, but we have a long discussion with the ESC/Java folk who have some fairly convincing arguments on the other side. My summary of this was that it appears that most protected methods do preserve class invariants, and even most private methods do preserve invariants. ESC/Java has an experimental annotation "helper" you can put on a method to have it not assume that the invariant is preserved by the method. In discussions recently with Clyde Ruby, it has also become clear that protected and package-visible methods should preserve invariants, because of Java's scoping rules, which allow such methods be called from other clients in the same package. So what do you think of the following proposal? By default, all methods in a class must preserve the invariant. A user could write the annotation "helper" on a private method, which would make it not preserve the invariant. Please let me know what you think. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1040 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580