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 t