From Jan.Dockx@cs.kuleuven.ac.be Fri Jan 11 10:46:02 2002 Date: Fri, 11 Jan 2002 12:21:01 +0100 From: Jan Dockx To: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: Re: Miscellaneous syntactic and semantic issues in JML Whe are a university research group focussed on software development methodology, and we have some years of experience now in using and teaching OOP using BISL. We are in the proces of reviewing JML, to replace our homegrown spec language. Our experience might be interesting for this list. As a first contribution, we want to give our views on the invariants topic: > >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. > First of all, we changed the term "class invariants" to "type invariants" in the Java context. Type invariants occur in Java interfaces also, and we have found that using this term clears up some misunderstandings with our students. On the question at hand, the following: 1) There certainly are methods that cannot uphold class invariants. 2) There are different kinds of type invariants. 1) There certainly are methods that cannot uphold class invariants. Just as an example, consider what we call "bidirectional associations". The most simple example we use in our courses is that of an account that has an optional bank card associated to it. A bidirectional association means that we want to be able to navigate the relationship both from the account to the card, and vice versa. This relationship is a 0..1 - 1..1 relationship: the account optionally can have 1 card, but a card is existentially dependent on its account ("weak type"). 2 versions are possible, depending on which object the developer chooses to carry the responsibility for the bidirectional association. For this example, I choose to put the responsibility in the bank card. (We use the term "relationship" during analysis, "association" during design, and "reference" during implementation. Associations add the directionality to the more abstract concept of relationship). Below is the code for the card and the account. My apologies to the list that the spec has not yet been changed to JML, but I expect that the readers will understand our syntax naturally. package banking; /** * A class for dealing with bank cards, attached to bank accounts. * * @invar A bank card must at all times be attached to a bank account. * | getAccount() <> null * @invar The account to which a bank card is attached, must reference * back to that bank card. * | getAccount().getCard() = this */ public class BankCard { /** * Initialize a new bank card attached to . * * @param account * The account to which the new bank card must be attached. * @pre must be effective. * | account <> null * @pre may not already have a card. * | account.getCard() = null * @post The bank card is attached to . * | (new account).getCard() = this * @post is attached to the new bank card. * | new.getAccount() = account */ public BankCard(Account account) { $account = account; account.linkCard(this); } /** * Terminate this bank card. * * @post The bank card is terminated and detached from its account. * | (new getAccount()).getCard() = null */ public void terminate() { $account.unlinkCard(); $account = null; // not really necessary } /** * Return the account to which this bank card is attached. */ public Account getAccount() { return $account; } /** * is the pincode of this card. */ public boolean isPincode(String code) { ^Ê } /** * Withdraw from the account associated with this card, if * is the pincode of this account. * * @param amount * The amount to be withdrawn. * @param code * The code that is checked against the pincode of this card. * @pre may not be negative. * | amount >= 0 * @post The balance is diminished with the . * | (new getAccount()).getBalance() = * getAccount().getBalance() - amount * @excep BalanceUnderflow * The balance of the associated account would go beyond the * lower limit. * | getAccount().getBalance() - amount < getLowerLimit() * @excep WrongPincodeException * is not the correct pincode for this card. * | not isPincode(code) */ public void withdraw(long amount, String code) throws WrongPincodeException, BalanceUnderflow { if (! isPincode(code)) { throw new WrongPincodeException(); } getAccount().withdraw(amount); // throws BalanceUnderflow // class invariant: getAccount <> null } /** * A reference to the bank account to which this bank card is attached. * * @invar (For non-terminated cards) The reference to the bank account * can never be a null-reference. * | $account <> null */ private Account $account; } --- package banking; /** * A class of bank accounts, involving an association with bank cards. * * @invar The bank card attached to an account, if any, must reference * back to that account. * | if (getCard() <> null) then (getCard().getAccount() = this) */ public class Account { /** * Initialize a new account with no bank card attached to it. * * @post No bank card is attached to the new account. * | new.getCard() = null */ /* the code below is not needed: the result is the same as the default default constructor public Account() { // NOP } */ /** * Terminate this bank account. * * @post This account and its associated bank card, if any, are * terminated. */ public void terminate() { if (getCard() != null) { getCard().terminate(); } } /** * Attach the to this account. * * @param card * The bank card to be attached to this account. * @pre may not be null. * | card <> null * @post is attached to this account. * | new.getCard() = card */ void linkCard(BankCard card) { $bankCard = card; } /** * Detach this account's bank card from this account. * * @post The card is detached from this account. * | new.getCard() = null */ void unlinkCard() { $bankCard = null; } /** * Return the bank card attached to this account, if any. * A null reference is returned if no card is attached. */ public BankCard getCard() { return $bankCard; } /** * A reference to the bank card attached to this account. */ private BankCard $bankCard; } The clue is that, to set up the bidirectional association, the card, that carries the responsibility, needs some access to the internals of the account. This is allowed through the package accessible methods linkCard() and unlinkCard(). These methods are package accessible precisely because using them can violate the type invariants (if (getCard() <> null) then (getCard().getAccount() = this)). They should not be open to just any public user. In fact, in C++, we would use the friend mechanism to restrict their use to exactly the constructor of BankCard and the terminator of BankCard respectively. If all methods are required to uphold the type invariants, implementing bidirectional associations becomes impossible (unless the type invariants are relaxed, and the bidirectional nature if the association is no longer required, leaving all other methods with the burden of dealing with the possible case of a badly setup association). 2) There are different kinds of type invariants. As you can see in the example code above, we also use private invariants. We call these "representation invariants". Obviously, in the above example, they are so simple they loose almost all meaning. Representation invariants are especially interesting when your implementation uses complex data structures, e.g., an array to implement set behavior: /** * Array of references to savings accounts attached to this universal * account. * Effective references are stored at positions 0..$savingscount-1. * @invar A savings account is never registered twice for the same account. * | for each i, j in 0..$savingscount-1: * if ( (i <> j) and ($savings[i] ¼ null) ) * then $savings[i] <> $savings[j] * @invar The unused portion of the array is filled with null-references. * | for each i in $savingscount..$savings.length-1: * $savings[i] = null */ private SavingsAccount $savings[]; /** * @invar The number of savings account is positive. * | $savingscount >= 0 * @invar The number of associated savings accounts does not exceed * the total number of elements in the given array. * | $savingscount <= $savings.length */ private int $savingscount; These representation invariants work as an "attractor" for the correctness proofs of the class. All methods can count on them being true, and make sure that they are uphold. This makes working with the complex data structure much easier, and is easier then to transport knowledge about the data structure in other ways from mutators to inspectors. Representation invariants are in fact private type invariants, and in JML we would use the notation //@ private invariant $savingscount >= 0; e.g.. Note that, theoretically, it might be interesting to also have "helper" methods that do not uphold representation invariants (but we have no examples of such methods). In general, all methods should uphold the representation invariants, at least as a default. Some private methods might depart from this. This further suggest that also protected and package level type invariants could be useful, although we have no examples for it. 3) Conclusion and suggestions So, public methods should uphold public type invariants and private type invariants, always. Private methods should uphold private type invariants, but not public type invariants, but exceptions are theoretically possible. The first section above shows that at least package accessible methods should not be required to uphold public type invariants. On the other hand, we also experienced a need to state that private or protected methods do uphold public type invariants. Sometimes, they actually do so naturally, and it is a big aid in proving the correctness of a public method that uses them, if it was already proven for the private method that it does uphold the public type invariants. A simple example: public class MyClass { //@ public invariant some_complex_invariant /*@ @ behavior @ post some_test ==> some_very_complex_result @*/ public void myMethod() { if (some_test) { myHelperMethod(); } } /*@ @ behavior @ pre some_test @ post some_very_complex_result @*/ private void myHelperMethod() { some_very_complex_algorithm; } } If myHelperMethod() has been proven correct, the proof of myMethod is still very complex because, nominally, myHelperMethod wasn't required to fullfill public type invariants. This has to be proven in the myMethod() proof from the postcondition of myHelperMethod. In our experience, it would a big help if you have a syntax that lets you say that the public invariants are part of the postcondition of the private method, although this isn't required. A suggestion (for an implementation that is proven to uphold public invariants if they applied to begin with): /*@ @ behavior @ pre some_test @ pre public invariants @ post some_very_complex_result @ post public invariants @*/ private void myHelperMethod() { All in all, it might be a good idea to have semantics as follows: * public methods imply the public, protected, package and private type invariants in their post and preconditions * protected methods imply the protected, package and private type invariants in their post and preconditions * package methods imply the package and private type invariants in their post and preconditions * private methods imply the private type invariants in their post and preconditions Less is not possible. If you need less, you should relax the invariants themselves. A syntax is provided to easily state that a method upholds more than required. This is a consistent semantics, although we need to add a PS: 4) PS: yes, but ... (Exemptions) The one thing that bugs me a bit is that, in the programming style I prefer, protected methods should also always uphold the public (and potential protected) type invariants. In that style, there would be a better mode of operation: All methods, by default, uphold all type invariants of all accessibility levels. A syntax is provided to easily state that a given method does not uphold a certain invariant or group of invariants. Only invariants of broader accessibilty can be exempt. * public methods imply the public, protected, package and private type invariants in their post and preconditions * protected methods imply the protected, package and private type invariants in their post and preconditions, and all public type invariants that are not explicity exempt * package methods imply the package and private type invariants in their post and preconditions , and all public and protected type invariants that are not explicity exempt * private methods imply the private type invariants in their post and preconditions, and all public, protected and package level type invariants that are not explicity exempt. A syntax suggestion: /*@ @ behavior @ post some_condition @ post_exempts_protected_invariant some_protected_invariant @ post_exempts_public_invariants \all @*/ somePackageAccessibleMethod() ... (On a side note: this approach suggest another point: JML should offer a mechanism to give clauses a name. A specific invariant could then be exempt by name. We felt a need for such a naming scheme while doing correctness proofs: it is very handy to be able to refer to a given by name.) Although this approach more closely fits my programming style, I think it is more difficult to bring into JML and the tools, so the list might prefer the version proposed in 3. (For the interested reader, on the style that makes protected methods uphold public invariants: This style departs radically from the open-closed principle. In this style, which I prefer, a class offers complete encapsulation of its innards to protected users as it does to its public users, except for openings that are explicitly designed that way through hook methods. Public and protected type invariants acknowledge these openings. Properties that are introduced in a superclass are dealt with, made secure for public and protected invariant violations, and proven correct, once and for all. Subclasses simply have no means by which they could violate superclass public or protected invariants, and therefor their developers are not faced with the burden of taking them into account and proving them. Potentially hook methods are provided to add LSP compliant extra effects, that have to do with properties introduced in the subclass, but nothing can be changed to the behavior of the properties introduced in the superclass. This is in direct contrast to examples given by Meyer in Object Oriented Software Construction, where subclasses manipulate data structures of the superclass directly, even violating representation invariants stated there (a polygon has an array of all its corners, a subclass rectangle uses the array to store only the upper left and bottom right corner, instead of all 4 corners as demanded by the superclass data representation). From leavens@cs.iastate.edu Fri Jan 11 11:04:36 2002 Date: Fri, 11 Jan 2002 11:02:23 -0600 (CST) From: Gary T. Leavens To: Jan Dockx Cc: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: Re: Miscellaneous syntactic and semantic issues in JML Hi Jan, On Fri, 11 Jan 2002, Jan Dockx wrote: > Whe are a university research group focussed on software development > methodology, and we have some years of experience now in using and > teaching OOP using BISL. We are in the proces of reviewing JML, to > replace our homegrown spec language. Our experience might be > interesting for this list. Yes, welcome, and thanks. I'm glad you're considering using JML and find your experiences interesting. A caveat to this reply. Unfortuantely I (and a bunch of other JML-ers) are off to a workshop today, and so this response will be brief and others may be delayed... > As a first contribution, we want to give our views on the invariants topic: > First of all, we changed the term "class invariants" to "type > invariants" in the Java context. Type invariants occur in Java > interfaces also, and we have found that using this term clears up > some misunderstandings with our students. Yes, that's a good point. > On the question at hand, the following: > > 1) There certainly are methods that cannot uphold class invariants. Michael Ernst in a private communication made a similar point; in particular he gave an example (from a standard data structures book) of a queue abstraction with a private method that doesn't preserve an invariant. My summary of his suggestion is the following: > So what you're suggesting ... is that we have > two annotations: "helper", which could be applied to protected and > default access methods to make them not preserve the invariant (and > history constraint by default), and "nonhelper" (which needs a better > name), which could be applied to private methods to make them perserve > the invariant. We could make it so that "pure" and "helper" can't > both be used as method annotations (since a pure method would > automatically preserve all invariants). Your example of a bidirectional association is interesting, and also seems to be pretty convincing, although I haven't had time to study it in detail. > 2) There are different kinds of type invariants. I agree with this, and as you noted, in JML we already have public, protected, private and default access invariants, as well as static variations of these. I agree that private invariants are representation invariants, but protected invariants may also have this flavor. > 3) Conclusion and suggestions > So, public methods should uphold public type invariants and private > type invariants, always. Private methods should uphold private type > invariants, but not public type invariants, but exceptions are > theoretically possible. The first section above shows that at least > package accessible methods should not be required to uphold public > type invariants. > > On the other hand, we also experienced a need to state that private > or protected methods do uphold public type invariants. > All in all, it might be a good idea to have semantics as follows: > > * public methods imply the public, protected, package and private > type invariants in their post and preconditions > * protected methods imply the protected, package and private type > invariants in their post and preconditions > * package methods imply the package and private type invariants in > their post and preconditions > * private methods imply the private type invariants in their post and > preconditions > > Less is not possible. If you need less, you should relax the > invariants themselves. > A syntax is provided to easily state that a method upholds more than > required. I agree completely about the public methods. The rest sounds reasonable, although I think your example of the bidirectional association shows that we need some annotation like "helper" to deal with other methods that don't preserve invariants. I'm still not sure how to deal with these in verification however. So I will still be thinking about it, and hope you and others will too. > 4) PS: yes, but ... (Exemptions) I'll have to come back to this part later... sorry. I welcome more thoughts on this subject. -- 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 Jan 14 23:43:34 2002 Date: Mon, 14 Jan 2002 23:38:53 -0600 (CST) From: Gary T. Leavens To: JML Interest List Cc: Jan Dockx Subject: JML-Interest: Notes from the Java Verification workshop, various JML decisions Hi, I'm in Portland, and yesterday we finished the Java Verification Workshop. We had lots of JML people there, including Bart Jacobs and Erik Poll from Nijmegen, and Rustan Leino (now at Microsoft) and Cormac Flanagan from Compaq SRC, and Michael Ernst from MIT, as well as others who have expressed interest in JML, including Heike Wehrheim and John Field. Bart says that lots of people in Europe on the Verificard project are interested in JML and many are using it. They also seemed happy with it. There is also some interest from Heike Wehrheim and John Field in possibly joining in with the JML efforts to some extent. John Field is particularly interested in model programs and has been working on components. Heike Wehrheim talked about runtime assertion checking in Jass, and has a feature (trace assertions) that perhaps can be added to JML in a more general form as some kind of temporal logic mechanism, perhaps like that in Bandera... I announced at the workshop that we now have a domain for JML "jmlspecs.org". You can now get to the JML web page using the URI: http://www.jmlspecs.org/ We are thinking of reorganizing the JML package structure so that the model types for JML would be found in org.jmlspecs.models instead of the current package edu.iastate.cs.jml.models. We (Michael Ernst, Rustan Leino, Cormac Flanagan, Bart Jacobs, John Field, Heike Wehrheim, Michael Norrish and myself) had a dinner on Saturday night January 12, 2002, where we hashed out some things about JML, driven largely by Michael Ernst's notes about the differences between ESC/Java and JML that affected his work on Daikon. One issue we discussed at length was the semantics of type invariants. In essence we agreed on a semantics that is similar to that in issue 13 of my email to the jml-interest list on Dec 17, 2001. It's also similar in spirit to the technique in part 4 of Jan Dockx's email of a few days ago. Proposed semantics: 1. By default, all instance methods of a type T must preserve all invariants and history constraints (of all visibilities) for type T (both static and non-static ones). All constructors of type T must preserve the static invariant and must establish the non-static invariant of type T. In particular, by default, private methods must preserve invariants and history constraints of type T, and private constructors must perserve static invariants and static history constraints of type T and must establish non-static invariants for the object of type T being initialized. Constructors would have to preserve invariants and history constraints of other objects of type T passed as arguments or in static fields. 2. The specifier can write the modifier "helper" on a private method or constructor. The semantics of this is that a such a helper method does not have to preserve any invariants and history constraints, and that such a helper constructor does not have to preserve static invariants and static history constraints, does not have to establish the invariant for the object being initialized. 3. Only private methods and constructors may be declared with the "helper" modifier. Thus public, protected, and package visibility methods (and constructors) must preserve (establish) invariants and history constraints. There was some discussion about what to do to get around the restrictions of this semantics in cases where a non-private method or constructor doesn't want to preserve the invariant. Here's an example of a pattern that does this without adding any new syntax. It handles a common case (offered by Rustan and Cormac). Suppose, for example, we want to have a public constructor for a type C that does not establish an invariant I, and instead allocates space for the object, and relies on an "init()" method to initialize the object. Cormac and Rustan call such an object that is not initialized "dented". So the idea is to record this in the abstract state of the object with a ghost field: public class C { //@ public ghost boolean dented; //@ ensures dented == true; public C() { /*@ set dented = true; @*/ } //@ requires dented; //@ ensures !dented; public void init() { /*@ set dented = false; *@/ ... } //@ public invariant !dented ==> I; // ... //@ requires !dented; public void m() } This pattern accomplishes several things. The invariant "I" is applied to all methods when the object is not dented. Second, the methods explicitly enforce the sequencing of calling init before the other methods; for example, you have to call init before you can call m on an object. Also, the notion of whether an object is dented or not is recorded in the specification, so clients of C are not burdened with tracking the "dented" status of objects. I believe that this can be used to handle the bidirectional association example in Jan Dockx's email. (Jan, do you want to try that?) This semantics is simple for clients, since all client-visible methods and constructors preserve the visible invariants and history constraints. Michael Ernst promises to take up the topic of array comprehensions again, and to write up a proposed semantics (and send it to this list, I presume). In particular, he will describe what assertions like a[0..5] == b[0..5]+1 mean. (This was supposed to be point 7 in my Dec. 17 email, but it looks like I have a fairly garbled version of it in my email.) We also talked about adding method calls to the assertions supported by ESC/Java, and the semantics of these. This seems to fit in with JML's syntax and semantics better. ESC/Java's source is supposed to be released "any day now", and so we hope that Michael Ernst or someone else will make such changes. We promised to keep diffs from the official ESC/Java release available from the JML web page at Iowa State (www.jmlspecs.org). Another change that would help semantic compatibility with JML would be to allow privacy specifications on invariants in ESC/Java. In my talk at the workshop, I mentioned issue 11 in my Dec 17 email, which is to delete the "and" form of method combination from JML. This seems fairly convincing to me now, and others say that they don't use it and seem convinced. So it has been decided to take it out. Any objections or comments on these decisions? A funny quote from our dinner. Michel Ernst was comparing how permissive JML (and its checker) is compared with ESC/Java. He said: "Does JML allow me to stay out past midnight? Yes." It became clear at the workshop that a high priority in JML's checker should be checking purity annotations. This was already supposed to be a high priority, but John Hatcliff mention that purity was confusing to his students, and it seemed also to be confusing to various people in the audience. Having a way to check it and a clear semantics for it would be quite helpful. We welcome your comments about any of this. -- 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 Kerry.Trentelman@sophia.inria.fr Fri Jan 18 01:40:29 2002 Date: Thu, 17 Jan 2002 10:58:07 +0100 From: Kerry Trentelman To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: Temporal JML Quoting Gary T. Leaven's email 14th Jan: ''...has a feature (trace assertions) that perhaps can be added to JML in a more general form as some kind of temporal logic mechanism, perhaps like that in Bandera...'' Hi all, I'm a student in the Automated Reasoning Group at the Australian National University. I'm currently visiting INRIA Sophia-Antipolis: my work here being supervised by Marieke Huisman. We've been looking at extending JML with temporal logic with influences from the SANTOS/Bandera pattern project. We've come up with an extended specification language (see attached). We think that it can describe all temporal aspects of the JavaCard API. For example, the JCSystem class API specs: beginTransaction throws TransactionExcception.IN_PROGRESS if a transaction is already in progress, abortTransaction throws TransactionException.NOT_IN_PROGRESS if a transaction is not in progress, and commitTransaction throws TransactionException.NOT_IN_PROGRESS if a transaction is not in progress can be written as; after beginTransaction called never beginTransaction enabled & always abortTransaction enabled & always commitTransaction enabled until abortTransaction called, commitTransaction called after abortTransaction called, commitTransaction called always beginTransaction enabled & never abortTransaction enabled & never commitTransaction enabled until beginTransaction called. (By enabled we mean that if the method is called, it has normal behaviour.) Our semantics are still very much a work in progress - and changing by the day. It looks like we'll have to take into consideration the entire state model... Any comments or suggestions on this are very welcome. There should be a paper finished reasonably soon - or this is what I've been telling my supervisor back home anyway :) Cheers, Kerry Trentelman. [ Part 2, "jml.ps" Application/POSTSCRIPT 28KB. ] [ Unable to print this part. ] From kristof.mertens@cs.kuleuven.ac.be Fri Jan 18 01:59:26 2002 Date: Thu, 17 Jan 2002 13:14:32 +0100 From: Kristof Mertens To: JML developers Subject: JML-Interest: invariants Hi all, I'm a researcher at the same university/department/workgroup as Jan Dockx, being Katholieke Universiteit Leuven/Computer Science/Software development methodolgy (http://www.cs.kuleuven.ac.be/) in Belgium. I have coded the Account-BankCard example using the technic proposed in the email of Gary T. Leaven, 14 jan 2002 (technic offered by Rustan and Cormac). I have specified it in JML. The code is added as an attachment. I have made the methods setAccount, setBankCard, removeAccount, removeBankCard public, because in the worst case Account and BankCard may reside in different packages. Remarks about the specification or other parts of the classes are always welcome. Here are my experiences with / ideas about the method: Benefits: - no extensions to JML - it is possible (as for as I can see) Disadvantages: - Most methods in the class/interface have to include a precondition saying that some boolean value has to be false (or true in other implementations). For example in the BankCard class the precondition "requires !changingAccount;" - The previously is not only needed for most methods in the class/interface itself, but also for most methods where the given class/interface is used as a parameter. This is because in most methods you want to be certain that the invariants are satisfied. For example if we made a class Transaction, with a method transact(BankCard .., ..), in which we want to use a BankCard, we want to be sure that the invariants are satisfied (eg that the references really are modelling a bidirectional association) - As long as there is only one bidirectional association in every type it may be workable, but wat happens with multiple associations (or in general: more constructions in one type that need invariants that cannot be satisfied by every method)? See next paragraph. Mutiple bidirection associations: I use bidirection assocciations, but it holds in general for every construction in a type that needs invariants that cannot be satisfied by every method. I think there are 2 sollutions: 1. use multiple boolean fields, 1 for every association 2. only use 1 boolean for all every bidirectional association. In the first solution you need for most methods with that type as parameter (implicit or explicit) a precondition for each boolean saying that the value should be false. If you add a bidirectional association you have to add another boolean and you have to add a precondition in most methods, that use the type, saying that the boolean should be false. In the second case you use only one boolean for all bidirectional associations. If you have for example bidirectional associations A, B, C, ... For every method that doesn't satisfies the invariants for association A, you have to add all the invariants for B, C, ... as pre and postconditions. If you add another association you have to add the preconditions for these new association to every method that doesn't satisfy some invariant. My conclusion: It seems to me that adding the extra preconditions can be a lot of effort, especially when you have multiple constructs that have invariants that can't be satisfied by all methods. Maybe other constructs such as helper methods can reduce those overhead and give also a more natural impression (for me it doesn't feel natural that you have to add preconditions for invariants, IMHO they should hold by default and it should be cited when an invariant isn't satisfied) For multiple constructs that have invariants it may also be a good idea to make it possible to exlude only some invariants. For this last it may be possible to use model methods. Kristof Mertens [ Part 2, Application/ZIP 2.6KB. ] [ Unable to print this part. ] From leavens@cs.iastate.edu Fri Jan 18 23:35:59 2002 Date: Fri, 18 Jan 2002 23:34:36 -0600 (CST) From: Gary T. Leavens To: Stephen Edwards Cc: JML Interest List Subject: Re: JML-Interest: Notes from the Java Verification workshop, various JML decisions Steve, et al. Steve, thanks for your note below, which I think does make sense, and which I'm herewith including as part of the record for the jml-interest mailing list. I have something of a small response below... On Thu, 17 Jan 2002, Stephen Edwards wrote: > This is a reply to one of your list messages. I'm only sending > it to you, but if it makes sense, you can forward it on. > > You wrote: > > > Proposed semantics [for type invariants]: > [...] > > > 2. The specifier can write the modifier "helper" on a private method > > or constructor. The semantics of this is that a such a helper > > method does not have to preserve any invariants and history > > constraints, and that such a helper constructor does not have to > > preserve static invariants and static history constraints, does not > > have to establish the invariant for the object being initialized. > > > > 3. Only private methods and constructors may be declared with the > > "helper" modifier. Thus public, protected, and package visibility > > methods (and constructors) must preserve (establish) invariants and > > history constraints. > > > This is reminiscient of a similar issue in RESOLVE, where the > same issue arises, WRT both abstract invariants and representation > invariants. I agree in spirit with what Gary suggests here, but > wanted suggest an alternative (dual) possibility as well. > > Note that private methods can *only* be called by other methods of > the class, and are likely to most often be "helper" methods as a result. > In general, if they do maintain the invariants, they are likely to > cause a useful, understandable transformation in the object's state > that might be useful as a public method. > > Further, since they are private, they are obviously only called by > other methods of the same class (say, the run-of-the-mill "public" > methods). Most such run-of-the-mill methods, while preserving > invariants on entry/exit, break the invariants internally, only > to restore them before completion. This means that such a > run-of-the-mill method might not be able to call any private methods > except those declared as "helper"s. The main exception is methods > that are built simply by calling other publicly available methods. > > The net effect of your suggestion would be to make the "default" > the less common case, and require the special annotation for the > more common case. > > In RESOLVE, we took the approach of simply not requiring private > operations to uphold (or assume) any invariants, making "helper" > the default. We also decided that if a private op does use an > invariant property, we'd simply repeat the invariant in both the > pre- and postcondition. We could have instead created a modifier > like "helper" that meant the same thing (say, "respects_invariant"), > but we never went that far. One reason is that in over a decade > of experience with components spec'ed this way, I've never seen a > private operation that actually *does* respect its type's invariant > conditions! This may just be a side-effect of the way RESOLVE > code is designed, since I certainly see such private operations in > OO software frequently (albeit without any attempt to formally > specify). > > In the end, though, it makes me wonder what the "default" should > be, since it makes more sense to make the common case the "default" > and require a special modifier for out-of-the-ordinary cases. > > Does that make any sense? > > > -- Steve > > -- > Stephen Edwards 604 McBryde Hall Dept. of Computer Science > e-mail : edwards@cs.vt.edu U.S. mail: Virginia Tech (VPI&SU) > office phone: (540)-231-5723 Blacksburg, VA 24061-0106 > ------------------------------------------------------------------------------- In response, the reason for choosing the default for private methods was that there seems to be some evidence (noted by the ESC/Java folks) that most private methods do in fact preserve invariants. But this is an empirical question, and I do agree that it would be best to make the default go the way that makes for the least amount of writing in the common case. I looked at some of the methods in the JDK collection classes about this, and I was surprised to find that most private methods I looked at do seem to preserve the invariant. But I'm quite interested to hear from anyone who has time to look at some representative sample of Java code and can tell us which way the decision goes for it. -- 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 david.cok@kodak.com Wed Jan 23 17:25:44 2002 Date: Wed, 23 Jan 2002 16:55:30 -0500 From: david.cok@kodak.com To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: invariants and helper methods From: David R Cok I can make a few comments about invariants and helper methods from personal experience. Last year I was experimenting with jml and esc/java by annotating an existing java application. One of the comments I sent back to the esc/java team was precisely the one of past emails: the need to relax some invariants when calling some (helper) methods. I encountered this problem in two types of cases: a) the one already mentioned: two objects that need to point at each other. The invariants for the two classes require consistent object references, but they have to be set up serially, so there are some method calls for which the invariants do not hold (at least at entrance to the method). b) providing an initialization function for a group of common methods, particularly constructors. I had a group of constructors all call one init () method to consistently initialize an object without replicating code (and it was not possible to have one of the constructors do the dirty work). The invariants did not hold at the time init() was called. In this case init() was private and purely a helper. The work-arounds were messy. In particular I tried something akin to Rustan and Cormac's "dented" pattern described in Gary's note. In the case of a private helper function, it required sprinkling a "dented" or "isInitialized" predicate all around all the method pre- and post-conditions of the methods of the class. This was a lot of editing and complicated the verification; it made the conditions harder to understand and harder to prove. Also, since the initialization was private and confined to the constructors, from a public point of view, everything should have been initialized. So the "isInitialized" predicate should have been private. But it had to be in all the (public) invariants and preconditions as well. In the case where the helper function is public (e.g. the init() method of the previous email), one has no choice but to use a "dented" predicate to describe whether init() has been called on an object. In this case, the public use of "dented" or its equivalent matches the semantics of the set of methods of the class. However, I found that introducing the verification conditions necessary to be able to verify that use of the class was correct (and getting them all to verify) was worse than introducing an innocent const in a C++ program. One has to add conditions to assure that everywhere an object of that type is used, throughout all the classes in which it is used, one can prove what state the object is in. Again - consistent with the semantics and sometimes necessary - but messy in practice. I think that some judicious use of history constraints would help - and is worth exploring - but I will tread cautiously with a design of that sort that I intend to try to verify [ perhaps there is at least some truth in saying that the value of automated software verification tools is that if one can generate a software design with verification conditions that a computer will agree are correct, it will be trivial to convince a human.] Note that in the example given, namely: public class C { //@ public ghost boolean dented; //@ ensures dented == true; public C() { /*@ set dented = true; @*/ } //@ requires dented; //@ ensures !dented; public void init() { /*@ set dented = false; *@/ ... } //@ public invariant !dented ==> I; // ... //@ requires !dented; public void m() } we also need either (a) to add "ensures !dented;" on every method besides the constructor, or (b) use a history constraint to require that once an object is !dented it remains !dented. ( And then any methods called from methods of C need to be sure to be able to convince the verification checker that they preserve non-dentedness... ) In the case of private helper functions, I am definitely in favor of some ability to relax invariant requirements. A few comments on that: There was some discussion of having the default be that private methods do not satisfy invariants on the assumption that that is the common case and one wants to avoid extra writing. I would argue that the choice should be made in favor of the reader and not the writer of the code. After all, we hope that the specs are read often (and written only once :-). So I would say that the default should be the same as every other method. Furthermore, although using "helper" to indicate that no constraints are required or ensured is better than nothing, that is a broad brush approach. I would prefer the ability to turn off individual, named, invariants explicitly for given methods. The use of names avoids having to create rules describing when invariants are the same and avoids problems if an invariant is changed at one lexical location and other locations are missed. The names could also be used in error messages. I realize that this requires more significant changes to the grammar and to tools. One approach might be to utilize a pattern like this (stretching the usual semantics of model variable initialization): //@ model boolean allIsConsistent = ... complicated invariant expression ...; //@ invariant allIsConsistent ; //@ allows !allIsConsistent; private void init() { } Alternatively: //@ invariant allIsConsistent = ... complicated invariant expression ...; //@ allows !allIsConsistent; private void init() { } If the text following the "allows" keyword is kept restricted (e.g. to a positive or negative instance of an invariant name) the semantics should not be too complicated to specify. ------------- Also, Gary wrote: > We also talked about adding method calls to the assertions supported > by ESC/Java, and the semantics of these. I certainly needed that when trying jml and esc/java out on a "real" (if not commercial) problem, along with support for "represents" in order to use public model variables rather than private class variables in specifications. ----------------- The relaxing of restrictions on the order of specification clauses will solve one problem: the obscure (parser) error messages one can get when the clauses are out of order. - David From david.cok@kodak.com Wed Jan 23 17:30:07 2002 Date: Wed, 23 Jan 2002 15:47:22 -0500 From: david.cok@kodak.com To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: documentation before invariants, and other matters From: David R Cok This is a rather belated comment (perhaps too late), owing to my just having caught up with some discussions from last year. Gary commented: > 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. and later > 5. Can to disallow documentation comments before jml-declarations in a class, such as invariants and history constraints. This is not implemented in current jmldoc, but I had thought allowing such comments to be appropriate and useful in the context of jmldoc (javadoc with jml information). Consider public class Mine { /** An array of Integer objects. */ public Vector a; /** This invariant requires that the Vector a (if it is not null) be sorted in increasing order. */ public invariant ...a fairly complicated expression.... ; ... } The associated (jmldoc-produced) html page for the class will list members, fields, invariants, etc. of the class. For each one, some degree of explanation and documentation is appropriate (required???). Why not provide a means to explain the invariants as well? ------------------ On ordering of jml clauses - David From Jan.Dockx@cs.kuleuven.ac.be Thu Jan 24 15:11:36 2002 Date: Thu, 24 Jan 2002 12:18:41 +0100 From: Jan Dockx To: jml-interest-list@cs.iastate.edu Cc: Marko van Dooren , Nele Smeets , Kristof Mertens , Eric Steegmans Subject: JML-Interest: Re: Notes from the Java Verification workshop, various JML decisions We are studying the Preliminary Design document, and we have some questions for the authors. We discuss the August 2001 version, the latest at the time of this writing. If the questions are answered somewhere already, a reference would be appreciated.

Questions

Model-Based Approach

(abstract) JML combines this idea from Eiffel with the model-based approach to specifications, typified by VDM and Larch, which results in greater expressiveness. (1.3) However, Eiffel specifications, as written by Meyer, are typically not as detailed as model-based specifications written, for example, in Larch BISLs or in VDM-SL. a) It is not clear to us what is meant by model-based approach. This is a pretty vague term which has different connotations in different context, e.g., AI and formal specications. Can you elaborate? b) The clause greater expressiveness caused some commotion. Normally, this would mean that some things could not be expressed, and thus specified, only with assertions, as in Eiffel, which can be expressed in JML, because of the model based approached. This is surprising to us, and we would like an example.

Initially Clause

What does the initially clause mean?
  • the postconditions of the initialization code; or
  • constraints on the postconditions of all constructors of the type and the subtypes (or part of the postconditions of all constructors of the type and the subtypes).

Invariants and Construction

(2.1) An invariant must hold for each state outside of a public method's execution, and at the beginning and end of each such execution. When does an invariant "start": after the allocation and default initialization (i.e., after the new), after the initialization code, or after the completion of a constuctor's body?

Assignable and Inheritance

Can a method overwritten in a subclass add assignable clauses, or remove them?

Note: Problems With the Examples

The examples on page 2 and 3, which we believe are intended to be equivalent, are not. In the example on page 2, -6 is an allowed result for isqrt(36). In the example on page 3 it is not. We seem to remember from the first reading that operators, such as addition, in a JML specification, are the Java operation, and not the mathematical addition. In that case, both examples have a problem: the + 1 which is done twice in each example might overflow. Solutions might be an upper bound precondition, or using mathematical addition in the language (we believe the latter is the way to go in the long term). There probably will be more in the future ... From Marko.vanDooren@cs.kuleuven.ac.be Thu Jan 24 15:12:37 2002 Date: Thu, 24 Jan 2002 14:16:29 +0100 From: Marko van Dooren To: Jan Dockx , jml-interest-list@cs.iastate.edu Cc: Nele Smeets , Kristof Mertens , Eric Steegmans Subject: Re: JML-Interest: Re: Notes from the Java Verification workshop, various JML decisions > We seem to remember from the first reading that operators, such as > addition, in a JML specification, are the Java operation, and not the > mathematical addition. In that case, both examples have a problem: > the + 1 which is done twice in each example might overflow. Solutions > might be an upper bound precondition, or using mathematical addition > in the language (we believe the latter is the way to go in the long > term). As kristof pointed out in his mail (internal one), mathematical addition will cause problems when using floating points and doubles. It is very unlikely that the mathematical result of for example a multiplication of 2 floating points will be a floating point. There will be an error on the result, and thus a mathematical specification would be violated. To solve this, IEEE floating point rules could be used (although I understood from colleagues that java floating point is not very good, which would cause significant problems). However, on overflow, IEEE does not wrap , but returns NAN. This isn't very useful in the specification. Additionally, if you want to be correct, you must specify an error bound for the result. a+b+c is not necessarily equal to c+b+a due to relative rounding errors. To perform such a calculation as stable as possible, the numbers should be sorted, and added starting from the smallest value (which is an enormous overhead). Explicitly specifying an error bound for all such calculations, seems way too much troubles for ordinary applications where ultimate precision is not required, but it would be necessary since there is no default bound. I doubt there are many programmers who could even perform such a calculation, which defeats the purpose of JML. Therefore, I think mathematical rules in general are not possible. With long and int, I don't see any problems when considered in isolation, but then you have different rules for int,long and float,double. Not specifying an error bound however might render the specification useless because depending on the numerical condition and the numerical stability of the calculation, about any error can occur. Actually, even java semantics aren't necessarily correct because the calculation might be performed in another way than mentionned in the specification. Marko No. 5 From kristof.mertens@cs.kuleuven.ac.be Thu Jan 24 15:12:57 2002 Date: Thu, 24 Jan 2002 15:30:42 +0100 From: Kristof Mertens Cc: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: Re: Notes from the Java Verification workshop, various JML decisions Marko van Dooren wrote: > To solve this, IEEE floating point rules could be used (although I > understood from colleagues that java floating point is not very > good, which would cause significant problems). However, on > overflow, IEEE does not wrap , but returns NAN. This isn't very > useful in the specification. IEEE works with +0 -0 +infinity and -infinity for overflow. NAN does also exist, but is not used in overflows. JLS: 4.2.3 Floating-Point Types, Formats, and Values A NaN value is used to represent the result of certain invalid operations such as dividing zero by zero. NaN constants of both float and double type are predefined as Float.NaN and Double.NaN Positive zero and negative zero compare equal; thus the result of the expression 0.0==-0.0 is true and the result of 0.0>-0.0 is false. But other operations can distinguish positive and negative zero; for example, 1.0/0.0 has the value positive infinity, while the value of 1.0/-0.0 is negative infinity. From leavens@cs.iastate.edu Thu Jan 24 17:10:11 2002 Date: Thu, 24 Jan 2002 17:00:47 -0600 (CST) From: Gary T. Leavens To: Jan Dockx Cc: jml-interest-list@cs.iastate.edu, Marko van Dooren , Nele Smeets , Kristof Mertens , Eric Steegmans Subject: Re: JML-Interest: Re: Notes from the Java Verification workshop, various JML decisions Jan, Thanks for your questions and interest. These are all good questions. Answers from me will be slow for the next few days; others are welcome to say things also... On Thu, 24 Jan 2002, Jan Dockx wrote: > We are studying the Preliminary Design document, and we have some > questions for the authors. We discuss the August 2001 version, the > latest at the time of this writing. If the questions are answered > somewhere already, a reference would be appreciated. > >

Questions

> >

Model-Based Approach

> (abstract) JML combines this idea from Eiffel with the > model-based approach to specifications, typified by VDM and Larch, > which results in greater expressiveness. > (1.3) > However, Eiffel specifications, as written by Meyer, are > typically not as detailed as model-based specifications written, for > example, in Larch BISLs or in VDM-SL. > a) It is not clear to us what is meant by model-based approach. This > is a pretty vague term which has different connotations in different > context, e.g., AI and formal specications. Can you elaborate? This terminology is adapted from Jeannette Wing's paper: @Article{Wing90a, Key="Wing", Author="Jeannette M. Wing", Title="A Specifier's Introduction to Formal Methods", Journal="Computer", Volume=23, Number=9, Month=Sep, Year=1990, Pages="8-24", Annote="Survey with categorized references on formal methods and specification languages." } That said, I can see how it's somewhat confusing. > b) The clause greater expressiveness caused some commotion. Normally, > this would mean that some things could not be expressed, and thus > specified, only with assertions, as in Eiffel, which can be expressed > in JML, because of the model based approached. This is surprising to > us, and we would like an example. When I refer to expressiveness of a langauge I mean that it's easier to say the kind of things you want to say. For example, consider the humble stack. In JML, you can have a model, say a sequence, which makes it easy to say that when you push an element on a stack, the other elements are unchanged. This is relatively more difficult to say in Eiffel, which doesn't provide the notion of a specification-only variable, and which doesn't provide something like JML's model types (e.g., JMLObjectSequence). But the case can also be made much more strongly that JML really can express things that Eiffel cannot express at all. For example, JML has quantifiers, and Eiffel doesn't. JML allows one to express both partial and total correctness and Eiffel only can discuss partial correctness. JML also has frame axioms which Eiffel doesn't have. >

Initially Clause

> What does the initially clause mean? >
    >
  • the postconditions of the initialization code; or >
  • constraints on the postconditions of all constructors of the > type and the subtypes (or part of the postconditions of all > constructors of the type and the subtypes). >
You can give a specification in JML for initialization code directly. The initially clause means that objects have to always appear in a state that is reachable (by using the methods) from a state that satisfies the initially clause. It's most useful if you don't have constructors or initializers (as in interfaces and abstract classes). >

Invariants and Construction

> (2.1) An invariant must hold for each state outside of a public > method's execution, and at the beginning and end of each such > execution. > When does an invariant "start": after the allocation and default > initialization (i.e., after the new), after the initialization code, > or after the completion of a constuctor's body? Good question. Invariants should hold at the end of (non-private and non-helper) constructors, certainly. Invariants shouldn't be required to hold after allocation and default initialization. I think Meyer has a picture in OOSC that illustrates the idea, something like: (allocation/creation) | v constructor returns | invariant holds | V invariant holds method call | invariant holds | V invariant holds method call | invariant holds . . . | V invariant holds method call So the invariant must hold at the end of constructors, but is not assumed to hold not in their pre-state. And invariants are assumed and assured by each method. If there are destructors, the invariant holds in their pre-state but not in their post-state. >

Assignable and Inheritance

> Can a method overwritten in a subclass add assignable clauses, or > remove them? I'm not sure what you mean here... >

Note: Problems With the Examples

> The examples on page 2 and 3, which we believe are intended to be > equivalent, are not. In the example on page 2, -6 is an allowed > result for isqrt(36). In the example on page 3 it is not. You're right. Thanks. > We seem to remember from the first reading that operators, such as > addition, in a JML specification, are the Java operation, and not the > mathematical addition. In that case, both examples have a problem: > the + 1 which is done twice in each example might overflow. Solutions > might be an upper bound precondition, or using mathematical addition > in the language (we believe the latter is the way to go in the long > term). Yes, you are right about this as well. There is certainly something of a problem with overflow in such examples. > There probably will be more in the future ... Great, thanks. -- 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 Thu Jan 24 17:10:35 2002 Date: Thu, 24 Jan 2002 17:07:03 -0600 (CST) From: Gary T. Leavens To: Marko van Dooren Cc: Jan Dockx , jml-interest-list@cs.iastate.edu, Nele Smeets , Kristof Mertens , Eric Steegmans Subject: Re: JML-Interest: Re: Notes from the Java Verification workshop, various JML decisions Hi Marko, et al., On Thu, 24 Jan 2002, Marko van Dooren wrote: > As kristof pointed out in his mail (internal one), mathematical addition will > cause problems when using floating points and doubles. It is very unlikely > that the mathematical result of for example a multiplication of 2 floating > points will be a floating point. There will be an error on the result, and > thus a mathematical specification would be violated. > > To solve this, IEEE floating point rules could be used (although I understood > from colleagues that java floating point is not very good, which would cause > significant problems). However, on overflow, IEEE does not wrap , but returns > NAN. This isn't very useful in the specification. I thought that Java did use the IEEE 754 floating point standard (see JLS p. 35). NaN is a problem because it doesn't compare well under equality. For example, Double.NaN == Double.NaN is defined to be false! I also agree that if one is serious about floating point, one must use numerical analysis techniques. It would be nice to define some model methods to give "approximate equality" in a way that would be both mathematically rigorous, useful for run-time checking, and readable. I leave that to those who know more about it... or who have more time. -- 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 edwards@cs.vt.edu Fri Jan 25 10:23:13 2002 Date: Fri, 25 Jan 2002 09:29:50 -0500 From: Stephen Edwards To: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: invariants and helper methods david.cok@kodak.com wrote: > Alternatively: > > //@ invariant allIsConsistent = ... complicated invariant expression ...; > > //@ allows !allIsConsistent; > private void init() { > } > > If the text following the "allows" keyword is kept restricted (e.g. to a > positive or negative instance of an invariant name) the semantics should > not be too complicated to specify. David's suggestion here seems like a much more useful, elegant addition than the "helper" keyword to me. It also aids readability more by speaking directly to the behavior of the method. One possible superficial change in word choice, though: the connotation of "allows" suggests that the method is happy to operate when the pre-state does not satisfy the invariant, but does not directly imply anything about (the possible lack of) invariant satisfaction in the post-state. Another phrasing, like "ignores " or "omits " might both simplify the structure (no bangs needed--just a list of identifiers) and better convey the intent that the invariant does not apply either before or after the call. -- Steve -- Stephen Edwards 604 McBryde Hall Dept. of Computer Science e-mail : edwards@cs.vt.edu U.S. mail: Virginia Tech (VPI&SU) office phone: (540)-231-5723 Blacksburg, VA 24061-0106 ------------------------------------------------------------------------------- From david.cok@kodak.com Fri Jan 25 10:25:02 2002 Date: Fri, 25 Jan 2002 10:28:13 -0500 From: david.cok@kodak.com To: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: invariants and helper methods From: David R Cok If Stephen Edwards idea of using "ignores" or some equivalent to turn off a requirement of an invariant were adopted, then one should also add a mechanism to turn it back on as a postcondition or precondition as well. Such as: //@ invariant allIsConsistent = ... complicated invariant expression ...; //@ ignores allIsConsistent; //@ ensures allIsConsistent; // invariant satisfied on exit private void init() { } //@ ignores allIsConsistent; //@ requires allIsConsistent; // invariant satisfied on entry private void release() { } //@ ignores allIsConsistent; // invariant not necessarily satisfied on either entry or exit private void helper() { } Naming has other potential uses as well, such as //@ requires consistentLinks = ... complicated boolean expression...; //@ ensures consistentLinks; public void m() {...} or //@ requires consistentLinks = ... complicated boolean expression...; public void m() {...} //@ requires consistentLinks; public void n() { ...} In these cases, I think that a macro-like semantics will make intuitive sense: use of a name is a pure textual substitute for the full expression. Then there is perhaps even //@ define consistentLinks = ... complicated expression...; //@ requires consistentLinks; public void m() {...} //@ requires consistentLinks && name != null; public void p(String name) { ...} But now we are getting to the point where a pure model method may be the better approach: /*@ public model boolean consistentLinks() { return ... complicated expression...; } @*/ //@ requires consistentLinks(); public void m() {...} //@ requires consistentLinks() && name != null; public void p(String name) { ...} - David From erikpoll@cs.kun.nl Fri Jan 25 13:40:30 2002 Date: Fri, 25 Jan 2002 19:32:08 +0100 (CET) From: Erik Poll To: Jan Dockx Cc: jml-interest-list@cs.iastate.edu, Marko van Dooren , Nele Smeets , Kristof Mertens , Eric Steegmans Subject: JML-Interest: Re: Jan Dockx question about adding/removing assignable clauses Hallo Jan, On Thu, 24 Jan 2002, Jan Dockx wrote: >

Assignable and Inheritance

> Can a method overwritten in a subclass add assignable clauses, > or remove them? You cannot add assignable clauses for a method in the subclass, but you can remove them. This is because JML insists that a method in a subclass obeys the specs given for that method in parent class as well as any additional specs given in the subclass itself. (This principle, called "specification inheritance", guarantees that any subclass is a "behavioural subtype" of its parent.) For example, in public Parent { public int x,y,z; //@ requires true; //@ assignable x,y; //@ ensures true; void m() { ... } } public Child extends Parent { //@ requires true; //@ assignable x,y,z; //@ ensures true; void m() { ... } } the implementation of m in Child has to obey both the spec given in Child and the spec given in Parent. So, although the spec in Child allows assigments to z, the spec in Parent does not, and the the implementation of m in Child is not allowed to assign to z, as this would violate the spec given in Parent. On the other hand, for public AnotherChild extends Parent { //@ requires true; //@ assignable x; //@ ensures true; void m() { ... } } the implementation of m in AnotherChild is only allowed to assign to x, and not to y. (Another way to understand this is that specification of a subclass should be as least as strong as the specification of its parent. Since adding assignable clauses would weaken the specification, this is not possible. Conversely, removing assignable clauses strengthens a specification, so this is OK.) In practice, the fact that it's not possible to add assignable clauses can be very annoying. Many subclasses have some additional fields that one would want to add to be assignable clause. Eg, think of the classic public Point2 { public int x,y; //@ assignable x,y; move() { ... } } public Point3 extends Point2 { public int z; move() { ... } } We might want to allow the move in Point3 to modify the z-coordinate, but - as explained above - this is not possible. The way around this is to use model variables: if we specify that the method in the parent class can modify a model variable, then in the subclass we are still free to extend the set of variables on which this model variable depends. Eg. public Point2 { //@ public model Object position; int x,y; //@ public depends postion <- x,y //@ assignable position; move() { ... } } (The type of position is not relevant here.) public Point3 extends Point2 { int z; //@ public depends position <- z; move() { ... } } Something similar happens in the example of PlusAccount extending Account in Section 2.6 of the Preliminary Design paper. The method deposit in class Account is allowed to assign to the model variable "credit", but the class PlusAccount declares that credit actually depends on two additional (model) variables - namely savings and checking - so that the implementation of credit in PlusAccount can modify savings and checking as well as credit. (Another solution to this problem of allowing a subclass to modify its additional state - which is in essence really equivalent to the use of model variables in JML - is discussed in K. Rustan M. Leino. Data groups: Specifying the modification of extended state. In Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA '98), volume 33(10) of ACM SIGPLAN Notices, pages 144-153, October 1998. . ) > We seem to remember from the first reading that operators, such as > addition, in a JML specification, are the Java operation, and not the > mathematical addition. In that case, both examples have a problem: > the + 1 which is done twice in each example might overflow. Solutions > might be an upper bound precondition, or using mathematical addition > in the language (we believe the latter is the way to go in the long > term). As Gary already remarked, you are right about this. However, note that JML does offer a potential way out in such situations . If the standard types and operations that Java provides are not good enough, you can use objects of some Java API class in your specification that does satisfy your needs; eg. instead of Java integers you could use java.lang.BigInteger's to specify isqrt. Or, if that fails, you could write your own (model) class that does meet your needs. Eg I assume that Gary wrote the class edu.iastate.cs.jml.models.JMLInfiniteInteger because in some situation java.lang.BigInteger didn't work. Groeten, Erik ------------------------------------------------------------------------- Erik Poll http://www.cs.kun.nl/~erikpoll/ erikpoll@cs.kun.nl phone: +31 24-3652710 fax: +31 24-3653137 Computing Science Institute - University of Nijmegen - The Netherlands From leavens@cs.iastate.edu Mon Jan 28 10:22:57 2002 Date: Mon, 28 Jan 2002 09:33:38 -0600 (CST) From: Gary T. Leavens To: Erik Poll Cc: Jan Dockx , jml-interest-list@cs.iastate.edu, Marko van Dooren , Nele Smeets , Kristof Mertens , Eric Steegmans Subject: Re: JML-Interest: Re: Jan Dockx question about adding/removing assignable clauses, finiteness Hi Eirk, Jan, et al., Erik, thanks for your reply on this. I just wanted to add my two cents to the discussion... On Fri, 25 Jan 2002, Erik Poll wrote: > On Thu, 24 Jan 2002, Jan Dockx wrote: > > >

Assignable and Inheritance

> > Can a method overwritten in a subclass add assignable clauses, > > or remove them? > > You cannot add assignable clauses for a method in the subclass, > but you can remove them. > > This is because JML insists that a method in a subclass obeys the specs > given for that method in parent class as well as any additional specs > given in the subclass itself. (This principle, called "specification > inheritance", guarantees that any subclass is a "behavioural subtype" > of its parent.) That's right. Thanks. > The way around this is to use model variables: if we specify that the > method in the parent class can modify a model variable, then in the > subclass we are still free to extend the set of variables on which > this model variable depends. ... > (Another solution to this problem of allowing a subclass to modify > its additional state - which is in essence really equivalent to the > use of model variables in JML - is discussed in > K. Rustan M. Leino. > Data groups: Specifying the modification of extended state. > In Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented > Programming, Systems, Languages, and Applications (OOPSLA '98), > volume 33(10) of ACM SIGPLAN Notices, pages 144-153, October 1998. . > ) I just wanted to be sure to not leave anyone with the impression that our solution to the modification of extended state problem that uses dependencies is original in JML. Actually it is also taken from Rustan Leino's work, his 1995 Ph.D. thesis. @PhdThesis{Leino95, author = {K. Rustan M. Leino}, title = {Toward Reliable Modular Programs}, school = {California Institute of Technology}, year = 1995, key = {Leino}, note = {Available as Technical Report Caltech-CS-TR-95-03.} } This is where the dependency idea first appears. JML adops this solution because it seems better for verification than datagroups. However, if you like datagroups, you can use the type edu.iastate.cs.jml.JMLDataGroup for the declaration of a model variable which represents a datagroup. Peter Mueller's thesis (soon to appear as a LNCS volume) also explores this issue. @Book{Mueller01, key = {M{\"u}ller}, author = {Peter M{\"u}ller}, title = {Modular Specification and Verification of Object-Oriented programs}, Publisher="Springer-Verlag", Series = LNCS, Volume = 2262, Year=2002, Note="The author's PhD Thesis. Available from http://www.informatik.fernuni-hagen.de/import/pi5/publications.html." } > > We seem to remember from the first reading that operators, such as > > addition, in a JML specification, are the Java operation, and not the > > mathematical addition. In that case, both examples have a problem: > > the + 1 which is done twice in each example might overflow. Solutions > > might be an upper bound precondition, or using mathematical addition > > in the language (we believe the latter is the way to go in the long > > term). > > As Gary already remarked, you are right about this. > > However, note that JML does offer a potential way out in such situations . > If the standard types and operations that Java provides are not good > enough, you can use objects of some Java API class in your specification > that does satisfy your needs; eg. instead of Java integers you could use > java.lang.BigInteger's to specify isqrt. Or, if that fails, you could > write your own (model) class that does meet your needs. Eg I assume > that Gary wrote the class > edu.iastate.cs.jml.models.JMLInfiniteInteger > because in some situation java.lang.BigInteger didn't work. Actually, the type JMLInfiniteInteger was intended to be a model of the integers with a positive and negative infinity appended. These were actually written not to solve the finiteness problems with the integers, but to be used with Eric Hehner's idea of specification with partial correctness and a time variable. @Article{Hehner99, author = {Eric C. R. Hehner}, title = {Specifications, programs, and total correctness}, journal = {Science of Computer Programming}, year = 1999, key = {Hehner}, volume = 34, pages = {191-205}, annote = {Argues that a formal specification is a boolean expression, that a program is a formal specification, and that total correctness is worse than partial correctness plus time. 20 references.} } I don't believe that the specification and implementation of JMLInfiniteInteger allow the integers to grow to truly unbounded size. However, perhaps they can be adjusted by making it seem as if the JVM fails when the underlying BigIntegers run out of space, as that would relieve the implementation from its contract (and would probably be good enough for practical purposes). -- 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 Jan.Dockx@cs.kuleuven.ac.be Tue Feb 26 23:32:40 2002 Date: Tue, 26 Feb 2002 11:54:39 +0100 From: Jan Dockx To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: jml tool problem Is this a bug in jml? I have a model interface in a .jml file which defines 1 boolean method. I have a regular interface which model extends the model interface. The boolean method is used in preconditions. No problem. I have a regular class which model implements the same model interface. The boolean method is used in preconditions and type invariants. This is not ok: jml says "Undefined Variable" for each instance. I copy the boolean method spec from the model interface into the regular class (effectively duplicating the method definition). All is wel. Conclusion: there seems to be a problem in the jml tool with regular classes model implementing a model interface. From leavens@cs.iastate.edu Tue Feb 26 23:32:56 2002 Date: Tue, 26 Feb 2002 23:12:43 -0600 (CST) From: Gary T. Leavens To: Jan Dockx Cc: JML Interest List Subject: Re: JML-Interest: jml tool problem Hi Jan, Yes, I think this is a bug in the JML type checker. I believe it's the same as one we know about (quoting from the BUGS.txt file): "Methods inherited from an interface, and not present in an abstract class, but used in the abstract class in other methods, prompt complaints from JML, incorrectly. (See $jml/models/InfiniteIntegerClass.java, and take out the three methods compareTo, signum, negate to see the problem.)" If that isn't the same thing, can you please send me the files that trigger the bug? On Tue, 26 Feb 2002, Jan Dockx wrote: > Is this a bug in jml? > > I have a model interface in a .jml file which defines 1 boolean method. > I have a regular interface which model extends the model interface. > The boolean method is used in preconditions. No problem. > > I have a regular class which model implements the same model > interface. The boolean method is used in preconditions and type > invariants. This is not ok: jml says "Undefined Variable" for each > instance. > > I copy the boolean method spec from the model interface into the > regular class (effectively duplicating the method definition). All is > wel. > > > Conclusion: there seems to be a problem in the jml tool with regular > classes model implementing a model interface. -- 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 Jan.Dockx@cs.kuleuven.ac.be Tue Feb 26 23:33:14 2002 Date: Tue, 26 Feb 2002 12:42:34 +0100 From: Jan Dockx To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: jml tool problem For inner classes defined in methods, we often have to declare arguments of the method final. jml --assertc throws away the final declaration of arguments. As a result jassertc gives compile errors. Correct, or am I missing something? From leavens@cs.iastate.edu Wed Feb 27 17:09:39 2002 Date: Wed, 27 Feb 2002 15:20:40 -0600 (CST) From: Gary T. Leavens To: Jan Dockx Cc: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: model variable does not seem to have a representes clause Jan, On Wed, 27 Feb 2002, Jan Dockx wrote: > What does Model variable MAX_SIZE used in Class: > edu.iastate.cs.jml.samples.stacks.BoundedStack does not seem to have > represents clause. This part of specification will be ignored > mean? > > I get it on my code, but also on .../edu/iastate/cs/jml/samples/stacks/ > jml --assertc --warn --all .. It's a warning that the runtime assertion checker won't check assertions using the given model variable at run-time. But there is a represents clause in the file //@ private represents MAX_SIZE <- MAX_STACK_ITEMS; so this is a bug. Sorry about that. We'll put it in the list -- 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 Jan.Dockx@cs.kuleuven.ac.be Wed Feb 27 17:12:19 2002 Date: Thu, 28 Feb 2002 00:06:13 +0100 From: Jan Dockx To: jml-interest-list@cs.iastate.edu Cc: leavens@cs.iastate.edu Subject: Re: JML-Interest: jml tool problem Probably, but then you can remove the "abstract" from the description, because my inheriting class is regular. If you want to see, please go to . The file in question is EventSourceSupport.java. This file works. See comments at the top of the class body for what to remove to make the problem obvious. >Hi Jan, > >Yes, I think this is a bug in the JML type checker. I believe it's >the same as one we know about (quoting from the BUGS.txt file): > >"Methods inherited from an interface, and not present in an abstract >class, but used in the abstract class in other methods, prompt >complaints from JML, incorrectly. (See >$jml/models/InfiniteIntegerClass.java, and take out the three methods >compareTo, signum, negate to see the problem.)" > >If that isn't the same thing, can you please send me >the files that trigger the bug? > >On Tue, 26 Feb 2002, Jan Dockx wrote: > >> Is this a bug in jml? >> >> I have a model interface in a .jml file which defines 1 boolean method. >> I have a regular interface which model extends the model interface. >> The boolean method is used in preconditions. No problem. >> >> I have a regular class which model implements the same model >> interface. The boolean method is used in preconditions and type >> invariants. This is not ok: jml says "Undefined Variable" for each >> instance. >> >> I copy the boolean method spec from the model interface into the >> regular class (effectively duplicating the method definition). All is >> wel. >> >> >> Conclusion: there seems to be a problem in the jml tool with regular >> classes model implementing a model interface. > >-- > 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 kristof.mertens@cs.kuleuven.ac.be Fri Mar 1 10:33:00 2002 Date: Fri, 01 Mar 2002 10:38:18 +0100 From: Kristof Mertens To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: preliminary design : 2.2.1.4 In the preliminary design of JML in chapter 2.2.1.4 we read: The specification of the last method of BoundedThing, clone, is interesting. Note that it begins with the keyword also. This form is intended to tell the reader that the specification given is in addition to any specification that might have been given in the superclass Object, where clone is declared as a protected method. A form like this must be used whenever a specification is given for a method that overrides a method in a superclass, or that implements a method from an implemented interface. Here is probably faulty assumed that BoundedThing is a class. If it were a class, it would extend from Object and would have the clone() already, but it is an interface so it doesn't inherit the method clone() from Object. The stated situation can nevertheless occur, therefore: What is the exact semantics of overriding a protected method with a public one? Is it as follows: the protected and possibly the package accessible specification is inherited, no public specification is inherited (because the protected method in the supertype cannot have a public specification). To get a public specification in the overriding method, you have to write it completely without using any protected or package accessible specification. Is the also keyword needed if you only write public specification in a overridden method, that overrides a protected method? Kristof From leavens@cs.iastate.edu Sat Mar 2 10:46:52 2002 Date: Fri, 01 Mar 2002 17:45:19 -0600 From: Gary T. Leavens To: Kristof Mertens Cc: JML Interest List Subject: Re: JML-Interest: preliminary design : 2.2.1.4 Hi Kristof, Thanks for your feedback on the preliminary design document. Kristof Mertens wrote: > > In the preliminary design of JML in chapter 2.2.1.4 we read: > > The specification of the last method of BoundedThing, clone, is > interesting. Note that it begins with the keyword also. This form is > intended to tell the reader that the specification given is in > addition to any specification that might have been given in the > superclass Object, where clone is declared as a protected method. A > form like this must be used whenever a specification is given for a > method that overrides a method in a superclass, or that implements a > method from an implemented interface. > > > Here is probably faulty assumed that BoundedThing is a class. If it > were a class, it would extend from Object and would have the clone() > already, but it is an interface so it doesn't inherit the method > clone() from Object. I was under the impression that interfaces "inherit" in some sense the methods of Object. I'll have to check the JLS again on this. > The stated situation can nevertheless occur, therefore: > What is the exact semantics of overriding a protected method with a > public one? Is it as follows: the protected and possibly the package > accessible specification is inherited, no public specification is > inherited (because the protected method in the supertype cannot have a > public specification). To get a public specification in the overriding > method, you have to write it completely without using any protected or > package accessible specification. Also can be used to combine specifications at different levels of visibility. In this case, it's right that there can be no public specification. You can write a public specification case if you promote the visibility of the protected method to public (as you suggest), because then having a public specification makes sense. > Is the also keyword needed if you only write public > specification in a overridden method, that overrides a protected method? Also is needed whenever you override a method, regardless of visibility (or even the existence of a specification in the supertype). > -- 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 Jan.Dockx@cs.kuleuven.ac.be Sat Mar 2 10:48:21 2002 Date: Sat, 2 Mar 2002 10:53:52 +0100 From: Jan Dockx To: Gary T. Leavens Cc: Kristof Mertens , JML Interest List Subject: Re: JML-Interest: preliminary design : 2.2.1.4 At 17:45h -0600 1/3/2002, Gary T. Leavens wrote: >Also is needed whenever you override a method, regardless of >visibility (or even the existence of a specification in the >supertype). Then effectively the keyword is superfluous. When method overriding happens is defined by Java, and whenever a method is overridden, the contract of the super method has to be conjugated (logical AND) with the contract specified in the subtype (Liskov Substitution Principle) in JML. This also means that JML always enforces conjunction of super method contracts with the local contract, as required by LSP. In other words, Java software that violates behavioral subtyping cannot be specified in JML. This conflicts with the design goals of JML that state that the intention is to have a BISL that can specify any valid Java program, regardless of style. There is a lot of working code out there that isn't LSP compliant. It's bad code in my, and probably your, mind, but working code nonetheless. A "workaround" collegues of mine propose is to have the super method have an empty contract. Sadly, this really isn't what that code intents. Most often both methods have a contract in Javadoc English which clients do use. To dot the i's: we long ago decided to only focus on good code. One of our goals (in BISL and a formal OOA method) has always been to rig a spec syntax in such a way that bad code, spec, design, ... is syntactically impossible to write. As much as possible. The spec language then becomes a tool guiding developers in design decissions. We have had relative success with this. Our experience shows it is certainly not impossible. The above is a good example. In our homegrown BISL we simply stated that the local spec of an overridden method is always partial. The complete spec is the conjunction of the local spec with the spec of the super method. If this results in a contradiction, tant pis. It will be impossible to implement the method (and thus the class) correctly. A static or dynamic verification tool would flag any implementation as incorrect easily. Although Java allows to write LSP-violating code, our BISL (and JML as it turns out) doesn't, so programmers using it don't. One might debate the good criteria. Obviously, they are our criteria, and your mileage may differ. Too bad. But actually we have seen that this work gives a kind of meta-feedback. Working on a BISL as described above leads to a better understanding of sensible code quality criteria. In conclusion, my advise: - Lose the design goal of "any Java code" in the preliminary design. Otherwise you have to change JML to allow for LSP-violating code (i.e., make also optional). - Lose the also keyword in the syntax. From leavens@cs.iastate.edu Sat Mar 2 12:03:04 2002 Date: Sat, 2 Mar 2002 11:26:45 -0600 (CST) From: Gary T. Leavens To: Jan Dockx Cc: Kristof Mertens , JML Interest List Subject: Re: JML-Interest: preliminary design : 2.2.1.4 Hi Jan, On Sat, 2 Mar 2002, Jan Dockx wrote: > At 17:45h -0600 1/3/2002, Gary T. Leavens wrote: > >Also is needed whenever you override a method, regardless of > >visibility (or even the existence of a specification in the > >supertype). > > Then effectively the keyword is superfluous. No, you can't use "also" when you aren't overriding a method, and you must use it when you are. So the keyword tells the reader that there may be a specification (and that there is at least an implicit one that is being added to. > When method overriding > happens is defined by Java, and whenever a method is overridden, the > contract of the super method has to be conjugated (logical AND) with > the contract specified in the subtype (Liskov Substitution Principle) > in JML. This idea of forcing behavioral subtyping through specification inheritance is described in my paper with Krishna Kishore Dhara in the International Conference on Software Engineering from 1996. @InProceedings{Dhara-Leavens96, Key = "Dhara \& Leavens", Author = "Krishna Kishore Dhara and Gary T. Leavens", Title = "Forcing Behavioral Subtyping Through Specification Inheritance", BookTitle = "Proceedings of the 18th International Conference on Software Engineering, Berlin, Germany", Publisher = "IEEE Computer Society Press", Pages = "258-267", Year = 1996, Month = Mar, Note = "A corrected version is Iowa State University, Dept. of Computer Science TR \#95-20c.", Annote = "19 references." } You can get a copy from: ftp://ftp.cs.iastate.edu/pub/techreports/TR95-20/TR.ps.gz > This also means that JML always enforces conjunction of > super method contracts with the local contract, as required by LSP. Yes, that is the point. (Although I hope you understand that "conjunction" of contracts is not defined in Liskov's 1987 OOPSLA talk, and is also not described in the later papers by Liskov and Wing on behavioral subtyping. They do not phrase things in terms of specification inheritance. I believe that the idea of specification inheritance in this vein was first published in the above cited paper.) > In other words, Java software that violates behavioral subtyping > cannot be specified in JML. Yes, that is also correct in one sense. As we described in the paper from ICSE 1996, specification inheritance in JML forces behavioral subtyping. However you can specify software that you might think would violate behavioral subtyping. For example, if you have public class B { /*@ public normal_behavior @ ensures \result == 7; @*/ int m() { return 7; } } public class D extends B { /*@ also @ public normal_behavior @ ensures \result == 3; @*/ int m() { return 3; } } This is a perfectly valid, legal JML specification (and so in that sense can be specified). The effective specification of D's method B is: /*@ public normal_behavior @ ensures \result == 7; @ also @ public normal_behavior @ ensures \result == 3; @*/ int m(); or in desugared form it is equivalent to /*@ public normal_behavior @ ensures \result == 7 && \result == 3; @*/ int m(); Of course, this can't be implemented correctly, so in that sense you are right that you can't violate behavioral subtyping in JML. Note that the implementatation given in D above (return 3) is incorrect. So this is what happens in JML when you try to violate behavioral subtyping, you get a specification that is stronger (by specification inheritance) and indeed so strong that it can't be implemented. > This conflicts with the design goals of > JML that state that the intention is to have a BISL that can specify > any valid Java program, regardless of style. That is also correct. I believe, in this case, however, that it's not sensible to be able to specify subtypes that can't be reasoned about using supertype abstraction (a term I prefer to the LSP :-). This design principle is not absolute, and isn't applied when it is not sensible. > A "workaround" collegues of mine propose is to have the super method > have an empty contract. Sadly, this really isn't what that code > intents. Most often both methods have a contract in Javadoc English > which clients do use. Underspecification is the general idea for specification of supertypes to allow behavior of different subtypes to be behavioral subtypes. If the demands of clients for reasoning about the subtype are such that they don't permit the subtypes to obey the supertype's contract, than some of them can't be subtypes of that supertype, and have to be moved out of the hierarchy. > To dot the i's: we long ago decided to only focus on good > code. One of our goals (in BISL and a formal OOA method) has always > been to rig a spec syntax in such a way that bad code, spec, design, > ... is syntactically impossible to write. As much as possible. That is not our goal in JML. > In our homegrown BISL we simply stated > that the local spec of an overridden method is always partial. The > complete spec is the conjunction of the local spec with the spec of > the super method. That's fine, I'm glad to see you've adopted the ideas of our 1996 ICSE paper in your language. :-) > If this results in a contradiction, tant pis. It > will be impossible to implement the method (and thus the class) > correctly. As I pointed out above that is also what we do in specification inheritance in JML. This is also mentioned in our 1996 ICSE paper. > A static or dynamic verification tool would flag any > implementation as incorrect easily. The runtime assertion checker can indeed find these errors (see also the 2001 OOPSLA paper by Findler et al.). However, in general, deciding whether a type is a behavioral subtype is undecideable in the same sense that the halting problem is undecideable. Similarly, deciding whether a specification is implementable is also undecideable. So I'd hardly characterize that as "easy". > Although Java allows to write > LSP-violating code, our BISL (and JML as it turns out) doesn't, so > programmers using it don't. Right. I'm glad your BISL agrees with JML in this respect. > In conclusion, my advise: > - Lose the design goal of "any Java code" in the preliminary design. > Otherwise you have to change JML to allow for LSP-violating code > (i.e., make also optional). > - Lose the also keyword in the syntax. I don't agree with either of these. You can certainly have goals that aren't achieved absolutely, and I think for a language design that will always be the case. However, maybe we should explicitly note this exception to the goals. I also think that "also" serves a very useful purpose for readers of a specification. Hope that makes sense. Thanks for your comments and the discussion. -- 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 Kristof.Mertens@cs.kuleuven.ac.be Mon Apr 15 13:32:42 2002 Date: Mon, 15 Apr 2002 18:00:13 +0200 From: Kristof Mertens To: jml-interest-list Subject: JML-Interest: assignable & fields_of() Hi, I have some questions about which fields exactly are assignable and fields_of(). Q1: For example in the example included with jml: ./edu/iastate/cs/jml/samples/stacks/UnboundedStackAsVector.java (version 1.19, 2001/05/03) the assignable clause of push does mention "theStack" and "theStack" depends on "elems" which is a vector. The assignable clause of push looks is: assignable theStack; Is it (1) now allowed to add or remove elements to "elems" in the method push (as is done)? or (2) is the depends clause fault and must it be "depends theStack <- fields_of(elems)"? or (3) must the depends clause be: "depends theStack <- elems.theVector"? or (4) something else? (the specification for Vector can be found in ./JDK/java/util/Vector.spec ./JDK/java/util/Vector.spec-refined ) Q2: Which fields are exactly named by the fields_of() construct? Are it all the instance fields - independent of there accessibility? - no matter if they are model are not? Q3: If the answer to my first question is (2): I make a class "MyVector" which uses a field of type "Vector" for its implementation. I also make a class "C" which has a field "myVector" of type "MyVector". In the the class "C" I want a method "m" that has to be able add and remove elements to myVector. What do I have to write as assignable clause (1) assignable myVector? (2) assignable fields_of(myVector)? (3) assignable fields_of(myVector), fields_of(fields_of(myVector))? If it answer (3), I have an extra question: If I change the implementation of MyVector so that it has an extra indirection then the assignable clause becomes: assignable fields_of(myVector), fields_of(fields_of(myVector)), fields_of(fields_of(fields_of(myVector))); Here is a problem, because the specification of some class does depend on the implementation of another class. I hope you understand the question(s). Kristof From leavens@cs.iastate.edu Mon Apr 15 14:29:45 2002 Date: Mon, 15 Apr 2002 14:21:17 -0500 (CDT) From: Gary T. Leavens To: Kristof Mertens Cc: jml-interest-list Subject: Re: JML-Interest: assignable & fields_of() Hi Kristof, Thanks for your questions. On Mon, 15 Apr 2002, Kristof Mertens wrote: > I have some questions about which fields exactly are assignable and > fields_of(). > > Q1: For example in the example included with jml: > ./edu/iastate/cs/jml/samples/stacks/UnboundedStackAsVector.java (version > 1.19, 2001/05/03) > the assignable clause of push does mention "theStack" and "theStack" > depends on "elems" which is a vector. > > The assignable clause of push looks is: assignable theStack; > Is it (1) now allowed to add or remove elements to "elems" in the method > push (as is done)? > or (2) is the depends clause fault and must it be "depends theStack <- > fields_of(elems)"? > or (3) must the depends clause be: "depends theStack <- elems.theVector"? > or (4) something else? > > (the specification for Vector can be found in > ./JDK/java/util/Vector.spec > ./JDK/java/util/Vector.spec-refined > ) Yes, the specification is definitely broken, and it is the depends clause which is at fault. I think the right fix is to rely recursively on the depends clause of the Vector class, so that "elems" is a "pivot" field. That is the depends clause in UnboundedStackAsVector.java should read: //@ protected depends theStack <- elems, elems.theVector; which corresponds pretty much to your alternative (3). Note that you want to allow both elems and elems.theVector to change when theStack changes, in general. For example, the constructor needs to change elems, although push will change elems.theVector. So the specification of push, for example, in UnboundedStackAsVector.java should read: /*@ also @ protected normal_behavior @ requires !theStack.isEmpty(); @ assignable theStack; @ ensures \not_modified(elems); @*/ public void push(Object x) { elems.insertElementAt(x,0); } Thanks for pointing out these probelms. We'll need to fix this entire specification along these lines... > Q2: Which fields are exactly named by the fields_of() construct? > Are it all the instance fields > - independent of [their] accessibility? > - no matter if they are model are not? Yes, I think, it is all of them, but you raise a good point which we have to consider in more detail. Let me get back to you on this. I welcome comments from others on this issue also... > If it answer (3), I have an extra question: > If I change the implementation of MyVector so that it has an extra > indirection then the assignable clause becomes: > assignable fields_of(myVector), fields_of(fields_of(myVector)), > fields_of(fields_of(fields_of(myVector))); > > Here is a problem, because the specification of some class does depend > on the implementation of another class. The change to the depends clause to make it rely on the model variables of the used class (Vector in this case) is intended precisely to avoid such a dependency. > I hope you understand the question(s). Me too! Thanks, -- 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 Apr 15 14:30:07 2002 Date: Mon, 15 Apr 2002 14:29:34 -0500 (CDT) From: Gary T. Leavens To: Kristof Mertens Cc: jml-interest-list Subject: Re: JML-Interest: assignable & fields_of() Hi again, On Mon, 15 Apr 2002, Gary T. Leavens wrote: > So the specification of push, for example, in > UnboundedStackAsVector.java should read: > > /*@ also > @ protected normal_behavior > @ requires !theStack.isEmpty(); > @ assignable theStack; > @ ensures \not_modified(elems); > @*/ > public void push(Object x) > { > elems.insertElementAt(x,0); > } Except that push, of course, doesn't want that requires cluause, which is the one for pop... Sorry about that. -- 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 Kristof.Mertens@cs.kuleuven.ac.be Wed Apr 17 10:54:32 2002 Date: Wed, 17 Apr 2002 15:38:51 +0200 From: Kristof Mertens To: jml-interest-list Subject: JML-Interest: signals clause A small question: Is it allowed to name "exceptions" in signals clauses that do not extend from java.lang.Exception? For example: signals (SomeInterface) someCondition; in which SomeInterface is an interface (an interface cannot extend java.lang.Exception) Kristof From leavens@cs.iastate.edu Wed Apr 17 15:21:02 2002 Date: Wed, 17 Apr 2002 10:54:15 -0500 (CDT) From: Gary T. Leavens To: Kristof Mertens Cc: jml-interest-list Subject: Re: JML-Interest: signals clause Kristof, On Wed, 17 Apr 2002, Kristof Mertens wrote: > A small question: > > Is it allowed to name "exceptions" in signals clauses that do not extend > from java.lang.Exception? > > For example: > signals (SomeInterface) someCondition; > in which SomeInterface is an interface (an interface cannot extend > java.lang.Exception) Java doesn't permit this in catch clauses, and the current JML checkers don't allow it, they require that the formal parameter declared in a signals clause be a subclass of java.lang.Throwable. I guess it may be more convenient to allow an interface that is implemented by several exception types to be named for the type of the formal parameters, which would save writing the same predicate several times. Is this the reason you're asking? The trade-off is that a JML checker can't then catch errors that it would otherwise be able to notice, when one mistypes the name of an exception and gets an interface name there by mistake. 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 Kristof.Mertens@cs.kuleuven.ac.be Wed Apr 17 15:21:34 2002 Date: Wed, 17 Apr 2002 18:08:49 +0200 From: Kristof Mertens To: jml-interest-list Subject: Re: JML-Interest: signals clause Gary T. Leavens wrote: >I guess it may be more convenient to allow an interface that is >implemented by several exception types to be named for the type of the >formal parameters, which would save writing the same predicate several >times. Is this the reason you're asking? > Not really. I am reasoning about signals clauses and I can make some simplifications if I can exclude the presence of interfaces in signals clauses. From leavens@cs.iastate.edu Wed Apr 17 15:25:46 2002 Date: Wed, 17 Apr 2002 15:23:59 -0500 (CDT) From: Gary T. Leavens To: Kristof Mertens Cc: jml-interest-list Subject: Re: JML-Interest: signals clause Kristof, On Wed, 17 Apr 2002, Kristof Mertens wrote: > Gary T. Leavens wrote: > > >I guess it may be more convenient to allow an interface that is > >implemented by several exception types to be named for the type of the > >formal parameters, which would save writing the same predicate several > >times. Is this the reason you're asking? > > > Not really. > I am reasoning about signals clauses and I can make some simplifications > if I can exclude the presence of interfaces in signals clauses. Ok, that is fine. Since JML's current restrictions on formals in signals clauses correspond to Java's restrictions in catch clauses, I don't think we'll be making any changes to this. -- 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 Thu Apr 18 14:01:47 2002 Date: Thu, 18 Apr 2002 12:15:33 -0500 (CDT) From: Gary T. Leavens To: JML Interest List Subject: JML-Interest: spec_public and spec_protected for methods and types in JML Hi, Yoonsik Cheon has noticed an ambiguity with the use of spec_public and spec_protected for methods and types. The use of these for field declarations is not a problem, but consider the following example of a spec_public method: public class GradesDatabase { private /*@ spec_public pure @*/ float ithGrade(int i) { ... } public /*@ pure @*/ int size() { ... } // ... } public class BetterGradesDatabase extends GradesDatabase { /*@ requires size != 0; @ ensures approxEqual( @ \result, @ (\sum int i; 0 <= i && i < size(); ithGrade(i)) / size()); public float average() { ... } private float ithGrade(int i) { ... } // ... } The problem is the use of ithGrade in the postcondition of average in the subclass. Java's scope rules would make ithGrade refer to the method declared in the subclass BetterGradesDatabase; however, there is an ambiguity: the spec_public declaration of ithGrade in GradesDatabase is also visible according to JML's rules. It's not going to be obvious to JML which method was intended in such cases. One can get similar kinds of problems for private types, and for package protected and protected methods and types. The simpliest fix for this ambiguity seems to be to not allow the use of spec_public and spec_protected for methods and types. It turns out that it is always possible to get the effect of spec_public (and spec_protected) for methods without having that feature. The trick, also due to Yoonsik Cheon, is to use a public (or protected) model method that calls the privacy restricted method. For example, we could get the effect of the above example, without using spec_public, and without the ambiguity by doing the following: public class GradesDatabase { private float ithGrade(int i) { ... } //@ public model pure float modelIthGrade(int i) { return ithGrade(i); } public /*@ pure @*/ int size() { ... } // ... } public class BetterGradesDatabase extends GradesDatabase { /*@ requires size != 0; @ ensures approxEqual( @ \result, @ (\sum int i; 0 <= i && i < size(); modelIthGrade(i)) / size()); public float average() { ... } private float ithGrade(int i) { ... } // ... } (In the case of a method without arguments, one can also use a public (or protected) model with a represents clause that makes it be dependent on the result of the privacy restricted method. But the above encoding is simplier.) Our question for you all is, will taking away the ability to declare spec_public and spec_protected methods and types cause anyone big problems? Is anyone using spec_public and spec_protected for methods and types? How painful would it be to respecify using the above tricks? -- 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@larch.cs.iastate.edu Wed Jun 5 17:51:44 2002 Date: Wed, 5 Jun 2002 17:51:06 -0500 (CDT) From: Gary T. Leavens To: JML Interest List Cc: Murali Sitaraman , Stephen Edwards Subject: JML 3.0 release Hi, I've just made another release of JML, 3.0, which is available from the JML ftp site: ftp://ftp.cs.iastate.edu/pub/leavens/JML/ in the file JML.3.0.tgz. Note that, unlike past releases, this is a gzipped tar file, not a zip file. You can also get it from the JML web page (http://www.jmlspecs.org/). By the way, there never was an official 2.9 release, but I've moved the old JML.zip file that has been in the ftp directory to JML.2.9.zip in case you want that. A warning: if you use the "refine" clause in JML, this release is not for you; instead you should wait for the 3.1 release, which we may make before the month is out, but will be soon anyway. Also, if you need JDK 1.2 or earlier support, this release is also not for you; you will need to stay with the 2.8 or 2.9 release until you go to JDK 1.3 at least. However, in most other respects, this release is much better than the old version of JML. Some highlights of the changes are summarized below. See the NEWS.txt file in the release for other changes, including changes inherited from JML 2.8 (more or less) and several bug fixes. New with release 3.0 (June 5, 2002) major improvements: - A complete reimplementation of the tools, including the checker, runtime assertion checker compiler, and jmldoc, based on the MultiJava compiler. This solves many previous problems, especially the problems with type checking of nested/inner classes. Thanks to Curtis Clifton for the MultiJava infrastructure. - New jmlunit and jtest scripts provide for integration of the runtime assertion checker with JUnit. - The runtime assertion checker can handle model and ghost variables, even in interfaces. Thanks to Yoonsik Cheon for his work on the runtime assertion checker. - The runtime assertion checker now generates bytecode directly and there is now JMLOUTDIR used by the tools. - The checker and tools now can use type checking information from Java .class files and from jar files, as in the JDK, so it is no longer necessary to have unzipped the JDK's sources to run the JML tools. minor improvements: - Many minor bugs have been fixed in the tools. - Redesigned options processing for the scripts. - The order of clauses in most parts of a method specification is no longer dictated by the syntax, although there is still a distinction between the spec-var-decls ("forall" and "old" clauses) spec-header ("requires" clauses) and the body (other clauses). - A store-ref-expression can be used on the left hand side of a "depends" or "represents" clause. - The JML tools now (by default) understand MultiJava source code constructs (although integration is largely untested). incompatible changes: - The "refines" clause does not work in the tools currently, although we hope to have that working in the next release. Similarly, not all suffixes related to refinement work. - The models are now found in the org.jmlspecs.models package. There is a perl script in bin/updatemodelspackage that may be useful to you in changing your specifications to use this package. - The conjoinable specification syntax ("and") has been deleted, because it was too non-modular. - The syntax of a spec-header no longer contains the "when" clause and the "measured" clause, since these are not just about the pre-state. Thus these clauses must be repeated in different specification cases. - The "model" keyword is no longer used for "old" declarations (formerly "let" declarations). - Previously deprecated forms (esp. "let") have been removed. - See also the incompatible changes noted below on the 2.9 release. - This has only been tested with JDK 1.3.1 and 1.4.0. We no longer guarantee compatability with JDK 1.2 or earlier. Please let us know your comments on JML, and if you find bugs. See the TODO.txt file in the release for the ones we know about. See the preliminary design document for other acknowledgments. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From leavens@cs.iastate.edu Thu Jun 6 06:20:42 2002 Date: Thu, 6 Jun 2002 06:16:37 -0500 (CDT) From: Gary T. Leavens To: Peter Chan Cc: JML Interest List Subject: JML-Interest: Re: BUG: jml\bin\jmlc.bat fails Peter, On Thu, 6 Jun 2002, Peter Chan wrote: > We have installed the JML release in Windows 98 under the directory C:\jml > > If we execute the jmlc.bat program by the following command, we got an > exception. > > C:\jml\bin>jmlc.bat --version > Exception in thread "main" java.lang.NoClassDefFoundError: > org/jmlspecs/jmlrac/M > ain > > If we changes the 13th line of jmlc.bat by fixing the sub-directory of > jml-release.jar file, > > CLASSPATH=.;%JMLDIR%\bin\mjc-for-jml.jar;%JMLDIR%\jml-release.jar;%JMLDIR%\specs;%CLASSPATH% > > changed to... > > CLASSPATH=.;%JMLDIR%\bin\mjc-for-jml.jar;%JMLDIR%\bin\jml-release.jar;%JMLDIR%\specs;%CLASSPATH% > > the jmlc.bat program complete successfully. > > C:\jml\bin>jmlc.bat --version > Version: 3.0 Thanks for pointing that out, I appreciate it. It will be fixed in the next release. Note that the same problem applies also to the scripts jmlc.bat, jmldoc.bat, and jmlunit.bat. Sorry for the trouble. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From Marko.vanDooren@cs.kuleuven.ac.be Fri Jun 21 14:12:03 2002 Date: Thu, 20 Jun 2002 14:28:30 +0200 From: Marko van Dooren To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: desugaring of \forall and \exists We (Jan Dockx and I) presume that (\forall Object o; p(o); r(o)) is equivalent to: (\forall Object o; ; p(o) => r(o)) and that (\exists Object o; p(o); r(o)) is equivalent to: (\exists Object o; ; p(o) && r(o)) Is this correct ? Marko van Dooren Jan Dockx -- Jutil.org - Programming as you know it is over http://org-jutil.sourceforge.net From erikpoll@cs.kun.nl Fri Jun 21 14:12:28 2002 Date: Thu, 20 Jun 2002 15:01:56 +0200 (CEST) From: Erik Poll To: Marko van Dooren Cc: JML Interest List Subject: Re: JML-Interest: desugaring of \forall and \exists On Thu, 20 Jun 2002, Marko van Dooren wrote: > We (Jan Dockx and I) presume that > > (\forall Object o; p(o); r(o)) > > is equivalent to: > > (\forall Object o; ; p(o) => r(o)) > > and that > > (\exists Object o; p(o); r(o)) > > is equivalent to: > > (\exists Object o; ; p(o) && r(o)) > > Is this correct ? Yes, it is. (I have noticed that the runtime assertion generator jmlc seems to prefer the (\forall Object o; ... ; ... ) notation. Maybe someone from Iowa can confirm this ?) Erik From hubbers@cs.kun.nl Fri Jun 21 14:27:12 2002 Date: Tue, 18 Jun 2002 17:03:19 +0200 (MET DST) From: Engelbert Hubbers To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: JML assertion exceptions being caught? Hi all, While doing some tests with the runtime assertion checker of JML-3.0 we ran into a problem with the exceptions. Problem was that we had an //@ assert false; somewhere in our code that didn't show up in the runtime check. The reason for this was probably that this assertion was inside a try { ... } catch (Exception) { ... } It seems quite logical that if a JMLAssertionException is thrown because of this assert statement, it is caught afterwards. Our idea about the generated java-code with the runtime assertions is that this assertion-checking should not be bothered by the original code that is to be checked. Hence it should not be able to catch JMLAssertionExceptions by the original code. Unfortunately I do not see a good solution for this. Therefore my questions: 1. Has anyone realized this problem before? 2. Does anyone has ideas for a(n elegant) way to tackle this problem? Engelbert Hubbers From leavens@cs.iastate.edu Fri Jun 21 14:27:55 2002 Date: Fri, 21 Jun 2002 14:15:39 -0500 (CDT) From: Gary T. Leavens To: Erik Poll Cc: Marko van Dooren , JML Interest List Subject: Re: JML-Interest: desugaring of \forall and \exists Hi Erik, Marko, Jan, et al., On Thu, 20 Jun 2002, Erik Poll wrote: > On Thu, 20 Jun 2002, Marko van Dooren wrote: > > > We (Jan Dockx and I) presume that > > > > (\forall Object o; p(o); r(o)) > > > > is equivalent to: > > > > (\forall Object o; ; p(o) => r(o)) > > > > and that > > > > (\exists Object o; p(o); r(o)) > > > > is equivalent to: > > > > (\exists Object o; ; p(o) && r(o)) > > > > Is this correct ? > > Yes, it is. (Technically, in JML, the implications are supposed to be written like "==>" and not "=>", but otherwise this is correct.) > (I have noticed that the runtime assertion generator jmlc seems to prefer > the (\forall Object o; ... ; ... ) notation. > Maybe someone from Iowa can confirm this ?) Yes, that is right. At the moment the runtime assertion checker generates assertion checks when the range predicate, p(o) in (\forall Object o; p(o); r(o)) satisfies certain criteria, and does not generate such checking code when the technically equivalent (\forall Object o;; p(o)==> r(o)) is used instead. Eventually this may be fixed... -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From leavens@cs.iastate.edu Fri Jun 21 14:28:06 2002 Date: Fri, 21 Jun 2002 14:26:57 -0500 (CDT) From: Gary T. Leavens To: Engelbert Hubbers Cc: JML Interest List , Yoonsik Cheon Subject: Re: JML-Interest: JML assertion exceptions being caught? On Tue, 18 Jun 2002, Engelbert Hubbers wrote: > While doing some tests with the runtime assertion checker of JML-3.0 we ran > into a problem with the exceptions. > > Problem was that we had an > //@ assert false; > somewhere in our code that didn't show up in the runtime check. > The reason for this was probably that this assertion was inside a > try { ... } catch (Exception) { ... } > It seems quite logical that if a JMLAssertionException is thrown because > of this assert statement, it is caught afterwards. Ah yes, that would happen certainly. > Our idea about the generated java-code with the runtime assertions is that > this assertion-checking should not be bothered by the original code that > is to be checked. Hence it should not be able to catch JMLAssertionExceptions > by the original code. Yes, I agree with that. > Unfortunately I do not see a good solution for this. > Therefore my questions: > 1. Has anyone realized this problem before? I don't think we thought of it before. > 2. Does anyone has ideas for a(n elegant) way to tackle this problem? The only thing I can think of is to have jmlc rewrite the program so that try { ... //@ assert false; ... } catch (Exception e) { ... } is turned into try { ... throw new JMLAssertionException(...); // or whatever ... } catch (JMLAssertionException e) { throw e; } // rethrow it catch (Exception e) { ... } We'd have to apply this rewriting everywhere that a user program caught an exception that is a supertype of JMLAssertionException. We could perhaps minimize the number of such rewrites if we could declare JMLAssertionException higher in the Java type hierarchy, but I think it's as high as it can go now. So at the moment we would have to do this for places where the user program catches Throwable, Exception, or RunTimeException. We would have to give an error message if the user explicitly tried to catch a JMLAssertionException or its subclasses. Comments? -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From leavens@cs.iastate.edu Fri Jun 21 14:28:53 2002 Date: Fri, 21 Jun 2002 14:26:57 -0500 (CDT) From: Gary T. Leavens To: Engelbert Hubbers Cc: JML Interest List , Yoonsik Cheon Subject: Re: JML-Interest: JML assertion exceptions being caught? On Tue, 18 Jun 2002, Engelbert Hubbers wrote: > While doing some tests with the runtime assertion checker of JML-3.0 we ran > into a problem with the exceptions. > > Problem was that we had an > //@ assert false; > somewhere in our code that didn't show up in the runtime check. > The reason for this was probably that this assertion was inside a > try { ... } catch (Exception) { ... } > It seems quite logical that if a JMLAssertionException is thrown because > of this assert statement, it is caught afterwards. Ah yes, that would happen certainly. > Our idea about the generated java-code with the runtime assertions is that > this assertion-checking should not be bothered by the original code that > is to be checked. Hence it should not be able to catch JMLAssertionExceptions > by the original code. Yes, I agree with that. > Unfortunately I do not see a good solution for this. > Therefore my questions: > 1. Has anyone realized this problem before? I don't think we thought of it before. > 2. Does anyone has ideas for a(n elegant) way to tackle this problem? The only thing I can think of is to have jmlc rewrite the program so that try { ... //@ assert false; ... } catch (Exception e) { ... } is turned into try { ... throw new JMLAssertionException(...); // or whatever ... } catch (JMLAssertionException e) { throw e; } // rethrow it catch (Exception e) { ... } We'd have to apply this rewriting everywhere that a user program caught an exception that is a supertype of JMLAssertionException. We could perhaps minimize the number of such rewrites if we could declare JMLAssertionException higher in the Java type hierarchy, but I think it's as high as it can go now. So at the moment we would have to do this for places where the user program catches Throwable, Exception, or RunTimeException. We would have to give an error message if the user explicitly tried to catch a JMLAssertionException or its subclasses. Comments? -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From jwnimmer@alum.mit.edu Sat Jun 22 12:30:47 2002 Date: Fri, 21 Jun 2002 21:36:21 -0400 From: Jeremy Nimmer Reply-To: jwnimmer@mit.edu To: 'Gary T. Leavens' , 'Engelbert Hubbers' Cc: 'JML Interest List' , 'Yoonsik Cheon' Subject: RE: JML-Interest: JML assertion exceptions being caught? I am not yet familiar with the runtime assertion checker so I may be speaking out of ignorance, but ... >> Our idea about the generated java-code with the runtime assertions >> is that this assertion-checking should not be bothered by the >> original code that is to be checked. Hence it should not be able to >> catch JMLAssertionExceptions by the original code. > > Yes, I agree with that. I do not know the philosophy behind the assertion checker, but in general, programmers who catch all exceptions (via Throwable, Exception, RuntimeException, or Error) are responsible for knowing what they are doing. Some programmers may employ such a catch clause in the outer parts of an application to gracefully shut down from unforeseen internal errors. Others may use a too-wide catch clause out of laziness, but this is a bug in their program, not a JML tool defect. Multi-threaded programs are an interesting case. If one thread crashes from an uncaught exception, the program will not terminate when there are other non-daemon threads still running. Many programmers handle this by placing a "catch (Throwable)" around the main loop of the thread, and explicitly terminating the application if an exception percolates to that catch block. For this and other reasons, I (as a programmer) would expect to have some way to catch exceptions from failed assertions. Having presented my philosophy, if others' opinions differ, I offer ideas below that can implement two different "catchability" options. >> 2. Does anyone has ideas for a(n elegant) way to tackle this >> problem? > > The only thing I can think of is to have jmlc rewrite the program so > that ... Working under the assumption that the application should *not* be able to catch assertion failures, it seems like you want the application to print a stack trace and terminate if an assertion fails? In that case, you may replace throwing a JMLAssertionException with printing a stack trace manually (via a method on Throwable), and calling "System.exit". Then, in almost all circumstances, the desired result will be achieved. (The only exception is if the runtime environment or the application changes the security policy for calls to "System.exit".) If you agree that programmers should be able to catch assertion exceptions, you might consider making JMLAssertionException extend the java.lang.Error class instead of RuntimeException. The Java 1.4 assertion facility takes this route already: http://java.sun.com/j2se/1.4/docs/guide/lang/assert.html (*) http://java.sun.com/j2se/1.4/docs/api/java/lang/AssertionError.html When JMLAssertionException extends Error, "catch (Exception e)" will let the JML exception through, but "catch (Throwable e)" will catch it. It seems like a reasonable compromise to me. Thanks, - Jeremy Nimmer (*) The first URL contains some discussion of this issue, specifically item 4 under the #design-faq-error HTML anchor tag. From leavens@cs.iastate.edu Sun Jun 23 08:31:38 2002 Date: Sat, 22 Jun 2002 17:46:59 -0500 (CDT) From: Gary T. Leavens To: jwnimmer@mit.edu Cc: 'Engelbert Hubbers' , 'JML Interest List' , 'Yoonsik Cheon' Subject: RE: JML-Interest: JML assertion exceptions being caught? Hi Jeremy, I think you have brought up some very good points. In thinking about it, I think I like your idea of making the JMLAssertionException class a subclass of java.lang.Error so that programmers can catch such exceptions if necessary, but won't usually catch them accidentally. The argument about multithreaded programs is also persuasive to me. I think this idea of signalling an exception that is a subtype of java.lang.Error also fits in well with JML's semantics for Error exceptions (which release the caller from the contract); that is, if you call a method that has an assertion violation, the error signaled would release you from your obligation under the contract. Hence we could still say that jmlc didn't change whether a contract was satisfied or not. Of course, such a semantics would also be easier for us to implement. In short I like the idea. Thanks. Other comments anyone? On Fri, 21 Jun 2002, Jeremy Nimmer wrote: > I do not know the philosophy behind the assertion checker, but in > general, programmers who catch all exceptions (via Throwable, > Exception, RuntimeException, or Error) are responsible for knowing > what they are doing. Some programmers may employ such a catch clause > in the outer parts of an application to gracefully shut down from > unforeseen internal errors. Others may use a too-wide catch clause > out of laziness, but this is a bug in their program, not a JML tool > defect. > > Multi-threaded programs are an interesting case. If one thread > crashes from an uncaught exception, the program will not terminate > when there are other non-daemon threads still running. Many > programmers handle this by placing a "catch (Throwable)" around the > main loop of the thread, and explicitly terminating the application if > an exception percolates to that catch block. > > For this and other reasons, I (as a programmer) would expect to have > some way to catch exceptions from failed assertions. > > Having presented my philosophy, if others' opinions differ, I offer > ideas below that can implement two different "catchability" options. > > >> 2. Does anyone has ideas for a(n elegant) way to tackle this > >> problem? > > > > The only thing I can think of is to have jmlc rewrite the program so > > that ... > > Working under the assumption that the application should *not* be able > to catch assertion failures, it seems like you want the application to > print a stack trace and terminate if an assertion fails? In that > case, you may replace throwing a JMLAssertionException with printing a > stack trace manually (via a method on Throwable), and calling > "System.exit". Then, in almost all circumstances, the desired result > will be achieved. (The only exception is if the runtime environment > or the application changes the security policy for calls to > "System.exit".) > > If you agree that programmers should be able to catch assertion > exceptions, you might consider making JMLAssertionException extend > the java.lang.Error class instead of RuntimeException. The Java 1.4 > assertion facility takes this route already: > > http://java.sun.com/j2se/1.4/docs/guide/lang/assert.html (*) > http://java.sun.com/j2se/1.4/docs/api/java/lang/AssertionError.html > > When JMLAssertionException extends Error, "catch (Exception e)" will > let the JML exception through, but "catch (Throwable e)" will catch it. > It seems like a reasonable compromise to me. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From leavens@cs.iastate.edu Tue Jun 25 20:46:39 2002 Date: Tue, 25 Jun 2002 18:20:56 -0500 (CDT) From: Gary T. Leavens To: JML Interest List Subject: JML-Interest: In JML, \fresh(null) should be false Hi all, In some examples, we've noticed that it seems more convenient to say something like: ensures \fresh(\result) && ...; than ensures \result != null && \fresh(\result) && ...; However, one might argue that the readability of the latter is better than the former. Still overall, I think in this case the intuitive meaning of \fresh(E) should imply that E is not null. That is, I'd like to specify that \fresh(null) == false. Any objections to that? -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From erikpoll@cs.kun.nl Wed Jun 26 09:05:09 2002 Date: Wed, 26 Jun 2002 11:41:04 +0200 (CEST) From: Erik Poll To: JML Interest List Subject: Re: JML-Interest: In JML, \fresh(null) should be false (Sorry if you get this message twice - our network is acting up) Gary wrote: > Still overall, I think in this case the intuitive > meaning of \fresh(E) should imply that E is not null. > That is, I'd like to specify that \fresh(null) == false. > > Any objections to that? No, seems like a very good idea. It makes sense to protect people against unintentionally forgetting to include "\result != null" in examples like the one you give. (In fact, I did a quick grep on "fresh" in the JML specs I wrote to see if I didn't forget it anywhere :-) If people want, they can always include an explicit (redundant) "\result != null". Erik From leavens@cs.iastate.edu Wed Jun 26 14:29:25 2002 Date: Wed, 26 Jun 2002 14:26:20 -0500 (CDT) From: Gary T. Leavens To: JML Interest List Subject: JML-Interest: The ChAsE tool for checking assignable clauses ESC/Java subset of JML Hi all, Néstor Catano wanted me to forward the following tool annoncement to you. -------------------------------------------------------------- The first version of the ChasE tool for statically checking JML assignable clauses. We have tried ChasE with an earlier JavaCard case study http://www-sop.inria.fr/lemme/verificard/electronic_purse/ and we have found interesting remarks about specifications errors we made at that time and about the set of side-effects free methods of that JavaCard application. The homepage of ChasE is: http://www-sop.inria.fr/lemme/verificard/modifSpec/index.html where you can find the tool, the specifications and a manuscript describing the process of constructing this tool. Néstor -- Néstor CATAÑO INRIA Sophia-Antipolis, France 2004 route des Lucioles B.P. 93, 06902 Cedex tel. (033+)4.92.38.78.59 fax. (033+)4.92.38.50.60 --------------------------------------------------------------- There is also a link from the JML web page. From Marko.vanDooren@cs.kuleuven.ac.be Wed Jul 3 07:35:24 2002 Date: Tue, 2 Jul 2002 16:37:49 +0200 From: Marko van Dooren To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: JML Tool 3.0 experience I've been using the JML tool to generate runtime assertion checking code of Jutil.org. Here are some remarks I made. 1) In org.jutil.java.collection, there is a class Arrays, which is used in the specification of 2 other classes in that same package. However, a static call Arrays.method() does not succeed unless I explicitly import Arrays. 2) When I explicitly set the import in 1 of the classes using Arrays, the other one also validates. This seems very weird to me. 3) The keyword "set" (I had a variable with that name) is reserved, but the tool doesn't say so, it just says there is a syntax error. 4) I use instance variables starting with a $, however JLS recommends against it, and so the JML tools gives errors. Can I turn that off ? It is valid java code, and I don't like underscores. The tool seems a lot better than version 2.7. However, I got the following error (the only error I've seen so far): marko@seven:~/cvs/jutil.org/src/org/jutil/junit$ jmlc-unix -d/home/marko/cvs/jutil.org/jml -classpath ~/cvs/jutil.org/lib/jregex1.2_00.jar:~/cvs/jutil.org/lib/ju nit.jar *.java ../java/regex/Pattern.java parsing AbstractRevision.java parsing CVSRevision.java parsing JutilTest.java parsing Revision.java parsing RevisionError.java parsing ../java/regex/Pattern.java parsing ../../../../../../../../tmp/jmlrac13993.java parsing ../../../../../../../../tmp/jmlrac13994.java parsing ../../../../../../../../tmp/jmlrac13995.java parsing ../../../../../../../../tmp/jmlrac13996.java parsing ../../../../../../../../tmp/jmlrac13997.java parsing ../../../../../../../../tmp/jmlrac13998.java AbstractRevision.java:149:52 error:Variable "JMLChecker.PRECONDITION" is not defined in current context AbstractRevision.java:155:54 error:Variable "JMLChecker.POSTCONDITION" is not defined in current context AbstractRevision.java:162:55 error:Variable "JMLChecker.POSTCONDITION" is not defined in current context AbstractRevision.java:168:33 error:Cannot find type "JMLAssertionException" Exception in thread "main" java.lang.RuntimeException: Cannot resolve a maybe-qualified class name without context information:JMLAssertionException at org.multijava.mjc.CClassNameType.checkType(CClassNameType.java:145) at org.multijava.mjc.CClassNameType.getCClass(CClassNameType.java(Compiled Code)) at org.multijava.mjc.CClassType.isAlwaysAssignableTo(CClassType.java:301) at org.multijava.mjc.JTryCatchStatement.typecheck(JTryCatchStatement.java:151) at org.multijava.mjc.JBlock.typecheck(JBlock.java:77) at org.multijava.mjc.JTryFinallyStatement.typecheck(JTryFinallyStatement.java:130) at org.multijava.mjc.JBlock.typecheck(JBlock.java:77) at org.multijava.mjc.JConstructorBlock.typecheck(JConstructorBlock.java:156) at org.multijava.mjc.JConstructorDeclaration.typecheck(JConstructorDeclaration.java:206) at org.multijava.mjc.JClassDeclaration.typecheck(JClassDeclaration.java:318) at org.multijava.mjc.JCompilationUnit.typecheck(JCompilationUnit.java:696) at org.multijava.mjc.JCompilationUnit.typecheck(JCompilationUnit.java:1089) at org.multijava.mjc.Main$TypecheckTask.processTree(Main.java:1375) at org.multijava.mjc.Main$TreeProcessingTask.execute(Main.java:1181) at org.multijava.mjc.Main$TypecheckTask.execute(Main.java:1364) at org.multijava.mjc.Main.processTaskQueue(Main.java:477) at org.multijava.mjc.Main.run(Main.java:149) at org.jmlspecs.jmlrac.Main.compile(Main.java:67) at org.jmlspecs.jmlrac.Main.main(Main.java:61) It complains about errors in lines 149,... , but AbstractRevision.java only has 96 lines. I have no idea what causes the problem. If anyone who wants the source in order to investigate the problem, it can be obtained as follows (just press enter when prompted for a password). cvs -z3 -d:pserver:anonymous@cvs.org-jutil.sourceforge.net:/cvsroot/org-jutil co jutil.org Btw, I've seen an issue regarding makefiles in TODO.txt of JML2 (which I haven't used). I think the developers of the jml tool would benefit a lot if they would use ant (http://jakarta.apache.org/ant/index.html), it is very easy, and very powerful. Just my 0.02$. greetings, Marko van Dooren -- Jutil.org - Programming as you know it is over http://org-jutil.sourceforge.net From leavens@cs.iastate.edu Sat Jul 13 16:56:21 2002 Date: Sat, 13 Jul 2002 15:00:19 -0500 (CDT) From: Gary T. Leavens To: JML Interest List Subject: JML-Interest: The meaning of \typeof in JML (should be as in ESC/Java) Hi, When we adopted the \typeof predicate from ESC/Java, we documented it incorrectly. In ESC/Java, \typeof(E) gives the most specific *dynamic* type of E, whereas in JML's preliminary design document we say that it is the *static* type of E. The static type seems a lot less useful (you can write it in yourself using \type(T) if you wish), and I've been thinking from various examples that JML needs a way to get at dynamic types of objects. So it seems very clear to me that we should change JML's interpretation of \typeof. I think we should do that unless there are objections, so please let me know if you object. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From Jan.Dockx@cs.kuleuven.ac.be Sat Jul 13 16:58:03 2002 Date: Sat, 13 Jul 2002 23:06:53 +0200 From: Jan Dockx To: Gary T. Leavens Subject: Re: JML-Interest: The meaning of \typeof in JML (should be as in ESC/Java) 1 simple objection: why don't you use E.getClass()? On zaterdag, juli 13, 2002, at 10:00 h, Gary T. Leavens wrote: Hi, When we adopted the \typeof predicate from ESC/Java, we documented it incorrectly. In ESC/Java, \typeof(E) gives the most specific *dynamic* type of E, whereas in JML's preliminary design document we say that it is the *static* type of E. The static type seems a lot less useful (you can write it in yourself using \type(T) if you wish), and I've been thinking from various examples that JML needs a way to get at dynamic types of objects. So it seems very clear to me that we should change JML's interpretation of \typeof. I think we should do that unless there are objections, so please let me know if you object. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 "I've got to ask you," I say. "How long do you envision this rule of the universe to be?" "I'm guessing it's really very short." "Like how long?" "I don't know. In Mathematica, for example, perhaps three, four lines of code." "Four lines of code?" "[...] it will be short if Mathematica was a well-designed language. It will be longer if it doesn't happen to be as well-designed, in the sense that that doesn't happen to be the way the universe works. But we're not looking at 25,000 lines of code or something. We're looking at a handful of lines of code." "So it's not like Windows?" Stephen Wolfram, in an interview with Steven Levy; The Man Who Cracked The Code to Everything ...; Wired; June 2002; http://www.wired.com/wired/archive/10.06/wolfram.html From Bart.Jacobs@cs.kun.nl Wed Jul 17 10:49:50 2002 Date: Wed, 17 Jul 2002 16:08:16 +0200 From: Bart Jacobs To: jml-interest-list@cs.iastate.edu Cc: Bart.Jacobs@cs.kun.nl Subject: JML-Interest: paper announcement Dear Colleague, You might be interested to have a look at my recent paper: Title ===== Weakest Precondition Reasoning for Java Programs with JML Annotations Abstract ======== This paper distinguishes several different approaches to organising a Weakest Precondition (WP) calculus in a theorem prover. The implementation of two of these approaches for Java within the LOOP project is described. This involves the WP-infrastructures in the higher order logic of the theorem prover PVS, together with some associated rules and strategies for automatically proving JML specifications for Java implementations. The soundness of all WP-rules has been proven on the basis of the underlying Java semantics. These WP-calculi are integrated with the existing Hoare logic, and together form a verification toolkit in PVS: typically one uses Hoare logic rules to break a large verification task up into smaller parts that can be handled automatically by one of the WP-strategies. URL === http://www.cs.kun.nl/~bart/PAPERS/jmlwp.ps.Z Your comments are appreciated. Have a nice summer! Bart Jacobs. From erikpoll@cs.kun.nl Thu Jul 18 08:39:43 2002 Date: Thu, 18 Jul 2002 09:58:04 +0200 (CEST) From: Erik Poll To: JML Interest List Subject: JML-Interest: Visibility (public, private,...) of invariants ? Hi all, I started discussing the issue below with Gary, but maybe other people have some thoughts on this ? Any comments are welcome ! In JML invariants can be declared with public, package, protected, or private visibility. As in Java, the default is package. The visibility of an invariant restricts the members (ie. fields and methods) that it can mention, as you'd expect: - public invariants can only refer to public (or spec_public) members - package invariants can also use package members - protected invariants can also use protected members - private invariants can refer to all members All this is expressed in the table below, which indicates if a member may be used in an invariant or not, given their visibilities : | public package protected private invariant ----------------------------------------------------------------- public | yes yes yes yes package | no yes yes yes protected | no no yes yes private | no no no yes member The restrictions in the table above make sense from the point of "visibility": public clients can see the public invariants, so these shouldn't mention private fields or methods. However, the question is if these restrictions are correct from the point of view of "enforceability", as discussed in the remainder of this email. The restrictions above suggest that the invariant in the example below, which mentions both a private and a public field, should be private: public int maxSize; private int size; //@ private invariant size < MaxSize; This respects the rules in the table above, but this is a strange invariant: anyone can change the value of the public field maxSize, and unwitttingly invalidate this invariant, as the invariant is private, and therefore outside of the class no one knows this invariant exist Unless there are other public JML specs preventing public clients from arbitrarily changing (decreasing) maxSize, eg //@ public invariant maxSize == 12; the JML spec above (and/or the associated Java code) is seriously flawed, as the private invariant is clearly not enforceable. One way to improve this would be to make the invariant public, and (hence) make the field size spec_public: public int maxSize; private /*@ spec_public @*/ int size; //@ public invariant size < MaxSize; The invariant is still not enforceable, but at least everyone can see the invariant, and try not to invalidate it. Of course, a better solution would be to realize that you shouldn't make maxSize public in the first place, and change the Java code ... Note that if the field maxSize is package-visible, which is clearly better than public, we do still face essentially the same question: Should the invariant "size < MaxSize" be private, because size is, or should it be package-visible, because MaxSize is ? All this suggests another (additional?) set of restrictions, namely that an invariant should be AT LEAST AS visible as any (non-final non-model) field it uses: | public package protected private invariant ----------------------------------------------------------------- public | yes no no no package | yes yes no no protected | yes yes yes no private | yes yes yes yes non-final non-model fields The justification for this is that if an invariant depends on a certain field, then anyone that has access to this field should know about the invariant, since they could disturb the invariant by modifying the field. (Final fields do not pose a problem, as these cannot be changed. Neither do model fields, as these can only be modified by calling methods of the class to which they belong.) Note that this second table is almost the exact opposite of the first one! Combining the constraints imposed by both tables just leaves the diagonal: an invariant with visibility X can only mention (non-final non-model) fields of visibility X. It's not clear to me if this rule would be unreasonably restrictive and clumsy, or if well-designed code does/should meet these restrictions anyway. Sticking to this rule might mean that you need a lot of spec_public declarations: as soon as an invariant mentions two fields with different visibility the least visible field would have to be made spec_public. Indeed, it might be worthwhile to introduce spec_protected and spec_package as well as spec_public ? An alternative would be to only impose the restrictions given by the first table, and produce warnings for any violations of the second table. After all, such violations suggest that something is wrong, as is clearly the case in the "size < MaxSize" example above. Eg I'd be suspicious of any private invariant mentioning a public or package-accessible field. If anyone has some thoughts on this, or some experience with examples that really use the public, private, protected modifiers for invariants, I'd be interested to know what they think. Cheers, Erik From Marko.vanDooren@cs.kuleuven.ac.be Thu Jul 18 08:40:44 2002 Date: Thu, 18 Jul 2002 10:41:07 +0200 From: Marko van Dooren To: JML Interest List Subject: Re: JML-Interest: Visibility (public, private,...) of invariants ? > The restrictions above suggest that the invariant in the example below, > which mentions both a private and a public field, should be private: > > public int maxSize; > private int size; > //@ private invariant size < MaxSize; > > This respects the rules in the table above, but this is a strange > invariant: anyone can change the value of the public field maxSize, and > unwitttingly invalidate this invariant, as the invariant is private, and > therefore outside of the class no one knows this invariant exist > Unless there are other public JML specs preventing public clients > from arbitrarily changing (decreasing) maxSize, eg > //@ public invariant maxSize == 12; > the JML spec above (and/or the associated Java code) is seriously flawed, > as the private invariant is clearly not enforceable. If it is not enforceable, it simply isn't an invariant, but an assumption (and a dangerous one). This is the reason why I (and our group) only use private fields, and also the reason why assignment to any field from another object simply is not possible in Eiffel (in Eiffel the fields are more or less protected fields). > One way to improve this would be to make the invariant public, > and (hence) make the field size spec_public: > > public int maxSize; > private /*@ spec_public @*/ int size; > //@ public invariant size < MaxSize; > > The invariant is still not enforceable, but at least everyone can > see the invariant, and try not to invalidate it. That still doesn't make it an invariant. You should never be able to break a public invariant when satisfying all preconditions, which are non-existent for assignment (except for type-checking of course). > Of course, a better solution would be to realize that you shouldn't make > maxSize public in the first place, and change the Java code ... I couldn't agree more. I personally don't see a reason to modify JML are anything else in order to specify such code. I think it is too easy to violate the invariant that way. You could of course do the same when violating the preconditions of a method, but I find that a more severe error. just my 0.02$ Marko -- Jutil.org - Programming as you know it is over http://org-jutil.sourceforge.net From Claude.Marche@lri.fr Thu Jul 18 08:41:02 2002 Date: Thu, 18 Jul 2002 12:39:53 +0200 From: Claude Marche To: Erik Poll Cc: JML Interest List Subject: Re: JML-Interest: Visibility (public, private,...) of invariants ? Hi all, Since it's the first time I write to this list, may be I should introduce myself briefly: I'm working in the Logical group at INRIA, a partner of the Verificard project. We are interested in proving validity of JML assertions of Java(card) programs, mainly "ensures" and "invariant" kinds, using the Coq proof assistant as a back-end. Erik's message is of particular interest for us, because we wonder what is *logical* meaning of visibility modifiers. The last sentence of this part of Erik's message is particularily surprising to me : >>>>> "Erik" == Erik Poll writes: Erik> The restrictions above suggest that the invariant in the example below, Erik> which mentions both a private and a public field, should be private: Erik> public int maxSize; Erik> private int size; Erik> //@ private invariant size < MaxSize; Erik> This respects the rules in the table above, but this is a strange invariant: Erik> anyone can change the value of the public field maxSize, and unwitttingly Erik> invalidate this invariant, as the invariant is private, and therefore Erik> outside of the class no one knows this invariant exist Does it mean that a private invariant should not be preserved by methods which do not see it? I find this semantics very strange! For the moment, we considered that visibility modifier of an invariant (or post-condition, etc.) is only the "best common visibility" of the variables it mentions (as shown by the first table in Erik's message). But we think it does not have any *logical* implications. On the example above, that would mean that the private invariant should be shown preserved by any external modification of maxSize, a very heavy task, that should be done again for each use of that class. To prove preservation of such an invariant once for all, one should better ensures that maxSize cannot be modified outside that class, so either make it private, or final. This is my point of view on that problem, I'd be very interested to know of others. - Claude -- | Claude Marché | mailto:Claude.Marche@lri.fr | | LRI - Bât. 490 | http://www.lri.fr/~marche/ | | Université de Paris-Sud | phoneto: +33 1 69 15 64 85 | | F-91405 ORSAY Cedex | faxto: +33 1 69 15 65 86 | From erikpoll@cs.kun.nl Thu Jul 18 08:42:11 2002 Date: Thu, 18 Jul 2002 15:06:26 +0200 (CEST) From: Erik Poll To: Claude Marche Cc: JML Interest List Subject: Re: JML-Interest: Visibility (public, private,...) of invariants ? Hi Claude, Thanks for your comments. I thought about it a bit more and I think understand the whole issue a lot clearer now. > Erik's message is of particular interest for us, because we wonder > what is *logical* meaning of visibility modifiers. This is the question that I was trying to raise, but you formulate it clearer than I did. The question is are these visibility modifiers just a matter of syntax/scoping/typing, or do/should they have a logical meaning ? I think there are two ways to view the meaning of the visibility modifiers for invariants, the "syntactical" view and "logical" view, as explained below. > For the moment, we considered that visibility modifier of an invariant > (or post-condition, etc.) is only the "best common visibility" of the > variables it mentions (as shown by the first table in Erik's > message). But we think it does not have any *logical* implications. I think that your view is essentially correct. This is what the current meaning of the visibility modifiers for invariants is in JML. I'll call this the "syntactical" view. However, at least on an intuitive level, there seems to be a natural logical meaning of the visibility modifiers: If an invariant is private, I'd expect that the object itself takes care of maintaining the invariant, that this invariant only concerns the private representation of object, and that clients of the object don't want to AND don't have to know about this invariant, because - they are not able to observe whether the invariant holds or not - they are not able to break the invariant, because they don't have access to the private representation I'll call this the "logical" view of the meaning of "private" for an invariant. Note that the jmldoc tool - at least implicitly - seem to take this "logical" view: private invariants are not mentioned in the jmldoc output (just like private fields are not mention in javadoc output). So jmldoc takes the view that clients don't have to know about private invariants; the only justification for this is that clients can't see or break these invariants. The "logical view" is the motivation behind the second table I gave. Eg the second table forbids a private invariant to mention public fields, which is allowed by the first table, because this means that anybody can break the invariant, which goes against the "logical" view sketched above. Of course, in general it is far from trivial to decide whether an invariant is private in the "logical" sense ! We cannot hope to decide this with a simple set of syntactical rules. The second table may be able to catch some private invariants that are not private in the "logical" sense, but it won't catch all of them. Maybe in a perfect world all invariants would be private in the "logical" sense. But it's well-known that in practice you cannot avoid invariants that can be violated by other objects - eg see Meyer's discussion of invariants in Eiffel. > Does it mean that a private invariant should not be preserved by > methods which do not see it? I find this semantics very strange! This not what I mean. A method should preserve all invariants, including those it cannot see. What I mean is that maybe - namely if we take the "logical" view of visibility modifiers - a method shouldn't have to worry about invariants that it cannot see, because it can't break those anyway. I hope the discussion above make the issue a bit clearer. It has done for me. Cheers, Erik From leavens@cs.iastate.edu Thu Jul 18 15:27:15 2002 Date: Thu, 18 Jul 2002 15:03:18 -0500 (CDT) From: Gary T. Leavens To: JML Interest List Subject: JML-Interest: Quiet flag for jml, jmlc, jmldoc as the default? Hi all, This isn't a weighty semantic issue, but one which we'd like your opinion on anyway. Currently, when one runs the jml checker, runtime assertion compiler, or documentation generator (jml, jmlc, or jmldoc, resp.), one gets by default output like: jml IntegerSet.java parsing IntegerSet.java parsing ../../../../specs/java/lang/Object.spec parsing ../../models/JMLDataGroup.java parsing ../../models/JMLObjectSet.java parsing ../../models/JMLType.java parsing IntegerSetInterface.java parsing ../../models/JMLValueSet.java parsing ../../models/JMLValueSetSpecs.java parsing ../../models/JMLListObjectNode.java parsing ../../models/JMLValueType.java parsing ../../models/JMLListException.java parsing ../../models/JMLSequenceException.java parsing ../../../../specs/java/lang/String.spec parsing ../../../../specs/java/util/Locale.jml parsing ../../models/JMLValueSequence.java parsing ../../models/JMLValueSequenceSpecs.java parsing ../../../../specs/java/lang/Class.jml parsing ../../../../specs/java/lang/ClassLoader.jml parsing ../../../../specs/java/util/Enumeration.spec parsing ../../../../specs/java/lang/Package.jml parsing ../../../../specs/java/lang/reflect/Field.spec parsing ../../../../specs/java/lang/reflect/AccessibleObject.jml parsing ../../../../specs/java/lang/reflect/Method.jml parsing ../../../../specs/java/lang/reflect/Constructor.jml parsing ../../models/JMLListValueNode.java parsing ../../models/JMLValueSequenceEnumerator.java parsing ../../models/JMLNoSuchElementException.java parsing ../../../../specs/java/lang/CharSequence.spec parsing ../../models/JMLObjectSetEnumerator.java parsing ../../models/JMLObjectType.java parsing ../../models/JMLValueSetEnumerator.java parsing ../../../../specs/java/lang/Integer.spec parsing ../../../../specs/java/lang/Number.spec parsing ../../../../specs/java/lang/Comparable.spec parsing TreeNode.java parsing SetSearchReturn.java parsing ../../../../specs/java/lang/Long.spec parsing ../../../../specs/java/util/Iterator.spec There is a way to make this a bit quieter, by using the -Q flag. Mostly, unless we're debugging things, we tend to use the -Q flag here when running these tools. On the other hand we think novice users may want to see what the scripts are doing, and it gives them some sense of progress. If there are no strong opinions on the matter we'll leave the default the way it is, as that seems easier for us. But let us know if you'd really like to have it changed. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From leavens@cs.iastate.edu Sat Jul 20 12:42:17 2002 Date: Sat, 20 Jul 2002 12:40:10 -0500 (CDT) From: Gary T. Leavens To: JML Interest List Subject: JML-Interest: "Helper" annotation being added to JML Hi, In the coming release of JML (next week I hope), we are adding the "helper" annotation from ESC/Java. This was discussed in the JML interest last way back in January of this year. That discussion went on for some time, however we perhaps never reached a definitive conclusion. However, we have decided for the moment to adopt the solution that various people (Michael Ernst, Rustan Leino, Cormac Flanagan, Bart Jacobs, John Field, Heike Wehrheim, Michael Norrish and myself) agreed-upon during our meeting in January, and was first floated on the this list: 1. By default, all [non-helper] instance methods of a type T must preserve all invariants and history constraints (of all visibilities) for type T (both static and non-static ones). All [non-helper] constructors of type T must preserve the static invariant and must establish the non-static invariant of type T. In particular, by default, [non-helper] private methods must preserve invariants and [validate] history constraints of type T, and [non-helper] private constructors must perserve static invariants and [validate] static history constraints of type T and must establish non-static invariants for the object of type T being initialized. [Non-helper] constructors would have to preserve invariants and [validate] history constraints of other objects of type T passed as arguments or in static fields. 2. The specifier can write the modifier "helper" on a private method or constructor. The semantics of this is that a such a helper method does not have to preserve any invariants and [does not have to validate any] history constraints, and that such a helper constructor does not have to preserve static invariants and [does not have to validate any] static history constraints, and does not have to establish the invariant for the object being initialized. 3. Only private methods and constructors may be declared with the "helper" modifier. Thus public, protected, and package visibility methods (and constructors) must preserve (establish) invariants and validate [(static in the case of constructors)] history constraints. One of the main reasons for adopting this syntax and semantics is because it corresponds pretty much exactly to what is already implemented in ESC/Java. The main reason for implementing it now is because it seems to also solve the problem with assertion checking for constructors in JML 3.0 that Marko van Dooren has pointed out to us. You may recall that, on the JML interest list, Steve Edwards suggested another alternative that would also work, which is to make all private methods be "helper" by default, and to have an annotation something like "respects_invariant" to say that such a method preserves, or in the case of a constructor establishes the invariant. However, the disadvantage of this is that it is not compatible with ESC/Java, and that from a survey of actual code, it appears that most private methods actually to preserve the invariant of a class, and so the default seems better this way. Another suggestion from that discussion was to have a general facility for naming assertions, and to say what parts owner variant, by naming the appropriate assertions, some private method should preserve. This would work, and we may want to pursue this in the future, but is quite a bit more complicated and would not be compatible with ESC/Java. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From leino@microsoft.com Mon Jul 22 13:29:26 2002 Date: Mon, 22 Jul 2002 11:05:15 -0700 From: Rustan Leino To: Gary T. Leavens , JML Interest List Subject: RE: JML-Interest: "Helper" annotation being added to JML Hello Gary,   You said: 2. The specifier can write the modifier "helper" on a private method    or constructor.  The semantics of this is that a such a helper    method does not have to preserve any invariants …   So a “helper” method does not need to preserve invariants, but can a “helper” method assume that invariants hold on entry?   ESC/Java handles this by inlining all “helper” methods and constructors, rather than checking them separately.  This means that helpers get to assume whatever is known in the context of the caller.  JML may want to say what one is allowed to assume on entry to a helper.   (Fine point:  In ESC/Java, recursive or mutually recursive calls to helper methods are not inlined.  And they are still not checked separately, an unsoundness.)     Another remark about “helper” in ESC/Java.  Any constructor or non-overridable, non-overriding method can be modified with the “helper” pragma.  However, the current implementation works properly only for calls within the same class.  Regrettably, the user gets no warning if “helper” is used in any other context.  For example, if you call “new” on a “helper” constructor in a different class, which in principle (and in particular, in the context of JML) is useful and makes perfect sense, then ESC/Java will not complain but it also won’t do the appropriate checking.     Rustan ^@ From erikpoll@cs.kun.nl Mon Jul 22 13:32:02 2002 Date: Mon, 22 Jul 2002 20:29:01 +0200 (CEST) From: Erik Poll To: Rustan Leino Cc: Gary T. Leavens , JML Interest List Subject: RE: JML-Interest: "Helper" annotation being added to JML > > 2. The specifier can write the modifier "helper" on a private method > or constructor. The semantics of this is that a such a helper > method does not have to preserve any invariants ... > > So a "helper" method does not need to preserve invariants, but can a > "helper" method assume that invariants hold on entry? I'd say that a helper method cannot assume that invariants hold on entry. For example, a public method might consist of two invocations of helper methods which together restore all the invariants. In such a situation the second invocation of a helper method will have a pre-state in which invariants are broken. > JML may want to > say what one is allowed to assume on entry to a helper. So I'd say that in JML a helper method may not assume anything that not explicitly stated in its precondition. Erik From leavens@cs.iastate.edu Mon Jul 22 13:50:12 2002 Date: Mon, 22 Jul 2002 13:45:35 -0500 (CDT) From: Gary T. Leavens To: Erik Poll Cc: Rustan Leino , JML Interest List Subject: RE: JML-Interest: "Helper" annotation being added to JML Erik, Rustan, On Mon, 22 Jul 2002, Erik Poll wrote: > > > > 2. The specifier can write the modifier "helper" on a private method > > or constructor. The semantics of this is that a such a helper > > method does not have to preserve any invariants ... > > > > So a "helper" method does not need to preserve invariants, but can a > > "helper" method assume that invariants hold on entry? > > I'd say that a helper method cannot assume that invariants hold > on entry. Yes, I agree here, that's one of the main points of the helper annotation, I thought. > For example, a public method might consist of two invocations > of helper methods which together restore all the invariants. > In such a situation the second invocation of a helper method > will have a pre-state in which invariants are broken. Yes. > > JML may want to > > say what one is allowed to assume on entry to a helper. > > So I'd say that in JML a helper method may not assume anything > that not explicitly stated in its precondition. Yes, I agree with this -- the way to say what is assumed is to use a precondition. I think it's best for documentation and verification purposes if this is done. It also seems to be quite modular and to handle recursive helper methods. I thought we agree for the semantics that the "helper" annotation only affects the verification conditions (or equivalently what the runtime assertion checker checks) for a method. For a helper method, the verification conditions don't include the (instance) invariant. (For a helper constructor, the postcondition that must be established also doesn't include the instance invariant.) Tools can use various strategies like inlining helpers if they wish, but that is an optimization (one hopes) on this semantics. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From edwards@cs.vt.edu Mon Jul 22 13:50:45 2002 Date: Mon, 22 Jul 2002 14:35:04 -0400 From: Stephen Edwards To: JML Interest List Subject: Re: JML-Interest: "Helper" annotation being added to JML Rustan Leino wrote: > ESC/Java handles this by inlining all "helper" methods and constructors, > rather than checking them separately. This means that helpers get to > assume whatever is known in the context of the caller. Since such "assumptions" may differ for different callers--and indeed differ as a class evolves over time--this introduces fragile coupling between the helper and the call site(s). The programmer must have made this segment into a separate method for a reason, though. In JML's case, wouldn't it be better for the helper method to explicitly state in its precondition what it needs to "assume"? Then that precondition can be checked at all call sites. Plus, the precondition is more useful for documentation and maintenance, especially if more than one person works on the class over time. Also, if helper operations do state their assumptions explicitly, should JML allow protected helpers rather than just private? It seems that in a subclass, which already has access to protected variables and must also uphold all inherited invariants, protected helpers that aid in common manipulation tasks on protected variables might be useful. This does not introduce any unsoundness, does it? Restricting helpers to private does not seem to guarantee anything--protected helpers provide no more opportunities for devious external access than already exists due to protected data members. One possible interpretation of "helper" is this: if we take "invariant" to simply mean an assertion that is implicitly and'ed onto every method's precondition and postcondition (with suitable modifications for initialization and finalization), then "helper" just means "don't implicitly 'and' the invariants onto this method's assertions; instead, all assumptions and guarantees are explicitly spelled out." -- Steve -- Stephen Edwards 604 McBryde Hall Dept. of Computer Science e-mail : edwards@cs.vt.edu U.S. mail: Virginia Tech (VPI&SU) office phone: (540)-231-5723 Blacksburg, VA 24061-0106 ------------------------------------------------------------------------------- From leavens@cs.iastate.edu Mon Jul 22 13:54:56 2002 Date: Mon, 22 Jul 2002 13:54:21 -0500 (CDT) From: Gary T. Leavens To: Stephen Edwards Cc: JML Interest List Subject: Re: JML-Interest: "Helper" annotation being added to JML Steve, Our mails crossed, but I must say I agree with you wholeheartedly about the use of preconditions to state assumptions. On Mon, 22 Jul 2002, Stephen Edwards wrote: > Rustan Leino wrote: > > ESC/Java handles this by inlining all "helper" methods and constructors, > > rather than checking them separately. This means that helpers get to > > assume whatever is known in the context of the caller. > > Since such "assumptions" may differ for different callers--and > indeed differ as a class evolves over time--this introduces fragile > coupling between the helper and the call site(s). The programmer must have > made this segment into a separate method for a reason, though. In JML's > case, wouldn't it be better for the helper method to explicitly state > in its precondition what it needs to "assume"? Then that precondition can > be checked at all call sites. Plus, the precondition is more useful for > documentation and maintenance, especially if more than one person works > on the class over time. Yes. > Also, if helper operations do state their assumptions explicitly, should > JML allow protected helpers rather than just private? It seems that in > a subclass, which already has access to protected variables and must also > uphold all inherited invariants, protected helpers that aid in common > manipulation tasks on protected variables might be useful. This does not > introduce any unsoundness, does it? Restricting helpers to private > does not seem to guarantee anything--protected helpers provide no more > opportunities for devious external access than already exists due to > protected data members. About the use of helper for protected methods, I am worried about callers who are in the same package in Java. > One possible interpretation of "helper" is this: if we take "invariant" to > simply mean an assertion that is implicitly and'ed onto every method's > precondition and postcondition (with suitable modifications for > initialization and finalization), then "helper" just means "don't implicitly > 'and' the invariants onto this method's assertions; instead, all assumptions > and guarantees are explicitly spelled out." Yes, I agree that this is the gist of the semantics. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From Marko.vanDooren@cs.kuleuven.ac.be Mon Jul 22 14:57:34 2002 Date: Mon, 22 Jul 2002 22:14:01 +0200 From: Marko van Dooren To: JML Interest List Subject: Re: JML-Interest: "Helper" annotation being added to JML > Also, if helper operations do state their assumptions explicitly, should > JML allow protected helpers rather than just private? It seems that in > a subclass, which already has access to protected variables and must also > uphold all inherited invariants, protected helpers that aid in common > manipulation tasks on protected variables might be useful. This does not > introduce any unsoundness, does it? Restricting helpers to private > does not seem to guarantee anything--protected helpers provide no more > opportunities for devious external access than already exists due to > protected data members. Actually, I think it is also necessary to have package accessible helper methods in order to be able to specify a bi-directional binding. One side will always invoke a method on the other side at a moment its own invariants do not hold, but the invariants of the object on which the method is invoked don't hold either because only 1 part of the bi-directional binding is set up. This makes me think, what can a helper method expect from its arguments ? In case of a bi-directional binding, that would be an object of which the invariants do not hold. Marko -- Jutil.org - Programming as you know it is over http://org-jutil.sourceforge.net From edwards@cs.vt.edu Mon Jul 22 14:59:05 2002 Date: Mon, 22 Jul 2002 15:16:36 -0400 From: Stephen Edwards To: JML Interest List Subject: Re: JML-Interest: "Helper" annotation being added to JML Gary T. Leavens wrote: > > About the use of helper for protected methods, I am worried about > callers who are in the same package in Java. OK, so you are worried about a caller outside the object potentially leaving the object in an inconsistent (invariant- violating state)? I can see that concern. OTOH, protected data members pose the same threat, right? That is, they are still open for package-level access from outside the class, even though they might be involved in some invariant. One neat thing about having invariants (that are inherited properly :-)) in the first place is that it does allow one to open up access a bit, allowing subclasses to see internal fields, while also obligating them to "behave correctly" if they tamper with any of them. I look at helper functions this way too--they may be common "internal utility" operations that subclasses can use too. But since Java doesn't really allow you to open things up to subclasses *without* also opening them to other entities in the same package--which are *not* operationally constrained by such invariant assertions in JML-- that's a problem. Currently, though, I'm thinking this is a problem with Java-- and one JML has to live with, because of the choice to build on Java. Saying non-private data members are "bad" is OK from the point of view of programming discipline, but that doesn't prevent others from writing them. Saying they are "dangerous, use with caution" may give guidance, but won't prevent erroneous use. Either approach would work with protected helpers too. Restricting "helper" doesn't really solve this problem, however--it just pushes it to a different area (the data member visibility). If you (a) restricted helpers to only be private, and (b) restricted all invariants to *only* mention (Java) private data members (regardless of spec visibility), you could syntactically prevent these issues and "seal" JML-spec'ed classes & objects from external influences that would leave them in an inconsistent state. But what will JML have lost? -- Steve -- Stephen Edwards 604 McBryde Hall Dept. of Computer Science e-mail : edwards@cs.vt.edu U.S. mail: Virginia Tech (VPI&SU) office phone: (540)-231-5723 Blacksburg, VA 24061-0106 ------------------------------------------------------------------------------- From erikpoll@cs.kun.nl Mon Jul 22 15:01:11 2002 Date: Mon, 22 Jul 2002 21:32:07 +0200 (CEST) From: Erik Poll To: JML Interest List Subject: Re: JML-Interest: "Helper" annotation being added to JML Gary wrote: > conclusion. However, we have decided for the moment to adopt the > solution that various people (Michael Ernst, Rustan Leino, Cormac > Flanagan, Bart Jacobs, John Field, Heike Wehrheim, Michael Norrish and > myself) agreed-upon during our meeting in January, and was first > floated on the this list: > > 1. By default, all [non-helper] instance methods of a type T must > preserve all invariants and history constraints (of all > visibilities) for type T (both static and non-static ones). All > [non-helper] constructors of type T must preserve the static > invariant and must establish the non-static invariant of type T. > In particular, by default, [non-helper] private methods must > preserve invariants and [validate] history constraints of type T, > and [non-helper] private constructors must perserve static > invariants and [validate] static history constraints of type T and > must establish non-static invariants for the object of type T being > initialized. [Non-helper] constructors would have to preserve > invariants and [validate] history constraints of other objects of > type T passed as arguments or in static fields. I can see that this restriction to the type T makes sense. (And it is what will actually be checked in the run-time checker.) The explanation above doesn't tell which invariants have to hold at the point in a method m in class T where another method n is invoked on an object s from class S. Presumably those of T (to cope with possible call-backs), but also those of S ? Presumably not, since we are restricting ourselves to the current class T. (Also, if we say the invariant of s must hold at this invocation point, then we must assume it held at the pre-state of m, and the whole restriction to the invariants of the current type T seems out of the window... ) The two viewpoints of the method invocation n.s(), from the prespective of the client class T and of the server class S, do then not agree on which invariants hold at this point of method invocation. Therefore I wonder if we shouln't keep the platonic ideal ALL invariants must hold at visible states (ie. all pre- and post-states of invocations of a non-helper methods) as the "offical" JML semantics, and take the restriction to the current type T as the compromise we (have to) make when we actually want to check something. Erik From leavens@cs.iastate.edu Mon Jul 22 15:19:48 2002 Date: Mon, 22 Jul 2002 15:17:02 -0500 (CDT) From: Gary T. Leavens To: Marko van Dooren Cc: JML Interest List Subject: Re: JML-Interest: "Helper" annotation being added to JML Marko, Steve, et al., On Mon, 22 Jul 2002, Marko van Dooren wrote: > > Also, if helper operations do state their assumptions explicitly, should > > JML allow protected helpers rather than just private? It seems that in > > a subclass, which already has access to protected variables and must also > > uphold all inherited invariants, protected helpers that aid in common > > manipulation tasks on protected variables might be useful. This does not > > introduce any unsoundness, does it? Restricting helpers to private > > does not seem to guarantee anything--protected helpers provide no more > > opportunities for devious external access than already exists due to > > protected data members. > > Actually, I think it is also necessary to have package accessible helper > methods in order to be able to specify a bi-directional binding. One side > will always invoke a method on the other side at a moment its own invariants > do not hold, but the invariants of the object on which the method is invoked > don't hold either because only 1 part of the bi-directional binding is set > up. We had this discussion earlier this year on the JML interest list. It would be easier on the writer of the specification to have "helper" be applicable to such methods, but our decision was, for now, not to allow that. Instead, we only allow helper on private methods and constructors. If you want to avoid having invariants apply in various states for non-private methods, then you have to use some extra logic, like the "dented" variable we described earlier. (Briefly, you make your invariant only apply to objects for which the value of "dented" is false, by writing something like "!dented ==> myRealInvariant". So during construction of a bi-directional binding, for example, both objects would be dented.) Yes, it's a pain to do this, but the advantages are that (a) it's very simple, and (b) the specificiations of methods that are potentially called by clients of all sorts explicitly reflect when they satisfy certain parts of the invariant. Let's try this semantics for a while and see if we can live with it. If we can't we'll find out soon enough. If we implemented the more liberal semantics we'll never know if we could have gotten by with this simple one. > This makes me think, what can a helper method expect from its arguments ? In > case of a bi-directional binding, that would be an object of which the > invariants do not hold. Just what the helper states in its preconditions for objects of the type in question. For other objects, which are in visible states, I think that their invariants must hold, as usual. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From leavens@cs.iastate.edu Tue Jul 30 17:51:05 2002 Date: Tue, 30 Jul 2002 16:34:52 -0500 (CDT) From: Gary T. Leavens To: JML Interest List Subject: JML-Interest: Sizes of JML model type collections limited to ints Hi all, Work with the JML model collection types, such as JMLObjectBag, JMLObjectSet, JMLObjectSequence, etc. has turned up an interesting (or perhaps troubling) limitation. We have specified the size() operation of these types to return an int value. Also indexes in JMLObjectSequence are Java ints. In effect, this means that - these collections can't contain more than Java's Integer.MAX_VALUE elements, and - the specification is wrong because it doesn't take into account integer overflow (wraparound). One fix is to use some infinite precision integer type, such as BigInteger or JMLFiniteInteger for sizes and indexes. This would not be convenient and certainly wouldn't be upward compatible. The fix I prefer is to rewrite the specifications of these collection types to take into account the finite nature of Java's int type. For example, in JMLObjectSet, we would specify that the insert, union, and powerSet methods require that the final sizes be representable as a Java int. Any objection to that? (P.S. Thanks to Patrice Chalin for bringing this issue to my attention, although it was my work with Brandon Shilling on java.util.Collection that revealed the specific problem for these types.) -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From leavens@cs.iastate.edu Wed Jul 31 14:48:29 2002 Date: Wed, 31 Jul 2002 14:31:42 -0500 (CDT) From: Gary T. Leavens To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: JML Release 3.1 Hi, We've just made another release of JML, 3.1, which is available from the JML web page: http://www.jmlspecs.org/ or directly from the JML ftp site: ftp://ftp.cs.iastate.edu/pub/leavens/JML/ in the file JML.3.1.tgz. This is a gzipped tar file, not a zip file. If you haven't upgraded from the 2.8 or 2.9 release of JML yet, now is probably the time to do so. This release features a much improved runtime assertion checker, thanks to Yoonsik Cheon. Also the refine clause now works, at least for type checking, thanks to Clyde Ruby. We have also put a lot effort into improving the quality of the documentation, utility, specifications, and implementations of the model types in the org.jmlspecs.models package. We have even better compatibility with ESC/Java in the specifications of these types. And the jmldoc tool is much improved, thanks to David Cok. Some other highlights of the changes are summarized below. See the NEWS.txt file in the release for other minor changes, including changes inherited from JML 3.0 (a release that was not widely announced) and several bug fixes. New with release 3.1 (July 31, 2002) major improvements: - Fixed bugs in lexical analysis found in JML 3.0 that caused JML keywords to be treated as reserved words and prevented some legal names from being used in specifications. (Thanks to Curt Clifton) - The refine clause now works, at least for type checking purposes. (Thanks to Clyde Ruby) It currently doesn't work for runtime assertion checking or jmldoc. - The tools now check whether 'also' is used correctly in specifications. (Thanks to David Cok) - Assertion violation exceptions are now subclasses of java.lang.Error, in order to avoid problems where code catches java.lang.Exception. - The runtime assertion checker is significantly improved and now works for most specfications. It has been extensively tested in the development of the JML model types. (Thanks to Yoonsik Cheon) - The runtime assertion checker now handles ghost variables and set statements. (Thanks to Yoonsik Cheon) - The runtime assertion checker now supports \TYPE, and type expressions including the \typeof, \type, and <: operators. (Thanks to Yoonsik Cheon) - The runtime assertion checker now supports non_null annotations to method return values. (These did not even parse in JML 3.0) - Assertion checking is turned off during construction of an object. (Thanks to Yoonsik Cheon) - Improvements to the output of jmlunit, which should make it easier to write the test data classes. (Thanks to Yoonsik Cheon) The jmlunit tool now checks for proper fixture initialization and also tests constructors. It has been extensively used in testing the JML model types. - The jmldoc tool no longer relies on running javadoc first. It's default behavior is to use the infrastructure of the multijava compiler (mjdoc) instead. This release also contains bug fixes and minor improvements to jmldoc; the current status is described in the package.html and TODO.txt files in org/jmlspecs/jmldoc. (Thanks to David Cok for all of the work on jmldoc) - The jmldoc tool now has a Model Fields section similar to the Fields sections, in which model fields are documented. (Thanks to David Cok) - The classes in the org/jmlspecs/models directory now have better specifications and javadoc comments for all methods. These no longer use the refine clause, so that they can be used with tools that don't implement the refine clause. In particular the enumerator types have been significantly better specified; their specifications also dovetail with ESC/Java. The collection types also maintain the elementType ghost variable to work better with ESC/Java. There is also a package overview that gives some orientataion to using the org.jmlspecs.models package in org/jmlspecs/models/package.html, which is accessible from the javadocs that ship with the release. - New model classes in org.jmlspecs.models include JMLDouble and JMLFloat. (Thanks to Joe Kiniry for the suggestion and to Brandon Shilling for the specifications.) incompatible changes: - The classes for assertion violations in the runtime assertion checker have been renamed from JMLAssertionException to JMLAssertionError, etc. - The specifications of java.lang.Iterator and java.lang.ListIterator provided in the specs directory no longer have the model sequence nextElements, because an iterator does not necessarily iterate over a finite collection. - The -t option to jmlunit now has the opposite default to its former value. - The deprecated index method of JMLObjectSequence and JMLValueSequence has been removed. - The interface CharSequence was removed from the org.jmlspecs.models package. Please let us know your comments on JML, and if you find bugs. See the TODO.txt file in the release for the ones we know about. See the preliminary design document for other acknowledgments. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From leavens@cs.iastate.edu Thu Aug 8 19:12:26 2002 Date: Thu, 8 Aug 2002 19:09:01 -0500 (CDT) From: Gary T. Leavens To: JML Interest List Subject: JML-Interest: Equating \TYPE and java.lang.class in JML? Hi all, Erik Poll suggested that JML should equate the type \TYPE with java.lang.Class. I'm in favor of it, as it would explain away the syntax we inherited from ESC/Java in terms of Java's reflective capabilities. The translation (which is what JML's runtime assertion checker uses) is as follows. ESC/Java syntax runtime representation --------------------------------------------------------------------- \TYPE java.lang.Class \typeof(Expr) [[Expr]].getClass() if Expr is of a reference type \typeof(7) Integer.TYPE \typeof(true) Boolean.TYPE \type(T) T.class Expr1 <: Expr2 [[Expr2]].isAssignableFrom([[Expr2]]) where Expr1 and Expr2 have type \TYPE where [[Expr]] is the value of the expression Expr. The reason ESC/Java has this syntax (and thus why JML does) is because they don't allow method calls in assertions. It seems reasonable to cater to tools like that in a subset of JML, but it would be nice to be able to desugar it in a standard way for tools as well. We don't see any problems with building this explanation into the language, but perhaps others see a problem? If so, please let us know. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From leavens@cs.iastate.edu Sun Aug 18 18:46:43 2002 Date: Sun, 18 Aug 2002 18:13:08 -0500 (CDT) From: Gary T. Leavens To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: JML 3.2, new release Hi, We've just made another release of JML, 3.2, which is available from the JML web page: http://www.jmlspecs.org/ or directly from the JML ftp site: ftp://ftp.cs.iastate.edu/pub/leavens/JML/ in the file JML.3.2.tgz. This is a gzipped tar file, not a zip file. Some highlights of the changes are summarized below. See the NEWS.txt file in the release for other changes, including changes inherited from JML 3.1 and several bug fixes. - The ESC/Java "helper" annotation is now supported in the runtime assertion checker. (This was actually in release 3.1.) - The runtime assertion checker now has an option, -F, that compiles specification inheritance without using Java's reflection API. This can be used to make faster, but less flexible, tests. It is still somewhat under development. - The runtime assertion checker now processes spec_public and spec_protected methods. (Thanks to Yoonsik Cheon) - The runtime assertion checker now executes the \elemtype operator in assertions. (Thanks to Erik Poll and Yoonsik Cheon) - The jmlunit tool now can deal properly with testing package-visible classes. (Thanks to Yoonsik Cheon) - The jmlunit tool now tests constructors, and also tests whether assertions are compiled with the runtime assertion checker (jmlc). - jmldoc now supports the -group option and uses it in preparing the documentation for JML; -help for jmldoc now has a complete list of options; annotation modifiers on methods, constructors, and formal arguments are displayed; informal predicates utilize html special characters where appropriate; ghost fields and model fields are displayed (separately), in a way similar to how javadoc displays fields; spec_public and spec_protected are now used to determine whether to include members and annotations in html files. (Thanks to David Cok) - Much work on the reference manual, in the introduction and in the sections on method specifications and invariants (Thanks to Erik Poll). This now begins to be useful. There are also the following incompatible changes from release 3.1: - The default for invariants and constraints in interfaces is static, so in interfaces they no loner can refer to instance fields unless the "instance" modifier is present. - jmldoc no longer supports the obsolete options --usejavadoc, --nousejavadoc, --embedded, --undo, --htmlLevel (use -private, -protected, -package, -public for htmlLevel), --link (use -link), --linkoffline (use -linkoffline). - In jmldoc, the -D option is now declared an error because it can be interpreted as either -d or --deprecation. - The collection types (sets, bags, sequences) in the org.jmlspecs.models package asserted that the elementType was the least upper bound on the elements in the collection. This was not true--it's only an upper bound. - The org.jmlspecs.models.JML*Relation types have a different method for "elements" than previously; this is to make the type more uniform with the other collections. - The org.jmlspecs.models.JMLModel*Set types now have methods instead of variables, which makes a few of the methods useful. Please let us know your comments on JML, and if you find bugs. See the TODO.txt file in the release for the ones we know about. See the preliminary design document for other acknowledgments. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From leavens@cs.iastate.edu Tue Sep 24 11:29:05 2002 Date: Tue, 24 Sep 2002 11:11:43 -0500 (CDT) From: Gary T. Leavens To: JML Non-local Users -- Albert C. Esterline , Arnd Poetzsch-Heffter , Bernhand Rumpe , Bharat Jayaraman , Cary Burnette , Chrislain Razafimahefa , Krishna Kishore Dhara , Doug Lea , Franklin Chen , Joe Oberleitner , Jon Squire , Keith Brian Gallagher , Magne Haveraaen , Paolo Ciancarini , Paul Grabow , Peter Mueller , Richard Lewis-Shell , JML Interest List , Thomas Lindner , William Buford Subject: JML-Interest: New Release of JML 3.3 available Hi all, We've just made another release of JML, 3.3, which is available from the JML web page: http://www.jmlspecs.org/ or directly from the JML ftp site: ftp://ftp.cs.iastate.edu/pub/leavens/JML/ in the file JML.3.3.tgz. This is a gzipped tar file, not a zip file. Some highlights of the changes are summarized below. See the NEWS.txt file in the release for other changes, including changes inherited from JML 3.2 and several bug fixes. - The JML type checker now performs visibility checking in assertions. So public specifications can only use public attributes, for example. (Thanks to Yoonsik Cheon.) - The JML type checker now prohibits the use of =, +=, ++, --, etc. in assertions. (Thanks to Yoonsik Cheon.) - The tools now support Java assert statements and understand the -source command-line option (from javac). (Thanks to Curtis Clifton and Todd Millstein.) - The runtime assertion checker now gives error messages for assertion violations that include useful debugging information (e.g., values of parameters, fields, \result, the exception thrown, this, etc.). Also, the label of a labeled expression is printed as a part of the assertion violation. (Thanks to Yoonsik Cheon.) - The runtime assertion checker generates better messages for non_null annotation violations. (Thanks to Yoonsik Cheon.) - More control over the runtime assertion checking compiler. The jmlc tool now has an option, --noredundancy (-C), for disabling runtime assertion checking for redundant specifications, such as requires_redundantly and ensures_redundantly. (Thanks to Yoonsik Cheon.) - The jmldoc tool now displays model methods, constructors, and inner classes in separate sections. It also separates out model fields from normal fields. (Thanks to David Cok.) - The jmldoc tool now has an extension to javadoc in which unqualified class references in see/link tags in a package.html file are resolved if they are in the same package as the package.html file. (Thanks to David Cok.) Please let us know your comments on JML, and if you find bugs. See the TODO.txt file in the release for the ones we know about. See the preliminary design document for other acknowledgments. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From leavens@cs.iastate.edu Thu Oct 3 11:55:09 2002 Date: Thu, 3 Oct 2002 11:30:10 -0500 (CDT) From: Gary T. Leavens To: JML Interest List Subject: JML-Interest: new JML tool ! (fwd) Hi all, You may be interested in this news from Erik Poll about JML -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 ---------- Forwarded message ---------- Date: Tue, 1 Oct 2002 17:32:22 +0200 (CEST) >From: Erik Poll To: Gary T. Leavens Subject: new JML tool ! Last week in France we met up with some people for the smartcard manufacturer Gemplus, who are in a European project with us. They gave us a demo of a tool for JML they are developing. It's something along the lines of ESC/Java - ie. the user doesn't see the theorem prover and the approach is not sound or complete. I guess that seeing ESC/Java in action on some of their code really convinced them of the value of such a tool! Their tool uses the B theorem prover, and the tool is integrated with the IDE that their developers use. It's not as good as ESC/Java in what it can prove, but has quite a fancy interface, where you can pop up list of goals to be poven for some method, see which ones the tool couldn't manage to prove etc. The tool will be presented at a developers' conference they organize next month : http://www.gemplus.com/developers/events/conf/session_abstract.html#jack Thought you might like to know. Always nice to hear that some people in industry are seriously interested in this kind of work ;-) Cheers, Erik From leavens@cs.iastate.edu Sun Oct 27 14:50:56 2002 Date: Sun, 27 Oct 2002 12:02:34 -0600 (CST) From: Gary T. Leavens To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: Purity checking and the purity of Object's "equals" method Hi all, This is a note about the conflict between Java's use of its "equals" method and purity checking in JML. In Java, the method "boolean equals(Object o)" in Object plays an important role in collections and in their specifcations. For example, in the interface java.util.List, the the javadocs say that the method "boolean remove(Object o)" removes the first object in the list, x, such that o.equals(x) (modulo handling of null). In JML we have a problem with purity checking and "equals". The problem is that: 1. We don't want to make equals in Object be specified as "pure", since this would prohibit benevolent side effects in any object's "boolean equals(Object o)" method. 2. To fully specify interesting properties of methods in collection types, such as java.util.List's remove method, we need to use the "equals" method on Objects, and thus Object's "equals" method must be pure. The first issue is particularly acute in Java, because it has a rooted, single-inheritance hierarchy, and by-name subtyping. Thus if we choose to make Object's equals method pure, we would be (retroactively) making every "equals(Object)" method of every type written in Java be pure. We know that it is common to want benelolent side effects in writing some equals methods for some types (e.g., for rational numbers being reduced to lowest terms). And JML's semantics does prohibit even benevolent side effects in pure methods; which Leino has pointed out is necessary for soundness of verification with modifies clauses. On the other hand, although we can (and have) specified that most methods that override Object's "equals" method are pure, when dealing with a collection of Objects, there is no substitute for the Object's "equals" method; that is wired into the specification of java.util.List and many other Java collection classes. Because pure methods must be used in assertions, and because pure methods can only call other pure methods, if Object's equals method is not pure, then no pure method can call it, including other model methods. Thus it becomes difficult to specify properties of collection classes with any precision, if the specifications rely on Object's "equals" method. Another relevant consideration is that whenever we start enforcing purity checking in JML, users will probably assume that "equals" is always pure, and may be confused that they have to specify such a basic property, and that they can't use Object's "equals" method in assertions. Two language design heuristics seem relevant here. First, it seems that making "equals" pure would make things work for 90% of people. The minority of cases that need side-effects in "equals" would be caught by purity checking. Second, if we don't impose this restriction, we'll never know if we could live with it and get its benefits. These arguments are making me think that we should take the somewhat radical step of specifying Object's "equals" method as a pure method. Although this would constrain the kind of programs people can specify with JML, the limitations could (one day) be enforced by purity checking. And the gains in ease of use and expressiveness for JML seem like they would pay us back. Yoonsik Cheon suggested that we do this when he put in to the JML checker the (limited) form of purity checking that it has so far. I argued point 1 above at the time, but now that I have looked at the specifications of java.util's collection classes in more detail, I think I was probably wrong. Do you have any thoughts on all this? Do you have an "equals" method that uses side effects in a crucial way and that can't be worked around? -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From boyland@solomons.cs.uwm.edu Mon Oct 28 14:29:18 2002 Date: Mon, 28 Oct 2002 10:22:21 -0600 From: John Tang Boyland To: Gary T. Leavens Cc: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: Purity checking and the purity of Object's "equals" method ] In JML we have a problem with purity checking and "equals". The ] problem is that: ] ] 1. We don't want to make equals in Object be specified as "pure", ] since this would prohibit benevolent side effects in any object's ] "boolean equals(Object o)" method. ] ] 2. To fully specify interesting properties of methods in collection ] types, such as java.util.List's remove method, we ] need to use the "equals" method on Objects, and thus Object's "equals" ] method must be pure. Gary, Yes, we struggle with similar issues. I've been mainly focusing on "hashCode" which again is "semantically pure" but many implementations (including that for "java.lang.String") include benign side-effects that essentially cache the value computed. Since we check read-effects as well as write-effects, we have another issue with equals: the fact that it (and hashCode()) are required by the Java Spec to depend on mutable information, although that means hashCode is dangerous to use for its declared purpose (hashing). Our solution here (which hasn't been fully developed) is to say that the Objects that come into a HashTable (or HashMap) must have an "immutable" equality region=datagroup: so that the hashCode will not change. My current take on benign side-effects is to try to see if we can come up with familes of benign side-effects which can be checked to be truly benign. If I recall, the side-effects that Rustan Leino found to be not-so-benign were so-called "temporary side-effects" wheere a field is temporarily changed and then changed back. A system with read-effects could be used to ensure that such effects were truly unnoticeable. Similarly, caching can be checked if the values cached are unchanging and if the cached value can be written atomically. John From leavens@cs.iastate.edu Mon Oct 28 18:32:29 2002 Date: Mon, 28 Oct 2002 18:30:52 -0600 (CST) From: Gary T. Leavens To: John Tang Boyland Cc: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: Purity checking and the purity of Object's "equals" method John, Thanks for your reply... On Mon, 28 Oct 2002, John Tang Boyland wrote: > ] In JML we have a problem with purity checking and "equals". The > ] problem is that: > ] > ] 1. We don't want to make equals in Object be specified as "pure", > ] since this would prohibit benevolent side effects in any object's > ] "boolean equals(Object o)" method. > ] > ] 2. To fully specify interesting properties of methods in collection > ] types, such as java.util.List's remove method, we > ] need to use the "equals" method on Objects, and thus Object's > ] "equals" method must be pure. > > Yes, we struggle with similar issues. I've been mainly focusing > on "hashCode" which again is "semantically pure" but many > implementations (including that for "java.lang.String") include > benign side-effects that essentially cache the value computed. I didn't know that before, but it's in the code... > Since we check read-effects as well as write-effects, we have another > issue with equals: the fact that it (and hashCode()) are required > by the Java Spec to depend on mutable information, although that means > hashCode is dangerous to use for its declared purpose (hashing). > Our solution here (which hasn't been fully developed) is to > say that the Objects that come into a HashTable (or HashMap) must > have an "immutable" equality region=datagroup: so that the hashCode > will not change. I'm not sure I fully understand what you're saying. Is it that Object has a datagroup that includes all of the storage that the hashCode could depend on? And then how do you make sure that this datagroup can't be mutated while the object is in the Hashtable? I suppose some type system annotations do this? > My current take on benign side-effects is to try to see if we > can come up with familes of benign side-effects which can be > checked to be truly benign. If I recall, the side-effects that > Rustan Leino found to be not-so-benign were so-called "temporary > side-effects" wheere a field is temporarily changed and then changed > back. A system with read-effects could be used to ensure > that such effects were truly unnoticeable. Similarly, caching can be > checked if the values cached are unchanging and if the > cached value can be written atomically. That is interesting. We do have an accessible clause in JML that can be used to specify read-effects. And it would be nice to have a middle way out of our quandry in JML. But it sounds rather complicated. Can you tell us something of how that would apply to JML? -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From kiniry@acm.org Tue Oct 29 05:05:22 2002 Date: Tue, 29 Oct 2002 11:56:15 +0100 From: Joseph Kiniry To: Gary T. Leavens Cc: jml-interest-list@cs.iastate.edu Subject: JML-Interest: Re: Purity checking and the purity of Object's "equals" method Hi everyone, Why not integrate the semantics of "pure" with the (ongoing?) semantics of scoped specifications? Thus, a pure public method denotes a method whose side-effects are invisible via any public method call, but are potentially visible by all more restricted calls. A pure private's side effects, on the other hand, are invisible via *any* method call. Likewise, specification method dependencies between pure and helper methods are scoped identically: a pure public method's specification can reference only other pure public methods and not pure [protected|package|private] pure methods, etc. Checking the latter would be straightforward enough. Analysis on the former is non-trivial unless you have full modifies coverage. Joe P.S. I currently use pure in the manner exactly matching the proposed semantics ("completely side-effect-free"), but I certainly understand the issues wrt base methods like equals() and hashcode(), especially in non-trivial class design. "Gary T. Leavens" writes: > Hi all, > > This is a note about the conflict between Java's use of its "equals" > method and purity checking in JML. ...snip... > Do you have any thoughts on all this? Do you have an "equals" > method that uses side effects in a crucial way and that can't be > worked around? From boyland@solomons.cs.uwm.edu Tue Oct 29 10:10:58 2002 Date: Tue, 29 Oct 2002 09:18:48 -0600 From: John Tang Boyland To: Gary T. Leavens Cc: John Tang Boyland , jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: Purity checking and the purity of Object's "equals" method Gary, Some further explanations: ] > Since we check read-effects as well as write-effects, we have another ] > issue with equals: the fact that it (and hashCode()) are required ] > by the Java Spec to depend on mutable information, although that means ] > hashCode is dangerous to use for its declared purpose (hashing). ] > Our solution here (which hasn't been fully developed) is to ] > say that the Objects that come into a HashTable (or HashMap) must ] > have an "immutable" equality region=datagroup: so that the hashCode ] > will not change. ] ] I'm not sure I fully understand what you're saying. Is it that Object ] has a datagroup that includes all of the storage that the hashCode ] could depend on? And then how do you make sure that this datagroup ] can't be mutated while the object is in the Hashtable? I suppose some ] type system annotations do this? Exactly. I'm working on a type system that handles pointer types like "uniqueness" and "immutability" as well as read and write effects (using datagroups eventually). ] > My current take on benign side-effects is to try to see if we ] > can come up with familes of benign side-effects which can be ] > checked to be truly benign. If I recall, the side-effects that ] > Rustan Leino found to be not-so-benign were so-called "temporary ] > side-effects" wheere a field is temporarily changed and then changed ] > back. A system with read-effects could be used to ensure ] > that such effects were truly unnoticeable. Similarly, caching can be ] > checked if the values cached are unchanging and if the ] > cached value can be written atomically. ] ] That is interesting. We do have an accessible clause in JML that can ] be used to specify read-effects. And it would be nice to have a middle ] way out of our quandry in JML. But it sounds rather complicated. Unfortunately yes, it does end up being complicated. ] Can you tell us something of how that would apply to JML? Assuming "accessible" works interprocedurally and inter-object, then essentially you ensure that the temporarily changed field is not read in any methods called while its change is in effect. Come to think of it, it isn't very useful unless you're doing something like Alias Burying (where a unique variable loses its uniqueness temporarily, which is OK if you don't read it while it is compromised). I can't think of a good reason to change a supposedly unmodified field in a method if its temporary value is never noticed.... With regard to caching, all I can offer are half-baked thoughts: (1) as I said before, the cached value should be atomically updateable. (2) the cache must be kept coherent. The easiest way to do this is to ensure it is computed with a "pure" expression, something that depends on immutable state only. (3) we ensure that the cache is never used unless it is immediately checked for whetehr it has been computed. For example, a strings hashCode cache is only used in the idiom: if (cache == 0) { cache = } ... use cache ... (This would require that the cache be "private" to ensure we could check all its use.) It seems plausible that this could be checked, but I haven't done the rigorous definition and proof. There may be other gotchas. John From boyland@solomons.cs.uwm.edu Tue Oct 29 10:11:55 2002 Date: Tue, 29 Oct 2002 09:28:37 -0600 From: John Tang Boyland To: Joseph Kiniry Cc: Gary T. Leavens , jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: Re: Purity checking and the purity of Object's "equals" method Some comments on "public pure" etc. ] Why not integrate the semantics of "pure" with the (ongoing?) ] semantics of scoped specifications? ] ] Thus, a pure public method denotes a method whose side-effects are ] invisible via any public method call, but are potentially visible by ] all more restricted calls. A pure private's side effects, on the ] other hand, are invisible via *any* method call. This sounds potentially useful but there are multiple problems awaiting the unwary. For example, suppose a "public pure" method updated some protected field. How can we be sure that some public method of (a) a subclass or (b) some other class in the package doesn't expose the value? We have to worry about combinations too: For example, another class in the package may have a protected method that accesses this updated protected field and it may have a subclass in another package which uses the result of this protected method to compute the result of a public method. The same problem occurs (I believe) with public/protected/private invariants. It is very tricky to come up with a semantics that is both sound and useful unless we stick with "private invariants" and "private pure". I believe JML has already made strides towards defining what invariants mean; it may be the same technique can be used for "public pure" et al, but I still have reservations. John From leavens@cs.iastate.edu Tue Oct 29 10:46:15 2002 Date: Tue, 29 Oct 2002 10:22:18 -0600 (CST) From: Gary T. Leavens To: John Tang Boyland Cc: Joseph Kiniry , JML Interest List Subject: Re: JML-Interest: Re: Purity checking and the purity of Object's "equals" method John, Thanks for your further explanations of your ideas and comments on Joe's proposal. It sounds like we should do the following for now. - declare java.lang.Object's equals method to be pure - still allow benevolent side effects in Object's hashCode method, (i.e., don't declare it to be pure) We'll have to recognize that this solution isn't ideal. While we do that, I think we should keep investigating more refined semantics and try to find something better for purity checking. But it sounds like the alternatives we've looked at so far aren't fully baked yet and/or require significant support from the type checker. While I'd like to have some alias control mechanism in JML, it's not clear exactly what that should be yet. Does that sound reasonable for the short term? -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From erikpoll@cs.kun.nl Tue Oct 29 11:00:00 2002 Date: Tue, 29 Oct 2002 17:45:11 +0100 (CET) From: Erik Poll To: Gary T. Leavens Cc: JML Interest List Subject: JML-Interest: Re: Purity checking and the purity of Object's "equals" method > It sounds like we should do the following for now. > > - declare java.lang.Object's equals method to be pure > - still allow benevolent side effects in Object's hashCode method, > (i.e., don't declare it to be pure) > > We'll have to recognize that this solution isn't ideal. > ... > Does that sound reasonable for the short term? Yes, I think this is a sensible compromise. While we're on the subject of equals: this discussion reminded me of another issue with equals that I noticed earlier. If a class overrides the equals method, it typically provides a _weaker_ notion of equality then Object provides, namely some "structural" notion of equality rather than reference equality. This makes it is tricky to come up with a good spec for equals in Object, ie. one that doesn't cause problems with behavioural subtyping. More specifically, I think that the current spec in specs/java/lang/Object.jml is too strong: it includes @ protected normal_behavior @ ensures \result <==> this == obj; but not all subclasses wil meet this spec (eg java.lang.Byte doesn't) Erik From leavens@cs.iastate.edu Tue Oct 29 11:17:22 2002 Date: Tue, 29 Oct 2002 11:15:57 -0600 (CST) From: Gary T. Leavens To: Erik Poll Cc: JML Interest List Subject: Re: JML-Interest: Re: Purity checking and the purity of Object's "equals" method Erik, On Tue, 29 Oct 2002, Erik Poll wrote: > > It sounds like we should do the following for now. > > > > - declare java.lang.Object's equals method to be pure > > - still allow benevolent side effects in Object's hashCode method, > > (i.e., don't declare it to be pure) > > > > We'll have to recognize that this solution isn't ideal. > > ... > > Does that sound reasonable for the short term? > > Yes, I think this is a sensible compromise. Ok, thanks. > While we're on the subject of equals: this discussion reminded me > of another issue with equals that I noticed earlier. > If a class overrides the equals method, it typically provides a > _weaker_ notion of equality then Object provides, namely some > "structural" notion of equality rather than reference equality. > > This makes it is tricky to come up with a good spec for equals > in Object, ie. one that doesn't cause problems with behavioural > subtyping. > More specifically, I think that the current spec in > specs/java/lang/Object.jml > is too strong: it includes > > @ protected normal_behavior > @ ensures \result <==> this == obj; > > but not all subclasses wil meet this spec (eg java.lang.Byte doesn't) It's true that the above does document the behavior of equals for Object and that this is not done in many other types (like Byte). So in the current JML semantics this is too strong, in that it would make other types (like Byte) not be correctly implemented. But then how do we document the behavior of Object's equals method to be used in super calls? Perhaps the problem is that the current semantics of specification inheritance in JML is too strong? We say in the preliminary design document for JML (and in the desugaring method specifications paper) that a subtype inherits both public and protected specifications for methods. However, that causes the above problem. I wonder if we should adopt a semantics more like what Clyde Ruby and I have designed for subclassing contracts, where the subclassing contracts are not inherited by subtypes, but are used in reasoning about the class when it is used as a superclass, e.g., in determining if super calls are valid. That is, I wonder if we should only inherit public specifications from supertypes, and use the protected specifications only to reason about calls to the supertype's methods (or to unoverridden methods...). I have yet to think through the ramifications of this in terms of how it might apply to invariants and history constraints. I'm not sure what the runtime assertion checker is doing in this respect either... although I know it's not enforcing the contracts in java.lang.Object yet. This would also potentially mean a change for jmldoc if adopted. Comments? -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From erikpoll@cs.kun.nl Wed Oct 30 04:32:02 2002 Date: Wed, 30 Oct 2002 11:27:37 +0100 (CET) From: Erik Poll To: Gary T. Leavens Cc: JML Interest List Subject: Re: JML-Interest: Re: Purity checking and the purity of Object's "equals" method > It's true that the above does document the behavior of equals for > Object and that this is not done in many other types (like Byte). So > in the current JML semantics this is too strong, in that it would make > other types (like Byte) not be correctly implemented. But then how do > we document the behavior of Object's equals method to be used in super > calls? We don't :-) You have to look at the code of the super-method to see what it does. Seriously, safely creating correct subclasses without seeing the actual code of the superclass is a very tricky issue - as some excellent papers on this subject make clear. Just treating protected specifications different when it comes to inheritance isn't going to solve this issue. > Perhaps the problem is that the current semantics of specification > inheritance in JML is too strong? We say in the preliminary design > document for JML (and in the desugaring method specifications paper) > that a subtype inherits both public and protected specifications for > methods. I always thought that a subtype inherited _all_ the specs of its parent, and that you needed that in order to get behavioural subtyping. Eg if a subclass parent doesn't respect a package spec of its parent (eg if java.lang.Byte would violate some package visible spec of equals given in java.lang.Object), then package clients of its parent class have a problem. > That is, I wonder if we should only inherit public > specifications from supertypes, and use the protected specifications > only to reason about calls to the supertype's methods (or to > unoverridden methods...). Maybe we should give no semantic meaning to the visibility modifiers at all ? Erik PS. Looks like we'll have plenty to discuss at FMCO next week :-) From leavens@cs.iastate.edu Wed Oct 30 04:51:39 2002 Date: Wed, 30 Oct 2002 04:47:16 -0600 (CST) From: Gary T. Leavens To: Erik Poll Cc: JML Interest List Subject: Re: JML-Interest: Re: Purity checking and the purity of Object's "equals" method Hi Erik, et al., On Wed, 30 Oct 2002, Erik Poll wrote: > > It's true that the above does document the behavior of equals for > > Object and that this is not done in many other types (like Byte). So > > in the current JML semantics this is too strong, in that it would make > > other types (like Byte) not be correctly implemented. But then how do > > we document the behavior of Object's equals method to be used in super > > calls? > > We don't :-) You have to look at the code of the super-method to see > what it does. > > Seriously, safely creating correct subclasses without seeing the actual > code of the superclass is a very tricky issue - as some excellent papers > on this subject make clear. Just treating protected specifications > different when it comes to inheritance isn't going to solve this issue. Yes, I am keenly interested in working on how to do this. I do think that maybe treating protected method specifications differently when it comes to inheritance may be part of the solution to this problem, however. Note that for behavioral subtyping, clients only use the public specifications of methods. I do think it's complicated, as you say, however, in that it doesn't seem like we can be so cavilier with inheritance of protected invariants and history constraints. Also, I worry that, since invariants and history constraints are something of an abbreviation mechanism for method specifications (although not exactly), there will be problems if we adopt such a semantics. So I'm not proposing we rush into this. > > Perhaps the problem is that the current semantics of specification > > inheritance in JML is too strong? We say in the preliminary design > > document for JML (and in the desugaring method specifications paper) > > that a subtype inherits both public and protected specifications for > > methods. > > I always thought that a subtype inherited _all_ the specs of its parent, > and that you needed that in order to get behavioural subtyping. That is roughly the semantics of JML currently, although private specifications are never inherited, and package visible specifications are only inherited by subtypes in the same package. > Eg if a subclass parent doesn't respect a package spec of its parent > (eg if java.lang.Byte would violate some package visible spec of equals > given in java.lang.Object), then package clients of its parent class > have a problem. That seems certain to be true for invariants and history constraints. I'm not sure it applies to method specifications for overridden methods. > PS. Looks like we'll have plenty to discuss at FMCO next week :-) Yes indeed. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From marinov@cag.lcs.mit.edu Thu Oct 31 07:19:23 2002 Date: Thu, 31 Oct 2002 07:40:51 -0500 From: Darko Marinov To: JML Interest List Subject: Re: JML-Interest: Re: Purity checking and the purity of Object's "equals" method I'd like to add some more comments on the subject of "equals", based on the work that Sarfraz Khurshid, Daniel Jackson, and myself did on AAL. (Sarfraz will present this work in a couple of days at OOPSLA.) Regarding purity, we considered all "equals" methods to be pure. We also had some assumptions on termination, but it's not relevant here. Regarding the specification of "Object.equals", or in general any method, we allow annotations to describe: 1. a specification which is essentially the same as in JML, i.e., consists of class invariants, pre- and post-conditions. 2. a *model* which can be stronger than the specification. A model can be used for reasoning about invocations for which the dynamic type of the receiver is known at compile time, e.g.: Object o = new Object(); o.equals(...); A specification is used when the type is not known, e.g.: void m(Object o) { o.equals(...); For a subclass to be a subtype (rather to allow modular checking), it needs to respect the specification, but not necessarily the model, of its superclass. This allows us to write the precise model for "Object.equals", using keyword "does": //@ does \result == true <==> this == o; We can also give a weaker specification for this method, e.g.: //@ ensures this == o ==> \result == true; Notice that this post-condition specifies that "equals" method is reflexive. By the informal comments/spec in "java.lang.Object", this is what is required for "equals" methods of all classes. Moreover, "equals" methods are required to be symmetric and transitive (and be consistent with "hashCode" etc.). We have made some progress on checking these properties of "equals" methods for some examples. This brings up an interesting issue of a specification that does not seem amenable to modular checking. I could provide more details if there is interest (and when I find some email access in Seattle :). Darko > Erik, > > On Tue, 29 Oct 2002, Erik Poll wrote: > > > > It sounds like we should do the following for now. > > > > > > - declare java.lang.Object's equals method to be pure > > > - still allow benevolent side effects in Object's hashCode method, > > > (i.e., don't declare it to be pure) > > > > > > We'll have to recognize that this solution isn't ideal. > > > ... > > > Does that sound reasonable for the short term? > > > > Yes, I think this is a sensible compromise. > > Ok, thanks. > > > While we're on the subject of equals: this discussion reminded me > > of another issue with equals that I noticed earlier. > > If a class overrides the equals method, it typically provides a > > _weaker_ notion of equality then Object provides, namely some > > "structural" notion of equality rather than reference equality. > > > > This makes it is tricky to come up with a good spec for equals > > in Object, ie. one that doesn't cause problems with behavioural > > subtyping. > > More specifically, I think that the current spec in > > specs/java/lang/Object.jml > > is too strong: it includes > > > > @ protected normal_behavior > > @ ensures \result <==> this == obj; > > > > but not all subclasses wil meet this spec (eg java.lang.Byte doesn't) > > It's true that the above does document the behavior of equals for > Object and that this is not done in many other types (like Byte). So > in the current JML semantics this is too strong, in that it would make > other types (like Byte) not be correctly implemented. But then how do > we document the behavior of Object's equals method to be used in super > calls? > > Perhaps the problem is that the current semantics of specification > inheritance in JML is too strong? We say in the preliminary design > document for JML (and in the desugaring method specifications paper) > that a subtype inherits both public and protected specifications for > methods. However, that causes the above problem. I wonder if we > should adopt a semantics more like what Clyde Ruby and I have designed > for subclassing contracts, where the subclassing contracts are not > inherited by subtypes, but are used in reasoning about the class when > it is used as a superclass, e.g., in determining if super calls are > valid. That is, I wonder if we should only inherit public > specifications from supertypes, and use the protected specifications > only to reason about calls to the supertype's methods (or to > unoverridden methods...). > > I have yet to think through the ramifications of this in terms of how > it might apply to invariants and history constraints. I'm not sure > what the runtime assertion checker is doing in this respect either... > although I know it's not enforcing the contracts in java.lang.Object yet. > This would also potentially mean a change for jmldoc if adopted. > > Comments? > > -- > > Gary T. Leavens > Department of Computer Science, Iowa State University > 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA > http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From leavens@cs.iastate.edu Fri Nov 1 01:05:35 2002 Date: Thu, 31 Oct 2002 18:17:24 -0600 (CST) From: Gary T. Leavens To: JML Non-local Users -- Albert C. Esterline , Arnd Poetzsch-Heffter , Bernhand Rumpe , Bharat Jayaraman , Cary Burnette , Chrislain Razafimahefa , Krishna Kishore Dhara , Doug Lea , Eve _fon_5 , Franklin Chen , Joe Oberleitner , Jon Squire , Keith Brian Gallagher , Magne Haveraaen , Paolo Ciancarini , Paul Grabow , Peter Mueller , Richard Lewis-Shell , Thomas Lindner , William Buford Cc: JML Interest List Subject: JML-Interest: New Release of JML, 3.4, available Hi all, Happy Halloween. We've just made another release of JML, 3.4, which is available from the JML web page: http://www.jmlspecs.org/ or directly from the JML ftp site: ftp://ftp.cs.iastate.edu/pub/leavens/JML/ in the file JML.3.4.tgz. This is a gzipped tar file, not a zip file. The major improvements in the release and incompatible changes are summarized below. See the NEWS.txt file in the release for other changes, including many minor impovements and bug fixes. New with release 3.4 (October 31, 2002) major improvements: - Ant tasks and some sample build files for running the JML tools with Ant are included in org.jmlspecs.ant. (Thanks to Marko van Dooren.) - The tools now are able to deal with package names, not just directories, on the command line. (Thanks to David Cok.) - The propagation of purity annotations from classes to non-static methods and from superclasses to subclasses now works. (Thanks to Yoonsik Cheon.) - JML now properly handles Java assert statements (in Java 1.4). (Thanks to Todd Millstein and Yoonsik Cheon.) - The syntax and checking of weak behavioral subtypes and constraint clauses with "for" parts are now supported. (Thanks to Yoonsik Cheon.) - The runtime assertion checker now checks loop invariants (maintaining) and variant functions (decreasing). (Thanks to Yoonsik Cheon.) - The runtime assertion checker now handles exceptions and non-executable specifications in the context of equality operators in a way that is better (less confusing). (Thanks to Yoonsik Cheon.) - The runtime assertion checker now can execute specifications of interfaces in JDK classes, such as java.util. - The runtime assertion checker now can execute some model methods with bodies. (Thanks to Yoonsik Cheon.) - In jmldoc, the -R/--recursive flag now applies to package names on the command line as well as directories. (Thanks to David Cok.) incompatible changes: - Object's equals method is now specified as pure. This means that JML now demands that methods named equals that take an Object as an argument have to be side-effect free, and even benevolent side effects in such methods are disallowed. Please let us know your comments on JML, and if you find bugs. See the TODO.txt file in the release for the ones we know about. Thanks to the folks mentioned above and to Joe Kiniry for testing of the pre-release today. See the preliminary design document for other acknowledgments. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From leavens@cs.iastate.edu Wed Nov 13 15:40:57 2002 Date: Wed, 13 Nov 2002 14:49:43 -0600 (CST) From: Gary T. Leavens To: rajeev.joshi@hpl.hp.com Cc: JML Interest List Subject: JML-Interest: Re: Update ESC/Java web page to give link to ESC/Java source release? Hi Rajeev, On Wed, 13 Nov 2002 rajeev.joshi@hpl.hp.com wrote: > > Is it possible you could update the ESC/Java web page to give a direct > > link to where folks can get the source release for ESC/Java? Thanks, > > We added the link this morning. If you follow the "Download" link from > the ESC/Java page (at http://www.research.compaq.com/SRC/esc ), you'll > see the link to the sources, which are available from the Compaq downloads > page. > > Note that the Compaq downloads page contains several links. The third > one (labelled Java Programming Toolkit Source Release) is the one you want. > (Confusingly, the second one is labeled ESC/Java, but that points to the > binary release.) > > Let me know if you have any problems, > > Cheers, > - Rajeev Thanks! -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From erikpoll@cs.kun.nl Thu Nov 28 12:03:19 2002 Date: Thu, 28 Nov 2002 15:59:56 +0100 (CET) From: Erik Poll To: JML Interest List Subject: JML-Interest: "assignable \nothing" vs "assignable \everything" as default Hi all, I'd like to raise the issue of what the best choice for the default assignable clause is. I've discussed this with Gary a few weeks ago, but we're keen to hear what other people think about this. Currently, if a method specification with one of the behavior-keywords, (ie. normal_behavior, behavior, or exceptional_behavior) does not contain an assignable clause, then it gets the default assignable clause assignable \nothing; When writing specs I find this is very inconvenient. I'd rather have assignable \everything; as default. In my experience, writing assignable clauses is one of the trickier aspects of writing JML specs. When writing specs, I _always_ start with just - pre- and postconditions, - invariants, - some pure annotations, so that I can use pure methods in assertions Only at a later stage - if ever! - will I add assignable clauses. I may never get around to adding assignable clauses. After all, if you only want to do runtime assertion checking, you don't really need them anyway. Now if "assignable \everything" were the default, then this approach works well. You can leave out assignable clauses without any problems. But with the current "assignable \nothing" as default, omitting assignable clauses is not an option, as most methods do assign to something. In fact, if the default were "assignable \everything", then people could safely use JML without even knowing that assignable clauses exist! When introducing new users to JML, I would prefer not to say anything about assignable clauses to begin with. I would get them to write pre- and postconditions, and invariants, and pure annotations. I think the biggest "market opportunity" for JML is allowing people to write the odd pre-condition and invariant in their code, and then using the runtime assertion checker. Anyone using JML in this way can completely ignore assignable clauses if the default is "assignable \everything". Other reasons in favor of having "assignable \everything" as default: - It seems to be more in line with the other choices for defaults. Eg. if no precondition is given, this is interpreted as the weakest possible precondition, ie. "true". The same goes for missing ensures and signals clauses. It then seems natural to interpret no assignable clause as the weakest possible assignable clause, ie. assignable \everything. - "assignable \nothing" is a very strong property, and a very desirable one. It seems to me that you would always want to document such a strong property explicitly, not implicitly. - Sometimes you have several behavior specifications for a single method, eg. a private and a public one, or a normal_behavior with the "sensible" precondition and a behavior with precondition true to specify all the exceptions that may be thrown. The current default "assignable \nothing" means that you then have to repeat the assignable clause in each of the behavior specifications, otherwise the method is not allowed to have side-effects under certain circumstances. With "assignable \everything" as default you are free to omit the assignable clause in some of of them. I'd be interested to know other people think about this, and what their experiences with assignable clauses in their JML specs has been. Cheers, Erik From leavens@cs.iastate.edu Fri Nov 29 03:22:39 2002 Date: Thu, 28 Nov 2002 12:47:24 -0600 (CST) From: Gary T. Leavens To: Erik Poll Cc: JML Interest List Subject: Re: JML-Interest: "assignable \nothing" vs "assignable \everything" as default Hi Erik, et al., I fully support this idea of changing the default assignable clause in heavyweight specifications to be, as Erik suggests, assignable \everything; for the reasons he suggests. I just got back from a JML discussion at the KU Leuven, where this topic came up and one of our users, Marko, was suprised at the current default, for precisely these reasons. The others also support it. I think consistency with the lightweight specifications is a big argument in favor of this. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From Michael.Moeller@Informatik.Uni-Oldenburg.DE Fri Nov 29 03:23:55 2002 Date: Fri, 29 Nov 2002 09:58:00 +0100 From: Michael Moeller To: JML Interest List Subject: Re: JML-Interest: "assignable \nothing" vs "assignable \everything" as default Hi, On Thursday 28 November 2002 15:59, Erik Poll wrote: > I'd like to raise the issue of what the best choice for the default > assignable clause is. I've discussed this with Gary a few weeks ago, > but we're keen to hear what other people think about this. > > Currently, if a method specification with one of the behavior-keywords, > (ie. normal_behavior, behavior, or exceptional_behavior) does not > contain an assignable clause, then it gets the default assignable clause > assignable \nothing; > When writing specs I find this is very inconvenient. I'd rather have > assignable \everything; > as default. I like the current default (assignable \nothing;), because it is similar to what Object-Z does with its delta-list. Everything in the delta-list is assignable and with no delta list nothing is assignable. But it would be no problem for me to write explicitly "assignable \nothing;". But I have a question concerning the meaning of the assignable clause in case of specification inheritance: what exactly does "assignable \everything;" mean? Example: public interface I { //@ public model instance int a; /*@ public normal_behavior assignable \everything; ensures a == \old(a) + 1; @*/ public void incA(); } public class C implements I { public int a1; public int a2; //@ public depends a <- a1; //@ public represents a <- a1; public void incA() { a1++; a2++; // is this legal? } } So the question is: Is \everything a short cut for "every accessible field in the current context of the specification" (i.e. a (and a1)) or for "every accessible field in the context where the specification is used" (a1 and a2)? I would prefer the first option so that one can define the semantics of "\everything" by desugaring it. Or is the semantics already set out in writing? Best regards, Michael -- Michael Möller University of Oldenburg, Fachbereich Informatik, P.O.Box 25 03, D-26111 Oldenburg, Germany phone:+49 441 798-3483 fax:+49 441 798-2965 mailto:Michael.Moeller@informatik.uni-oldenburg.de From leavens@cs.iastate.edu Fri Nov 29 03:40:53 2002 Date: Fri, 29 Nov 2002 03:39:46 -0600 (CST) From: Gary T. Leavens To: Michael Moeller Cc: JML Interest List Subject: Re: JML-Interest: "assignable \nothing" vs "assignable \everything" as default Hi Michael, et al., On Fri, 29 Nov 2002, Michael Moeller wrote: > On Thursday 28 November 2002 15:59, Erik Poll wrote: > > I'd like to raise the issue of what the best choice for the default > > assignable clause is. I've discussed this with Gary a few weeks ago, > > but we're keen to hear what other people think about this. > > > > Currently, if a method specification with one of the behavior-keywords, > > (ie. normal_behavior, behavior, or exceptional_behavior) does not > > contain an assignable clause, then it gets the default assignable clause > > assignable \nothing; > > When writing specs I find this is very inconvenient. I'd rather have > > assignable \everything; > > as default. > > I like the current default (assignable \nothing;), because it is similar to > what Object-Z does with its delta-list. Everything in the delta-list is > assignable and with no delta list nothing is assignable. The Larch family of specification langauges also had this default, which is (historically) why this is the default in JML. > But it would be no > problem for me to write explicitly "assignable \nothing;". That's good to hear. I do wonder how difficult it will be for people with existing JML specifications to go through all of their (nonexistent) assignable clauses in their specifications and add assignable \nothing. It may help some that pure methods already have this specification due to the use of "pure". > But I have a question concerning the meaning of the assignable clause in case > of specification inheritance: what exactly does "assignable \everything;" > mean? > > Example: > > public interface I { > //@ public model instance int a; > > /*@ public normal_behavior > assignable \everything; > ensures a == \old(a) + 1; > @*/ > public void incA(); > } > > > public class C implements I { > public int a1; > public int a2; > > //@ public depends a <- a1; > //@ public represents a <- a1; > > public void incA() { > a1++; > a2++; // is this legal? > } > } > > So the question is: Is \everything a short cut for "every accessible field in > the current context of the specification" (i.e. a (and a1)) or for "every > accessible field in the context where the specification is used" (a1 and a2)? > > I would prefer the first option so that one can define the semantics of > "\everything" by desugaring it. > Or is the semantics already set out in writing? The semantics isn't already set out in writing, and you raise a very good point with your question. We need to think about this in the context of our work in the semantis of the assignable/modifies clause in JML. My initial impression is that, if we have something like the context system described in the paper by Mueller and Poetzsch-Heffter and myself, then we would only take \everything to refer to all "relevant" locations in the context of the method. (This has a precise definition in the paper, but it's similar in spirit to waht you wish.) Lacking this context type system, I think we would take the more naive approach (the entire program is one context) and say that \everything refers to all allocated locations. Hence the example you give would be legal. But we should think about it more... It's clear that we need some sort of alias controlling type system in JML soon, which would allow the more sophisticated semantics. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From edwards@cs.vt.edu Mon Dec 2 10:30:48 2002 Date: Mon, 02 Dec 2002 11:26:21 -0500 From: Stephen Edwards To: JML Interest List Subject: Re: JML-Interest: "assignable \nothing" vs "assignable \everything" as default After reading this discussion about assignable clauses, I can sympathize strongly with the comments made about the default, especially when one's primary goal is generating run-time checkable assertions. However, in the interests of a well-balanced discussion ;-), I'm going to throw in a few dissenting comments. Gary T. Leavens wrote: > On Fri, 29 Nov 2002, Michael Moeller wrote: [...] >>I like the current default (assignable \nothing;), because it is similar to >>what Object-Z does with its delta-list. Everything in the delta-list is >>assignable and with no delta list nothing is assignable. > > The Larch family of specification langauges also had this default, > which is (historically) why this is the default in JML. There is a very good reason that Larch and Object-Z (and numerous other formal specification notations) take this approach. In effect, without this choice, it becomes impossible to formally verify any code that omits "assignable" clauses or their equivalent. Consider Gary's statement later in his reply: > Lacking this context type system, I think we would take > the more naive approach (the entire program is one context) and say > that \everything refers to all allocated locations. Now consider this code: int a = 10; Object b = ...; Object c = ...; c.foo(); // <-- consider the post state here ... Let's assume c.foo() has a fairly trivial specification (say, a precondition of "true", a postcondition of "true", and no assignable clause). What can we say about the state of the program after this trivial method has been called? If the default assignable clause is assignable \everything, then a *provably correct* implementation of foo() could still do virtually *anything at all* to *any accessible/allocated location* (assuming Gary's naive solution above, which is the worst-case scenario). From a technical reasoning point of view, one could no longer conclude anything about the values of the variables shown here, since any of them may have been arbitrarily changed inside foo(), all without violating anything in the exceedingly simple specification of foo(). This means that regardless of how one verifies foo(), one would not possibly be able to formally verify any code that used foo() in a modular way. Worse still, technically, one could not even be guaranteed they were reasoning correctly about this client code. The typical "human assumption" when reading this code is that c.foo() presumably affects nothing non-local. However, the default of "assignable \everything" allows something *omitted from the spec* to contradict this basic assumption, which means that valid implementations of foo (according to JML's semantic model) could do very unanticipated things. This doesn't have anything directly to do with run-time assertion checking--instead, it has to do with the semantics of JML and whether or not it is possible to reason about client code modularly, using only local information. The default of "assignable \nothing" gives you the "and nothing else changes" concept and is one thing that prevents frame problems in both formal reasoning and in simple human understanding during code-reading. I agree entirely with Erik Poll when he said: > I think the biggest "market opportunity" for JML is allowing people > to write the odd pre-condition and invariant in their code, and then > using the runtime assertion checker. I also agree with his other comments, including: > In my experience, writing assignable clauses is one of the trickier > aspects of writing JML specs. When writing specs, I _always_ start > with just > - pre- and postconditions, > - invariants, > - some pure annotations, so that I can use pure methods in assertions Unfortunately, there's got to be a way to fix this problem that isn't going to rupture locality of reasoning in the JML semantic model and let frame problems creep back in. I'm not sure about the context system that Gary mentioned in lieu of defining "relevant" locations, but that sounds far more promising than the naive strategy in providing a solid solution to this problem. -- Steve -- Stephen Edwards 604 McBryde Hall Dept. of Computer Science e-mail : edwards@cs.vt.edu U.S. mail: Virginia Tech (VPI&SU) office phone: (540)-231-5723 Blacksburg, VA 24061 ------------------------------------------------------------------------------- From boyland@solomons.cs.uwm.edu Mon Dec 2 14:01:38 2002 Date: Mon, 02 Dec 2002 13:41:40 -0600 From: John Tang Boyland To: JML Interest List Subject: Re: JML-Interest: "assignable \nothing" vs "assignable \everything" as default With regard to assignable clauses: (1) In fluid, we use "writes All" as the default. This means that any reachable updateable state may be modified. This does not make reasoning about the method in a modular way impossible for several reasons: -- some state is unreachable and therefore unmodifiable - local variables of the calling method - unique references (with standard caveats, of course) -- even if state is modifiable, this still does not give the method license to do anything whatsoever: - the types of modifiable variables must be preserved. - unmodifiable things (final fields, etc) are preserved. - invariants must be preserved. (Fluid currently doesn't have invariants; here I'm referring to JMLs "private invariants". I'm not convinced that you can make a useful coherent semantics for other kinds of invariants.) (2) FOOL 2003 will include an interesting paper by Fausto Spoto and Erik Poll that checks assignable clauses. I believe it provides an important negative result that JML people should closely observe: assignable clauses are not (usefully) checkable modularly unless the annotation also says what is assigned to those variables. Consider a simple example: foo() has an assignable clause of this.f (of type A) After calling foo(), the caller does: this.f.g := What should the assignable clause of the caller be ? Given that we don't know what foo() could put into this.f, the best we can do is: assignable this.f, \any(A).g // "\any(A)" means any object of type A. In other words, assignable elements of the form: x.y.z (with an indirection) are hard to prove except for leaf methods. John From cok@frontiernet.net Wed Dec 4 20:23:45 2002 Date: Wed, 04 Dec 2002 21:22:49 -0500 From: David To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: runtime assertion checks in the absence of java files (Sorry if you see this twice - the first accidentally went to the sourceforge list) The runtime assertion checker that is part of the JML suite of tools works as follows: given a class implementation in a .java file, with JML annotations, a method m( ) is rewritten so that the original method is now called internal$m, and a new method m is written that checks the validity of invariants and pre- and post-conditions, calling internal$m to do the actual work of the method. This works when the original .java file is available and can be rewritten before being compiled into .class file that masquerades as the compiled representation of the original .java file. But consider the situation in which there is no .java file. We then have a .class file (in a library most likely), and some file, such as a .spec or .jml file, in which JML annotations are given. It is still relevant and important to be able to test the operation of the library against the specifications. In fact it may be even more important than when the source code is available for inspection. In the absence of source code (and absolutely thorough and correct documentation), the user of the library must make assumptions about the behavior of the library that cannot be checked by inspection of the source. Those assumptions can be expressed as JML specifications. Since the code that uses the library will be correct only if the assumptions are valid, it is important to be able to test that the specs match the behavior of the supplied compiled code. The current implementation of the runtime assertion code generator does not work for the case of no source code. There are some architectural hurdles. Note first that when source code is available, an original method m is renamed internal$m and a new method incorporating assertion checking is created. That way code that calls method m can operate unchanged. When source code is not available, the new wrapper method m need only call the method m resident in the compiled code. There is no necessity for internal$m. However, we then have the difficulty that there are two methods with the same name in the same class in the same package. But if the package, class or method name are the same, then either (a) the original .class file will always be found by the standard class loader, or (b) the new .class file will be found, and its methods will call themselves recursively. If the generated class is generated using a different class or method name, then all code that interacts with the class under test will need to be modified. If the package name is different, then at minimum the import statements in code interacting with the class under test will need to be modified. One way around this problem is simply to punt. Instead of building the assertion checks into a revised version of the original class, build them into the test framework instead. This would allow the class under test to be tested in isolation, but would not identify problems in vivo either within an application that uses the class under test or during interactions between classes in the library under test. This approach does not accomplish the overall goals. A better solution requires cooperation of a modified class loader. We want all code but the generated revised code of the class under test to utilize that generated revised code for any instances of the class being tested. However, we want the generated revised code to call the original library code for its internal calls. The class loader needs to identify those method invocations (easy enough), but then must load the original class in a modified form so that it is distinguished from the generated class. Any reflections on the wisdom or possibility of this sketch of a solution are welcome. - David From leavens@cs.iastate.edu Wed Dec 4 20:58:39 2002 Date: Wed, 4 Dec 2002 20:57:23 -0600 (CST) From: Gary T. Leavens To: Stephen Edwards Cc: JML Interest List Subject: Re: JML-Interest: "assignable \nothing" vs "assignable \everything" as default Steve, et al., On Mon, 2 Dec 2002, Stephen Edwards wrote: > After reading this discussion about assignable clauses, I can > sympathize strongly with the comments made about the default, > especially when one's primary goal is generating run-time checkable > assertions. However, in the interests of a well-balanced > discussion ;-), I'm going to throw in a few dissenting comments. I appreciate the careful consideration of the design issues; thanks. > Gary T. Leavens wrote: > > > On Fri, 29 Nov 2002, Michael Moeller wrote: > [...] > >>I like the current default (assignable \nothing;), because it is similar to > >>what Object-Z does with its delta-list. Everything in the delta-list is > >>assignable and with no delta list nothing is assignable. > > > > The Larch family of specification langauges also had this default, > > which is (historically) why this is the default in JML. > > There is a very good reason that Larch and Object-Z (and numerous > other formal specification notations) take this approach. In effect, > without this choice, it becomes impossible to formally verify any > code that omits "assignable" clauses or their equivalent. Yes, it's true that when the default is \everything, then "it becomes impossible to formally verify any code that omits "assignable" clauses or their equivalent." But that's precisely the point; if the user hasn't told JML what their frame is, we should be wary of allowing them to do useful verifiction by assuming that it's \nothing. I think this boils down to whether we optimize to make it easier to read or to write a JML specification. My philosophy is to always make it easier to read the specification, and if that makes it harder to write, so be it. The change in default would certainly make it harder to write specifications, because to be useful for verification, you must write an explicit frame. But that seems okay, because we want the reader to always see when the method cannot assign anything. I think the proof of the pudding will be in trying this out. We'll have to go through a bunch of specifications and see how bad it is to use the default of \everything. (The only trouble is that it's hard to find the method specifications that do *not* use an assignable clause.) As an example of the effects of this change, here's the current version of IntegerSetInterface... package org.jmlspecs.samples.sets; //@ model import org.jmlspecs.models.*; /** Sets of integers. */ public interface IntegerSetInterface { /*@ public model instance JMLValueSet theSet @ initially theSet != null && theSet.isEmpty(); @ public instance invariant theSet != null @ && (\forall JMLType e; theSet.has(e); @ e instanceof JMLInteger); @*/ /** Insert the given integer into this set. */ /*@ public normal_behavior @ assignable theSet; @ ensures theSet.equals(\old(theSet.insert(new JMLInteger(elem)))); @*/ public void insert(int elem); /** Tell if the argument is in this set. */ /*@ public normal_behavior @ ensures \result == theSet.has(new JMLInteger(elem)); @*/ public /*@ pure @*/ boolean isMember(int elem); /** Remove the given integer from this set. */ /*@ public normal_behavior @ assignable theSet; @ ensures theSet.equals( \old(theSet.remove(new JMLInteger(elem))) ); @*/ public void remove(int elem); } If we change the default, we would only change the specification of isMember to be: /** Tell if the argument is in this set. */ /*@ public normal_behavior @ assignable \nothing; @ ensures \result == theSet.has(new JMLInteger(elem)); @*/ public /*@ pure @*/ boolean isMember(int elem); Even this isn't technically necessary because the modifier "pure" implies that the method modifies nothing, but I think it would be clearer this way. The other methods already have assignable clauses, so they are unchanged. Steve, I think you get carried away with your example when you say... > Unfortunately, there's got to be a way to fix this problem that isn't > going to rupture locality of reasoning in the JML semantic model and > let frame problems creep back in. It's not true that the change of default would change locality of reasoning. It only changes the default. People can still write all of the old specifications they could write before, they just have to express them differently. That is, if there is a problem with the semantics of \everything (and I think there is), it's already in JML with the default assignable clause of \nothing. The change of default just means that we had better clarify what \everything means because \everything will be more important. In other words, once you fill in the default, you get a specification that is either useful for verification or it isn't; but the particular choice of default has nothing to do with the utility of the specification that results, because the user can always avoid the default by writing the frame explicitly. Other objections? If not, I'm leaning heavily towards changing the default (after we get a chance to look at many examples). An additional argument comes from my visit to Leuven last week. The people there want to do design by contract and runtime checking, as in Eiffel. They don't want to write assignable clauses. So they really do want the default to be assignable \everything so that they can ignore the assignable clause. Meshing with lightweight specifications is certainly better supported this way. I think that the support from Boyland and his langauge, which has the equivalent of "assignable \everything" as the default, is another indication that this is the right way to go. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From erikpoll@cs.kun.nl Thu Dec 5 08:16:25 2002 Date: Thu, 5 Dec 2002 13:04:02 +0100 (CET) From: Erik Poll To: JML Interest List Cc: David Subject: Re: JML-Interest: refinement and JML tools Hi David, Most of your ideas for the rules for refine make excellent sense to me - esp. your decision to make things more restrictive if it makes things simpler ! Below detailed comments, plus some general remarks on how I have been making use of refines clauses so far. > I've been guided by these use cases in thinking about this. Most of the use cases you mention are ones that I have experienced. The use cases I have NOT come across are > c) It will sometimes be necessary to create files to refine further > [...] specification files [...] > f) It will sometimes be desirable to create refining specifications for > a spec that already exists (and that the specifier chooses not to > alter) [...] So far, my main reasons for using refining files have been 1) to write specs without editing the java sources (other than adding a single "refines" clause to point to the spec), ie. your use case (b). Eg if I write a jml spec for an API class A.java that someone else controls, I'd prefer to write the jml spec in a separate file A.jml and just add //@ refine A <- "A.jml" in A.java when I want to do say runtime assertion checking. Whenever there's a new release of A.java - or someone else comes up with an alternative implementation - all I have to do is add the same refine clause in this A.java file. 2) to separate implementation and (public) specification: When adding jml specs in the source code file, it may be convenient to move the public spec to a separate file, so that it is not cluttered by all the code and implementation-dependent jml specs such as private invariants. So far, I only ever used refinement sequences of length 2, ie. just consisting of a java source file and a jml spec file. Note that that I do not mind very strong restrictions on consistency between different refinements, since I never have more than one refinement anyway :-) I don't know how typical this is. Have other people really made use of longer refinement sequences ? > Use cases (f) and (g) might imply that we need two modes of checking - a > there is not necessarily a declaration of each of the non-model fields, > methods or classes that appear in the specification files) and a > full-checking mode in which all such declarations are required. I would > suggest that the full-checking mode be the default, with the prototype > mode being an option. Maybe it's not better to bother the prototype mode ? That keeps things simpler and I think most people could live without it. (I could.) > class/interface name: > [...] > Any jml modifiers (e.g. pure) must appear in a CU if they are present in > a less refined CU. To allow your use case (b) (writing jml specs without touching the java sources) or my (1) above, I think that it should be possible to omit jml modifiers in the .java file. So I think this policy should only apply to non-java refinement files, but not to the .java file - if there is one. > All CUs in the refinement sequence that contain a type declaration must > specify the same superclass and the same set of interfaces. > Question: Is that too restrictive? No, I don't think this is too restrictive. > A JML modifier applicable to a method (spec_public, spec_protected, > pure, non_null, helper) must appear in a method spec if it appears in > the spec of that method's declaration in a less refined CU. Again, to allow use case (b), I think that it should be possible to omit JML modifiers in the .java file. > The jml modifiers model, ghost, instance must be used consistently > across all CUs in a RS, wherever the declaration of the field occurs. > > Other jml modifiers (non_null, spec_public, spec_protected, pure, > monitored, uninitialized) - if any of these specifications appears in a > CU, it must appear in any more refined CU (including a .java file?) Again, to allow use case (b), I think that it should be possible to omit JML modifiers in the .java file. > If a parameter is declared non_null in a CU, it must be declared > non_null in any more refined CU (including a .java file?). Again, I'd say excluding the .java file. > Overall question: I've stated that the java modifiers for syntactic > elements have to be consistent across CUs in a RS. Will that cause too > much of a nuisance in editing? I think this is a good policy, for the reason you mention -- clarity. Cheers, Erik On Tue, 26 Nov 2002, David wrote: > This note describes suggestions for a design of the behavior of JML > tools in the presence of refinement as JML provides it. Though I am > prompted by my desire to upgrade jmldoc, now that refine clauses are > functional within the checker, I expect the rules would be implemented > within the checker itself and would apply consistently across all JML > tools. It is a work in progress, obviously - very much of a draft - I'd > appreciate your feedback (and there are questions called out in the > discussion, as well as points that I have not thought through as yet). > Plus, I don't expect to be implementing all of it. I'll be happy to be > pointed to references on this topic - they don't seem to be plentiful. > [If this has all been defined elsewhere, someone may stuff a virtual > sock in my mouth and tell me where to find the information.] > > - David > > There are multiple files in a sequence of refining files. They can > contain redundant information. Thus we need some rules to say what is > required to be repeated between files, what may be repeated, and what is > forbidden to repeat. > > I've been guided by these use cases in thinking about this. > a) Sometimes one will add specifications directly to a .java file > containing an implementation (no refinement files necessary). > b) It will sometimes be necessary to create files to provide > specifications for (i.e. to refine) .java files that contain no > specifications and that are not editable by the specifier (or the > specifier chooses not to edit). > c) It will sometimes be necessary to create files to refine further > either specification files or .java files that already contain some > specifications. > d) It will sometimes be necessary to create (and check) specifications > for classes that only exist in .class form. > e) It will sometimes be desirable to create (and check and document) > specifications prior to creating any implementation in a .java file, or > while the implementation is in progress. > f) It will sometimes be desirable to create refining specifications for > a spec that already exists (and that the specifier chooses not to > alter), prior to or while an implementation in a .java file is being > created. > g) It will be necessary to be able to thoroughly check that all the > specification files (and implementation) are completely consistent, when > > the specifier believes the specification and the implementation are both > complete. > > Also > h) make rules more restrictive if that aids simplicity and see if you > can live with it > i) the rules should match, in so far as possible, an experienced Java > programmer's intuition without the programmer having to be told the > rule. > j) One ought to be able to specify, implement, and check incrementally > k) Avoid making the program writer replicate stuff, but it is more > important to achieve clarity for the reader > > Use cases (f) and (g) might imply that we need two modes of checking - a > prototype mode in which an incomplete .java file is allowed (that is > there is not necessarily a declaration of each of the non-model fields, > methods or classes that appear in the specification files) and a > full-checking mode in which all such declarations are required. I would > suggest that the full-checking mode be the default, with the prototype > mode being an option. > > > The refine clauses in JML specifications define a sequence of refinement > files (or, strictly speaking, compilation units). For example, if (not > worrying about which suffixes are valid for the moment) > > X.a contains //@ refine X <- "X.b"; > X.b contains //@ refine X <- "X.java"; > X.java contains //@ refine X <- "X.y"; > X.y contains //@ refine X <- "X.z"; > X.z does not contain a refine clause. > > then the sequence X.a, X.b, X.java, X.x, X.y is a sequence of > refinements from most refined to least refined. A refinement sequence > (RS) may or may not contain a .java file. > > Note - a compilation unit (CU) may contain at most one refine clause. > So it may refine only one directly less refined compilation unit, if > any. > > Question: is it allowed to have two different files Z.a and Z.b that > both (directly refine) a third Z.c ? That is, both Z.a and Z.b contain > //@ refine Z <- "Z.c";. This seems ok, possibly useful, if potentially > confusing, except if tools go looking for most-refined files. I suggest > that for the moment we call it an error, if we have any behavior in > which the file system is searched for most-refined files. > > Now we will consider the various syntactic elements of these files and > propose in what ways they must be consistent or redundant among the > compilation units of a refinement sequence. > > class/interface name: > > The public class/interface name in a compilation unit must be identical > in all CUs of the refinement sequence, and there must be a declaration > of that class/interface appropriate to the suffix of the file it is in. > Any java modifiers of the public class/interface definition must be > identical in all CUs of the RS. > Any jml modifiers (e.g. pure) must appear in a CU if they are present in > a less refined CU. > > Non-public top-level class and interface declarations are not required > to be replicated in every CU, but otherwise follow the same rules as the > public declaration. This is the same policy as for inner classes below. > > > > > file name: > > The prefixes (portion before the last '.') of the names of files of the > refinement sequence must all be identical and must all match the name of > the class, as defined by the java language and the platform/file system. > > There are restrictions (defined elsewhere) on what suffixes are allowed > in a RS and which orders of suffixes are allowed in a RS. > > > package statement: > > The package statement must be present and must name the same package in > all of the CUs of the RS. > > > import statements: > > There are no restrictions on import statements across CUs. Each CU can > include the appropriate import statements in order to interpret > correctly the various names and identifiers used in that CU. > > > superclass and interfaces: > > All CUs in the refinement sequence that contain a type declaration must > specify the same superclass and the same set of interfaces. > Question: Is that too restrictive? Are there situations in which that > level of implementation detail need not be reflected in the > specification file? > Question: what about 'weakly' designations? > > > class level javadoc comments: > > Suggestion: Javadoc comments are not combined. A tool that processes > javadocs need only use the class-level javadoc comments from the most > refined CU in the RS that has non-empty class-level javadoc comments. > > Rationale: The semantics of combination may be messy. One can always > replicate if one wants to add to what is there. It could be possible > later to define some syntax that optionally indicates to combine a > javadoc comment with javadoc comments in less refined files, if one can > define how that combination is to occur. > > > > method/constructor level javadoc comments: > > Corresponding rules as for class-level javadoc comments > > > java (non-model, non-ghost) field declarations > > Any field that is to be used in the implementation must be declared in > the .java file. > A field declaration may be replicated in a (non-java) refinement file in > > order to provide a specification for that field or to declare the name > so that specification clauses can refer to it. > If a field is declared in a non-java refinement file, it must have the > same identifier, the same type, and the same java modifiers (that is, > identifiers may not be reused with different types in refining files). > If an identifier is redeclared it refers to the same field. > A field does not need to be redeclared in a refining file, even if it is > > used in a specification in the refining file; that is a field in a > refined file is equivalent to a locally declared field in any of its > refining files. > > > > Model or ghost field declarations: > > The same rules apply as to non-model, non-ghost field declarations, > except that model and ghost fields are not required to be declared in > the .java file. > In addition, a model or ghost field may not have the same identifier as > a java field defined anywhere in the refinement sequence. > > > Question: How do we interpret an identifier which has a non-private > declaration in a superclass or interface as well as in a less refined CU > in the RS? I think this has been answered already in email exchanges, > though I do not have the reference. In order to have no surprises in > interpreting the specifications from either a java context or a jml > context, it has to be illegal to declare a model or ghost field or > method in a specification file with no corresponding declaration in the > ..java file, but for which there is a non-private java declaration of > that identifier in a super class or interface. > > > > Methods (and equivalently for constructors): > > In non-prototype mode, all non-model method declarations must have a > declaration and implementation (if they are not abstract) in the .java > file, if it exists (and in a class file if it does not). > Method declarations may be replicated in non-.java specification files, > but they must have the same return value and the same java modifiers (if > the identifier or the argument types are different, it is a different > method). The formal parameter names need not be the same from one CU to > another. It is the formal parameter names in a given CU that are used > to interpret the specifications for that method in that CU. > Only the .java or .class file may provide an implementation for a method > > or constructor. > > > Model methods (and model constructors): > > The same rules apply as for non-model methods and non-model > constructors, except that these never have an implementation. > > It is not permitted to have a model method or model constructor with the > same parameter signature as a non-model method or non-model constructor > in the same class in any CU of the refinement sequence (nor may it match > any non-private non-model method in a superclass or superinterface). > > Question: How does inheritance work for model methods in the presence of > refinement? > > > Class-level specifications: > > Class level specifications need not be replicated across the CUs. It is > not an error to do so, but the point of the refinement seqeuence is to > add additional specifications. > > The complete class-level specification of the class (or interface) is > the union of all the specifications for that class across the entire RS. > > > > > Method and constructor specifications: > > Method level specifications need not be replicated across the CUs. It > is not an error to do so, but the point of the refinement seqeuence is > to add additional specifications. > > A JML modifier applicable to a method (spec_public, spec_protected, > pure, non_null, helper) must appear in a method spec if it appears in > the spec of that method's declaration in a less refined CU. > > The complete specification of the method is the concatentation of all > the specifications for that method across the entire RS, as if they were > in one CU connected by 'also' connectors, with appropriate renaming of > the formal parameter names. [I guess we have to talk about reordering > the spec-case-seq, subclassing-contract, implications, and examples > sections. It would be easire if just connecting them all with 'also' > was legitimate syntax.]. If the method overrides a method in a super > class or interface, each non-empty specification for a declaration of > that method in any CU of the RS must begin with 'also'. If the method > does not override, then each non-empty method specification must begin > with 'also', except the specification in the least refined CU to contain > a declaration of that method with a non-empty specification (which must > not begin with 'also'). > > > > Field specifications: > > The jml modifiers model, ghost, instance must be used consistently > across all CUs in a RS, wherever the declaration of the field occurs. > > Other jml modifiers (non_null, spec_public, spec_protected, pure, > monitored, uninitialized) - if any of these specifications appears in a > CU, it must appear in any more refined CU (including a .java file?) > > initially, readable_if phrases - these need not be replicated; the full > specification is the boolean AND of all the corresponding phrases across > > the RS > > monitored, monitored_by - TBD > > > > > Parameter modifier (non_null): > > If a parameter is declared non_null in a CU, it must be declared > non_null in any more refined CU (including a .java file?). > > > > > > Inner classes > > An Inner class/interface declaration need not be replicated in all CUs. > But when it is replicated, the same rules apply as for the top-level > classes. > > > Overall question: I've stated that the java modifiers for syntactic > elements have to be consistent across CUs in a RS. Will that cause too > much of a nuisance in editing? In favor of this rule is clarity. An > alternative would be to have no modifiers in specification files - but > that seems to be a non-starter since current practice already has such > modifiers, there may not be a .java file from which to determine the > modifiers, and it would mean always having to check the .java file to > remember the modifers when editing a specification file. > From david.cok@kodak.com Thu Dec 5 09:37:21 2002 Date: Thu, 5 Dec 2002 09:00:32 -0500 From: david.cok@kodak.com To: erikpoll@cs.kun.nl, jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: refinement and JML tools Eric, Thanks much for your comments - and taking the time to share them. I have one question based on your experience report. You write:    Eg if I write a jml spec for an API class A.java that someone else   controls,  I'd prefer to write the jml spec in a separate file A.jml    and just add     //@ refine A <- "A.jml"   in A.java when I want to do say runtime assertion checking.   Whenever there's a new release of A.java - or someone else comes up   with an alternative implementation - all I have to do is add the   same refine clause in this A.java file. You could use this alternative:  put the specifications in A.refines-java , including in that file the statement '//@ refine A<-"A.java'.  Then you don't ever need to modify the .java file, and don't even need write-permission (and perhaps eventually not need the source at all).  Is there a reason that that does not work or is not preferable in your situation? - David From leavens@cs.iastate.edu Thu Dec 5 09:55:37 2002 Date: Thu, 5 Dec 2002 09:51:59 -0600 (CST) From: Gary T. Leavens To: JML Interest List Subject: JML-Interest: Please sign up for the jmlspecs-interest mailing list on SourceForge Hi all, JML is in the process of moving to sourceforge.net, which is already hosting the MultiJava langauge development efforts. If you are a subscriber to this jml-interest-list, you should sign up for the new version of this list, which we will start using shortly, at least by the beginning of the next calendar year. To do this, you should go to http://lists.sourceforge.net/lists/listinfo/jmlspecs-interest and fill in the information needed to subscribe to the list jmlspecs-interest. This will be the replacement for the jml-interest mailing list. As a bonus, the sourceforge version offers you some new features, such as batching of messages. We plan to keep essentially the same charter for this list. Note that only subscribers will be able to post to it. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From edwards@cs.vt.edu Thu Dec 5 10:39:01 2002 Date: Thu, 05 Dec 2002 11:24:55 -0500 From: Stephen Edwards To: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: runtime assertion checks in the absence of java files David wrote: > But consider the situation in which there is no .java file. [...] > There are some architectural hurdles. Yes, big ones ;-). > A better solution requires cooperation of a modified class loader. [...] > Any reflections on the wisdom or possibility of this sketch of a > solution are welcome. It is interesting that you bring this up. Together with Gary Leavens and Murali Sitaraman, we've been working on *exactly* such a revised approach to delivering JML run-time assertions. The key idea is to separate the run-time checks into a separate wrapper class, and then use a modified class loader to conditionally "graft" this wrapper into the inheritance hierarchy at run-time (and make some minor changes to other class files as they are loaded to make it all fit together). We've already constructed a prototype of the class loader and some run-time checking wrappers. Best of all, JML's current assertion generation code looks like it can be modified to generate checks in this alternate form without having to rebuild the generation engine entirely. One of the advantages of this is that if you can write a JML behavioral description for an existing library of .class files, you can generate stand-alone run-time checks and use them without requiring that library-- or any of the client code!--to be recompiled. We've even figured out a sneaky way to do this with java.util classes, and will be running a performance experiment to characterize the overhead of this approach using a collection of 10 java.util classes during the spring. Further, an added benefit is that simply by changing the command you use to start up the program (say, using "java" instead of "jmlrac"), all the assertion-checking code disappears entirely. No extra memory footprint. No extra code. No cost for testing to see if checks are enabled at run-time. No recompilation. Yes, that means you could conceivably write a JML spec for Vector, say. Then generate assertion checks from this description without recompiling Vector. Then you could run a previously existing program that used Vectors (without recompiling either that client or the Vector implementation) and choose whether or not to transparently insert run-time checks into it at program startup. Once all the kinks have been shaken out, my hope is that we can get this approach integrated into a future version of JML, and Gary has expressed a similar intent. -- Steve -- Stephen Edwards 604 McBryde Hall Dept. of Computer Science e-mail : edwards@cs.vt.edu U.S. mail: Virginia Tech (VPI&SU) office phone: (540)-231-5723 Blacksburg, VA 24061-0106 ------------------------------------------------------------------------------- From edwards@cs.vt.edu Thu Dec 5 17:23:01 2002 Date: Thu, 05 Dec 2002 15:36:52 -0500 From: Stephen Edwards To: JML Interest List Subject: Re: JML-Interest: "assignable \nothing" vs "assignable \everything" as default Gary T. Leavens wrote: > But that's precisely the point; if the user hasn't told JML what > their frame is, we should be wary of allowing them to do useful > verifiction by assuming that it's \nothing. OK, now things are looking a little fuzzier. I suppose by this you mean you are taking the omission of an assignable clause to be a kind of incomplete/partial specification that, if used, would no longer allow formal verification. OK, but ... > I think this boils down to whether we optimize to make it easier to > read or to write a JML specification. I agree with this in principle, but disagree with your conclusion that this change in default makes it easier to *read* specifications. In particular, all the arguments that Erik put forward were motivated by the additional effort needed to *write* assignable clauses, which he wanted to conveniently omit. I can understand that omitting them makes the job of writing specs easier, particularly if your goal is to generate run-time checkable assertions (which aren't really affected by assignable). > My philosophy is to always make > it easier to read the specification, and if that makes it harder to > write, so be it. OK, so here is the critical problem. From your first statement, it is clear that a developer who omits assignable clauses is not defining the frame. However, a reader trying to understand that partial specification is naturally going to form his own frame mentally when reading the partial specification. That's just the way people are (and it is the source of many errors in human perception). The reader is going to implicitly build a frame that (in general) contains the items that are explicitly mentioned in the spec. In practice, for most well-behaved methods, that should be approximately correct. However, if JML's *semantic definition* actually *defines* a default frame in such a case that encompasses much more than the reader's naive version (i.e., the "whole program" in the worst case scenario), then almost certainly, a human reader is going to *routinely* build up a mental understanding of such a method that conflicts with the actual meaning of the specification in JML's semantic model. In my mind, that is a readability problem. It means that "partial specs" that omit assignable clauses are likely to be read informally in a way that is contradictory to the JML semantic model. Now, in practice, we know that virtually all methods where the assignable clause is omitted are not going to cause "random changes" elsewhere in the program, and this disconnect between what the spec would permit and what the code actually *does* would more than likely prevent any technically incorrect "misreadings" of the partial spec from causing any practical problems. > But that seems okay, because we > want the reader to always see when the method cannot assign anything. No--this is the "natural" assumption that people normally make. What we want is for them to *always* see when something can make arbitrarily far-reaching changes to the program state, including changes to objects not explicitly mentioned in the signature of the method. That is *definitely* something that should be explicit to the reader rather than hidden. This gets back to the statement I made at the end of my last message about "there's got to be a way to fix this problem." I'm not suggesting that one leave the default the way it is--instead, I'm suggesting that the default should be something that matches the reader's perceptions in the absence of an assignable clause (i.e., the scope of effects is limited to the receiver of the message and the parameters, or state reachable from these points). It sounds like you're really intending to head in that direction anyway, which is great. > Steve, I think you get carried away with your example when you say... > >>Unfortunately, there's got to be a way to fix this problem that isn't >>going to rupture locality of reasoning in the JML semantic model and >>let frame problems creep back in. > > > It's not true that the change of default would change locality of > reasoning. OK, what I meant to say was that, if \everything means everything allocated/addressable in the program (which you opened as a possibility), then this default would prevent one from using JML's semantic model to locally reason about the effects of an operation without an assignable clause. > People can still write all > of the old specifications they could write before, they just have to > express them differently. Sure. What I meant was that, if one omits assignable clauses-- and Erik's comments argue toward a practice where *most* people start off omitting them (and probably continue the practice until, if ever, they get interested in formal verification)--then such specs do not support local reasoning. Currently, such JML specs do support local reasoning even when they omit the assignable clause. I wasn't complaining that it would make JML less expressive or less complete. > Meshing with lightweight specifications > is certainly better supported this way. I agree that is the correct thing to do. I agree that assignable clauses should be "optional" in a clean way. However, for JML's semantic model, I think it all boils down to producing an effective definition of \everything that doesn't include "everything" ;-). Like I said, it sounds like that is what you intend to capture, so I'll wait until you do. I'm sure it will not have the limitations of allowing \everything to be a "program-wide" context. -- Steve -- Stephen Edwards 604 McBryde Hall Dept. of Computer Science e-mail : edwards@cs.vt.edu U.S. mail: Virginia Tech (VPI&SU) office phone: (540)-231-5723 Blacksburg, VA 24061 ------------------------------------------------------------------------------- From leavens@cs.iastate.edu Fri Dec 6 17:50:52 2002 Date: Fri, 6 Dec 2002 17:50:00 -0600 (CST) From: Gary T. Leavens To: Stephen Edwards Cc: JML Interest List Subject: Re: JML-Interest: "assignable \nothing" vs "assignable \everything" as default Hi Steve, et al., Thanks again, Steve, for your careful considerations... On Thu, 5 Dec 2002, Stephen Edwards wrote: > Gary T. Leavens wrote: > > But that's precisely the point; if the user hasn't told JML what > > their frame is, we should be wary of allowing them to do useful > > verifiction by assuming that it's \nothing. > > OK, now things are looking a little fuzzier. I suppose by this > you mean you are taking the omission of an assignable clause to > be a kind of incomplete/partial specification that, if used, would > no longer allow formal verification. OK, but ... > > > I think this boils down to whether we optimize to make it easier to > > read or to write a JML specification. > > I agree with this in principle, but disagree with your conclusion > that this change in default makes it easier to *read* specifications. > > In particular, all the arguments that Erik put forward were motivated > by the additional effort needed to *write* assignable clauses, which > he wanted to conveniently omit. I can understand that omitting > them makes the job of writing specs easier, particularly if your > goal is to generate run-time checkable assertions (which aren't > really affected by assignable). Yes, Erik did make that argument. But I meant that the specifications with explicit assignable clauses are easier to read than those without, and this goes back to Erik's argument that assignable \nothing is such a strong specification that you want to see it when it is required. I think we may also be looking at the specification from different viewpoints (client vs. implementer). > > My philosophy is to always make > > it easier to read the specification, and if that makes it harder to > > write, so be it. > > OK, so here is the critical problem. From your first statement, it > is clear that a developer who omits assignable clauses is not defining > the frame. I wasn't saying that exactly, although Erik was. > However, a reader trying to understand that partial > specification is naturally going to form his own frame mentally > when reading the partial specification. That's just the way people > are (and it is the source of many errors in human perception). Agreed. > The reader is going to implicitly build a frame that (in general) > contains the items that are explicitly mentioned in the spec. > In practice, for most well-behaved methods, that should be > approximately correct. > > However, if JML's *semantic definition* actually *defines* a > default frame in such a case that encompasses much more than the > reader's naive version (i.e., the "whole program" in the worst > case scenario), then almost certainly, a human reader is going > to *routinely* build up a mental understanding of such a method > that conflicts with the actual meaning of the specification in > JML's semantic model. Yes, that will be a problem, although it's perhaps better than the problem with assignable \nothing as the default. I asked one of the undergraduates working with me, Katie Becker, who has written some JML specifications and worked all semester on this, what she thought it meant when you omit the assignable clause (in a heavyweight specification). She said it means that the specification allows anything to be assigned to. I agree she may have been thinking of the fields of the particular class instead of "everything" in the grand sense, but she was very surprised when I told her it meant "assignable \nothing;". I've had similar experiences with other students. > In my mind, that is a readability problem. It means that > "partial specs" that omit assignable clauses are likely to be > read informally in a way that is contradictory to the JML > semantic model. I agree that's a readability problem, but I think the change in default makes it a smaller problem than currently for some specifications than it was before (although still a problem). See above. > Now, in practice, we know that virtually all methods where > the assignable clause is omitted are not going to cause > "random changes" elsewhere in the program, and this disconnect > between what the spec would permit and what the code actually > *does* would more than likely prevent any technically incorrect > "misreadings" of the partial spec from causing any practical > problems. > > > But that seems okay, because we > > want the reader to always see when the method cannot assign anything. > > No--this is the "natural" assumption that people normally make. That is certainly an educational problem, but I'm not sure which is "natural" to a human with no preconceptions in this area. > What we want is for them to *always* see when something can make > arbitrarily far-reaching changes to the program state, including > changes to objects not explicitly mentioned in the signature of > the method. That is *definitely* something that should be > explicit to the reader rather than hidden. I agree with that too, but the disadvantages outlined by Erik seem to outweigh this. I would say that if someone really intends to say that a method is chaotic like this, then it would be quite bad to hide that in the default. But I think as a default \everything corresponds better to the intuition that "I didn't say what it could assign" than does \nothing, since \everything is a superset of whatever they could actually assign. > This gets back to the statement I made at the end of my > last message about "there's got to be a way to fix this > problem." I'm not suggesting that one leave the default > the way it is--instead, I'm suggesting that the default > should be something that matches the reader's perceptions > in the absence of an assignable clause (i.e., the scope > of effects is limited to the receiver of the message and > the parameters, or state reachable from these points). > > It sounds like you're really intending to head in that > direction anyway, which is great. Yes, we are. I think JML desperately needs a context-limiting type system and semantics for modifies/assignable clauses like that Mueller and Poetzsch-Heffter pioneered. But I'd like to take this step first and that step (which is more complex and harder to implement) second. > OK, what I meant to say was that, if \everything means everything > allocated/addressable in the program (which you opened as a > possibility), then this default would prevent one from using > JML's semantic model to locally reason about the effects of an > operation without an assignable clause. > > > People can still write all > > of the old specifications they could write before, they just have to > > express them differently. > > Sure. What I meant was that, if one omits assignable clauses-- > and Erik's comments argue toward a practice where *most* people > start off omitting them (and probably continue the practice > until, if ever, they get interested in formal verification)--then > such specs do not support local reasoning. Yes, I agree with all of that. It's true for methods that don't write an assignable clause. So if you want to do formal verification, you have to write assignable clauses in the specifications. I agree the default affects this: if you don't write them in the \nothing default we currently have, then you get incorrect implementations, but if you don't write them in the \everything default, you get specifications that aren't useful in proofs. The exact effect of these defaults is something I hadn't thought about in exactly this way before. But perhaps it can be remedied by a compiler "caution" message (like a warning that isn't filtered out). If we change to \everything as the default, then perhaps we should have a flag in JML that gives a caution whenever you check specifications without a modifies/assignable clause. The warning would only have to be given for methods that are not pure, since a pure method has an implicit assignable clause. This would be useful for instructors in courses as well as verifiers, but would be left off by people doing runtime checking. > > Meshing with lightweight specifications > > is certainly better supported this way. > > I agree that is the correct thing to do. I agree that assignable > clauses should be "optional" in a clean way. However, for JML's > semantic model, I think it all boils down to producing an effective > definition of \everything that doesn't include "everything" ;-). I agree with that. Boyland's point about some storage never being assignable is part of this, and contexts a la Mueller are another part. > Like I said, it sounds like that is what you intend to capture, so > I'll wait until you do. I'm sure it will not have the limitations > of allowing \everything to be a "program-wide" context. Yes, I think that's right. Thanks again, Other comments? -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From Jan.Dockx@cs.kuleuven.ac.be Sun Dec 8 10:09:40 2002 Date: Sun, 8 Dec 2002 15:56:54 +0100 From: Jan Dockx To: jml-interest-list@cs.iastate.edu Subject: Fwd: JML-Interest: "assignable \nothing" vs "assignable \everything" as default Maybe the default should be: @const \everything_which_is_not_statically_reachable_from_here i.e., the transitive closure of all locations reachable from the static type of the arguments of the method (including the implicit prime argument). The difference with @assignable \anything (as I understand it) being that you now do have positive information about the things the method cannot know about, and you do not have any information about the things the method can reach. If you want to keep your reasoning monotonic, you should not depend on one of those latter things either being modifiable or const. In practice this means that you should not try to prove that another method using the former indeed does keep some things const, for you do not have enough (stable) information for that. And that is exactly what Garry is aiming at, as I understand it: validation without taking modifiability into account, probably as a starting point for use by students, and maybe as a starting point in any design. Begin forwarded message: > Hi Steve, et al., > > Thanks again, Steve, for your careful considerations... > > On Thu, 5 Dec 2002, Stephen Edwards wrote: > >> Gary T. Leavens wrote: >>> But that's precisely the point; if the user hasn't told JML what >>> their frame is, we should be wary of allowing them to do useful >>> verifiction by assuming that it's \nothing. >> >> OK, now things are looking a little fuzzier. I suppose by this >> you mean you are taking the omission of an assignable clause to >> be a kind of incomplete/partial specification that, if used, would >> no longer allow formal verification. OK, but ... >> >>> I think this boils down to whether we optimize to make it easier to >>> read or to write a JML specification. >> >> I agree with this in principle, but disagree with your conclusion >> that this change in default makes it easier to *read* specifications. >> >> In particular, all the arguments that Erik put forward were motivated >> by the additional effort needed to *write* assignable clauses, which >> he wanted to conveniently omit. I can understand that omitting >> them makes the job of writing specs easier, particularly if your >> goal is to generate run-time checkable assertions (which aren't >> really affected by assignable). > > Yes, Erik did make that argument. But I meant that the specifications > with explicit assignable clauses are easier to read than those > without, and this goes back to Erik's argument that > assignable \nothing > is such a strong specification that you want to see it when it is > required. I think we may also be looking at the specification from > different viewpoints (client vs. implementer). > >>> My philosophy is to always make >>> it easier to read the specification, and if that makes it harder to >>> write, so be it. >> >> OK, so here is the critical problem. From your first statement, it >> is clear that a developer who omits assignable clauses is not defining >> the frame. > > I wasn't saying that exactly, although Erik was. > >> However, a reader trying to understand that partial >> specification is naturally going to form his own frame mentally >> when reading the partial specification. That's just the way people >> are (and it is the source of many errors in human perception). > > Agreed. > >> The reader is going to implicitly build a frame that (in general) >> contains the items that are explicitly mentioned in the spec. >> In practice, for most well-behaved methods, that should be >> approximately correct. >> >> However, if JML's *semantic definition* actually *defines* a >> default frame in such a case that encompasses much more than the >> reader's naive version (i.e., the "whole program" in the worst >> case scenario), then almost certainly, a human reader is going >> to *routinely* build up a mental understanding of such a method >> that conflicts with the actual meaning of the specification in >> JML's semantic model. > > Yes, that will be a problem, although it's perhaps better than the > problem with assignable \nothing as the default. I asked one of the > undergraduates working with me, Katie Becker, who has written some JML > specifications and worked all semester on this, what she thought it > meant when you omit the assignable clause (in a heavyweight > specification). She said it means that the specification allows > anything to be assigned to. I agree she may have been thinking of the > fields of the particular class instead of "everything" in the grand > sense, but she was very surprised when I told her it meant > "assignable \nothing;". I've had similar experiences with other > students. > >> In my mind, that is a readability problem. It means that >> "partial specs" that omit assignable clauses are likely to be >> read informally in a way that is contradictory to the JML >> semantic model. > > I agree that's a readability problem, but I think the change in > default makes it a smaller problem than currently for some > specifications than it was before (although still a problem). See > above. > >> Now, in practice, we know that virtually all methods where >> the assignable clause is omitted are not going to cause >> "random changes" elsewhere in the program, and this disconnect >> between what the spec would permit and what the code actually >> *does* would more than likely prevent any technically incorrect >> "misreadings" of the partial spec from causing any practical >> problems. >> >>> But that seems okay, because we >>> want the reader to always see when the method cannot assign anything. >> >> No--this is the "natural" assumption that people normally make. > > That is certainly an educational problem, but I'm not sure which is > "natural" to a human with no preconceptions in this area. > >> What we want is for them to *always* see when something can make >> arbitrarily far-reaching changes to the program state, including >> changes to objects not explicitly mentioned in the signature of >> the method. That is *definitely* something that should be >> explicit to the reader rather than hidden. > > I agree with that too, but the disadvantages outlined by Erik seem to > outweigh this. I would say that if someone really intends to say that > a method is chaotic like this, then it would be quite bad to hide that > in the default. But I think as a default \everything corresponds > better to the intuition that "I didn't say what it could assign" than > does \nothing, since \everything is a superset of whatever they could > actually assign. > >> This gets back to the statement I made at the end of my >> last message about "there's got to be a way to fix this >> problem." I'm not suggesting that one leave the default >> the way it is--instead, I'm suggesting that the default >> should be something that matches the reader's perceptions >> in the absence of an assignable clause (i.e., the scope >> of effects is limited to the receiver of the message and >> the parameters, or state reachable from these points). >> >> It sounds like you're really intending to head in that >> direction anyway, which is great. > > Yes, we are. I think JML desperately needs a context-limiting type > system and semantics for modifies/assignable clauses like that Mueller > and Poetzsch-Heffter pioneered. But I'd like to take this step first > and that step (which is more complex and harder to implement) second. > >> OK, what I meant to say was that, if \everything means everything >> allocated/addressable in the program (which you opened as a >> possibility), then this default would prevent one from using >> JML's semantic model to locally reason about the effects of an >> operation without an assignable clause. >> >>> People can still write all >>> of the old specifications they could write before, they just have to >>> express them differently. >> >> Sure. What I meant was that, if one omits assignable clauses-- >> and Erik's comments argue toward a practice where *most* people >> start off omitting them (and probably continue the practice >> until, if ever, they get interested in formal verification)--then >> such specs do not support local reasoning. > > Yes, I agree with all of that. It's true for methods that don't write > an assignable clause. So if you want to do formal verification, you > have to write assignable clauses in the specifications. I agree the > default affects this: if you don't write them in the \nothing default > we currently have, then you get incorrect implementations, but if you > don't write them in the \everything default, you get specifications > that aren't useful in proofs. > > The exact effect of these defaults is something I hadn't thought about > in exactly this way before. But perhaps it can be remedied by a > compiler "caution" message (like a warning that isn't filtered out). > If we change to \everything as the default, then perhaps we should > have a flag in JML that gives a caution whenever you check > specifications without a modifies/assignable clause. The warning > would only have to be given for methods that are not pure, since a > pure method has an implicit assignable clause. This would be useful > for instructors in courses as well as verifiers, but would be left off > by people doing runtime checking. > >>> Meshing with lightweight specifications >>> is certainly better supported this way. >> >> I agree that is the correct thing to do. I agree that assignable >> clauses should be "optional" in a clean way. However, for JML's >> semantic model, I think it all boils down to producing an effective >> definition of \everything that doesn't include "everything" ;-). > > I agree with that. Boyland's point about some storage never being > assignable is part of this, and contexts a la Mueller are another part. > >> Like I said, it sounds like that is what you intend to capture, so >> I'll wait until you do. I'm sure it will not have the limitations >> of allowing \everything to be a "program-wide" context. > > Yes, I think that's right. > > Thanks again, > > Other comments? > > -- > > Gary T. Leavens > Department of Computer Science, Iowa State University > 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA > http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 > > > "I've got to ask you," I say. "How long do you envision this rule of the universe to be?" "I'm guessing it's really very short." "Like how long?" "I don't know. In Mathematica, for example, perhaps three, four lines of code." "Four lines of code?" "[...] it will be short if Mathematica was a well-designed language. It will be longer if it doesn't happen to be as well-designed, in the sense that that doesn't happen to be the way the universe works. But we're not looking at 25,000 lines of code or something. We're looking at a handful of lines of code." "So it's not like Windows?" Stephen Wolfram, in an interview with Steven Levy; The Man Who Cracked The Code to Everything ...; Wired; June 2002; http://www.wired.com/wired/archive/10.06/wolfram.html From leavens@cs.iastate.edu Sun Dec 8 11:27:12 2002 Date: Sun, 8 Dec 2002 10:14:52 -0600 (CST) From: Gary T. Leavens To: Jan Dockx Cc: jml-interest-list@cs.iastate.edu Subject: Re: Fwd: JML-Interest: "assignable \nothing" vs "assignable \everything" as default Hi Jan, On Sun, 8 Dec 2002, Jan Dockx wrote: > Maybe the default should be: > @const \everything_which_is_not_statically_reachable_from_here > i.e., the transitive closure of all locations reachable from the static > type of the arguments of the method (including the implicit prime > argument). > > The difference with @assignable \anything (as I understand it) being > that you now do have positive information about the things the method > cannot know about, and you do not have any information about the things > the method can reach. If you want to keep your reasoning monotonic, you > should not depend on one of those latter things either being modifiable > or const. In practice this means that you should not try to prove that > another method using the former indeed does keep some things const, for > you do not have enough (stable) information for that. > And that is exactly what Garry is aiming at, as I understand it: > validation without taking modifiability into account, probably as a > starting point for use by students, and maybe as a starting point in any > design. That's an interesting suggestion. However, I think that the client has no good way to know what locations are statically reachable from a method that is being called. This is why we need some sort of alias controlling type system. I think with that we will be able to approximate this semantics. So I think we wouold like to do something like what you say. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From leavens@cs.iastate.edu Wed Dec 11 10:15:16 2002 Date: Wed, 11 Dec 2002 10:14:11 -0600 (CST) From: Gary T. Leavens To: JML Interest List Subject: JML-Interest: Re: Please sign up for the jmlspecs-interest mailing list on SourceForge Hi all, Sorry to bother you about this again. Just a quick note to say that the JML and multijava projects are now live on sourceforge.net, and you are welcome to participate in the development and discussions of JML there. Also, if you were not already signed up for the jmlspecs-interest mailing list at lists.sourceforge.net, and if you posted to the JML interest list during the past year, then I signed you up at the last email address through which you posted to the JML interest list. I intended that as a convenience; my sincere apologies if you are no longer interested in JML and need to unsubscribe. I didn't want to leave anybody behind. I would ask that all further discussions about the design and semantics of JML take place on the sourceforge jmlspecs-interest mailing list . We will turn this list off shortly. Also, if you read the JML interest mailing list, haven't posted to it in the past year, and aren't already signed up on source forge, please do sign up on sourceforge.net as described below. On Thu, 5 Dec 2002, Gary T. Leavens wrote: > JML is in the process of moving to sourceforge.net, which is already > hosting the MultiJava langauge development efforts. If you are a > subscriber to this jml-interest-list, you should sign up for the new > version of this list, which we will start using shortly, at least by > the beginning of the next calendar year. To do this, you should go to > > http://lists.sourceforge.net/lists/listinfo/jmlspecs-interest > > and fill in the information needed to subscribe to the list > jmlspecs-interest. This will be the replacement for the jml-interest > mailing list. As a bonus, the sourceforge version offers you some new > features, such as batching of messages. We plan to keep essentially > the same charter for this list. Note that only subscribers will be > able to post to it. -- Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580