From leavens@cs.uiowa.edu Tue Apr 10 11:26:08 2001 MIME-Version: 1.0 Date: Tue, 10 Apr 2001 11:24:59 -0500 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en To: Kevin Lillis Subject: Re: Annotated Proof Outline Content-Type: text/plain; charset=us-ascii Kevin, you wrote: > I'm unclear how the terms t and T appear in an annotated proof outline. > > It would help greatly if you could provide an annotated proof outline (using > the form shown on the first page of homework 6) for the solution to the > example given in Cohen section 10.2. Good idea. Cohen's development is summarized in the following annotated proof outline. { #b >= 0 } |[ var n: int ; n,y := 0, +inf { invariant (P0: x == (\min i : 0 <= i /\ i < n : b.i)) /\ (P1: 0 <= n /\ n <= #b), bound #b - n } ; do n != #b --> { P0 /\ P1 /\ n != #b /\ t = T } n, x := n+1, x min b.n { P0 /\ P1 t < T } od ]| { (R: x == (\min i : 0 <= i /\ i < #b : b.i)) } From leavens@cs.uiowa.edu Tue Apr 10 11:42:29 2001 MIME-Version: 1.0 Date: Tue, 10 Apr 2001 11:41:19 -0500 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en To: Rex Gray Subject: Re: Homework 6 Content-Type: text/plain; charset=us-ascii Rex, you wrote: > Hi Professor Leavens, > > Wie geht es ihnen? Ich bin sehr jetlagged :-) > I have discovered that the choice of order in assignment statements can > break the desk-checking of my programs. For example, the following program > to compute a series of products exhibits an off by one error, and is fixed > by reversing the order of assignments. > > Fails > ; n, x := 1, 1 > ; do n <=!=> N + 1 --> n, x := n + 1, n * x od > > Succeeds > ; n, x := 1, 1 > ; do n <=!=> N + 1 --> x, n := n * x od, n + 1 > > Was I naive to assume that the calculation method would handle this > situation automatically? Does this indicate I calculated incorrectly? In the guarded command language, the simultaneous assignment statements n,x := n+1, n*x and x,n := n*x, n+1 are equivalent, as you can verify by checking their weakest preconditions. However, is your translating these into a sequence of sequential assignments, then the two sequences n := n+1; x := n*x and x := n*x; n := n+1 are definitely not equivalent. I think that if you're working on verification of a C++ or Java program, then it might be best to avoid the simultaneous assignment statement and just use sequences of assignment statement. From leavens@cs.uiowa.edu Wed Apr 11 12:58:24 2001 MIME-Version: 1.0 Date: Wed, 11 Apr 2001 12:59:07 -0500 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Timothy VanFosson Subject: Re: New version of 10.13 Content-Type: text/plain; charset=us-ascii Tim, That looks good. I can't see any mistakes. Timothy VanFosson wrote: > Could you look at this solution to 10.13 and let me know if I've > made any mistakes. I decided that it was easier to come up with > an equivalence for the post-condition first, then develop the > program from that equivalence, i.e., show {Q} S {R1} /\ R1 <=> R. > > I'm still concerned about the large jump using transitivity, but > I don't know how to express it differently. That is a bit of a worry, but it's certainly a valid equivalence. I think to make the proof more solid (i.e., convincing) the only thing to do is a mutual implication proof. The proof that R ==> R1 is straightforward, using instantiation. The proof that R1 ==> R I think would use mathematical induction, and of course transitivity of implication. Seems like we could prove a lemma for this kind of thing in general that would apply to any transitive relation, and then be able to use cite it for this kind of step. > Also there is a step > in the proof for 3a where I make an assumption about the left-hand > of an equivalence in order to get n == 0 that I'm not sure about. I think you mean this step: n < 1 ==> (\forall i : 0 <= i /\ i < n : b.i ==> b.i+1) <=> (\forall i : 0 <= i /\ i < 0 : b.i ==> b.i+1) To me this is okay, although it does appeal to the model theory. If you want to do that kind of case analysis more rigoriously, you have several options. One is to stop the proof before this step, and explain why you have the various cases, and then carry on the separate calculations. I almost prefer making a separate proof of the implication, since that allows you to assume the hypothesis, and thus substitute. Like this: n < 1 ==> (\forall i : 0 <= i /\ i < n : b.i ==> b.i+1) <==> n == 0 ==> (\forall i : 0 <= i /\ i < n : b.i ==> b.i+1) <==> true Lemma: n == 0 ==> (\forall i : 0 <= i /\ i < n : b.i ==> b.i+1). Proof: Assume n == 0. (\forall i : 0 <= i /\ i < n : b.i ==> b.i+1) <==> (\forall i : 0 <= i /\ i < 0 : b.i ==> b.i+1) <==> true Gary From leavens@cs.uiowa.edu Thu Apr 12 10:11:07 2001 MIME-Version: 1.0 Date: Thu, 12 Apr 2001 10:10:41 -0500 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en To: Timothy VanFosson Subject: Re: JML pre-release for use in 181 Content-Type: text/plain; charset=us-ascii Tim, That's a fault of the zip archive, which was made on a windows machine. I'll add something about that to the instructions. The only ones you need to set the execute bit on are the ones in the bin directory. You'll also need to edit some of them, potentially. Gary Timothy VanFosson wrote: > When I unzipped the archive, none of the files in the bin directory had > the execute bit set. Is that a function of my unzipping process or a > defect in the archive? I confess I'm more familiar with gzip and compress, > which retain permission information, than zip. Are the only files that > need execute permission the ones in bin? > > tv > > At 09:12 AM 4/12/01 -0500, you wrote: > >Hi, > > > >I'm making JML available on the department machines in ~leavens/JML/. > >To run JML from this directory, put ~leavens/bin in your Unix PATH, > >and then invoke it with the command > > jml filename.java > >Alternatively, you can copy ~leavens/bin/jml to your own bin directory > >and run it from there. > > > >If you want to use JML on your own computer, download it from > > > >ftp://ftp.cs.iastate.edu/pub/leavens/JML/JML-pre-2.5.zip > > > >Then unzip this file, and follow the instructions in the README.txt > >file. Let me know if you have trouble getting it to run. > > > >The version of JML in these places is not yet version 2.5, but almost. > >This is almost ready to release, but not quite... Because of that, its > >documentation is slightly different than the documentation on the JML > >web page. When in doubt, trust the documentation in this release. See > >the file ~leavens/JML/JML.html for details. > > > > Gary > > -- > Timothy VanFosson, Manager E-mail: timv@ccad.uiowa.edu > Computing Services, Web Master WWW: http://www.ccad.uiowa.edu/~timv/ > Center for Computer-Aided Design US Mail: The University of Iowa > Phone: (319) 335-6298 228 ERF > FAX: (319) 384-0542 Iowa City, Iowa 52242 > > What good is it for a man to gain the whole world, yet forfeit > his soul? Or what can a man give in exchange for his soul? From leavens@cs.uiowa.edu Mon Apr 16 20:42:08 2001 MIME-Version: 1.0 Date: Mon, 16 Apr 2001 20:42:48 -0500 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Elise Anderson Subject: Re: New Release of JML, 2.5 Content-Type: text/plain; charset=us-ascii Elise, Elise Anderson wrote: > Should I take of the previous version from my computer before I add this > one? Or is this an upgrade? You can delete the previous one, although it's not necessary to do so. Gary From leavens@cs.uiowa.edu Tue Apr 17 17:10:24 2001 MIME-Version: 1.0 Date: Tue, 17 Apr 2001 17:09:31 -0500 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en To: Elise Anderson Subject: Re: Question - Step 2 Content-Type: text/plain; charset=us-ascii Elise, I think I finally see the cause for confusion in step 2 of my example solution for homework 6. The problem is in step 1. I have the proof written as P /\ B ==> R, but it should be P /\ !B ==> R. I'll correct the homework 6 file... Gary From leavens@cs.uiowa.edu Tue Apr 17 17:12:54 2001 MIME-Version: 1.0 Date: Tue, 17 Apr 2001 17:12:40 -0500 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en To: Elise Anderson Subject: Re: Question - Step 2 Content-Type: text/plain; charset=us-ascii Elise, Oops, I meant step 0 of the example was wrong... "Gary T. Leavens" wrote: > Elise, > > I think I finally see the cause for confusion in step 2 of my example > solution for homework 6. The problem is in step 1. That should be "step 0" above. Sigh. > I have > the proof written as P /\ B ==> R, but it should be P /\ !B ==> R. > > I'll correct the homework 6 file... > > Gary From leavens@cs.uiowa.edu Wed Apr 18 14:19:11 2001 MIME-Version: 1.0 Date: Wed, 18 Apr 2001 14:19:56 -0500 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Gary Leavens , Shu Liu , Students in 181 , Timothy VanFosson , Jeff Mohror , Kevin Lillis , Young Ki Kim Subject: Solving Cohen's 10.12 Content-Type: text/plain; charset=us-ascii Hi, I struggled last night to find a nice development for Cohen's problem 10.12, so I can appreciate the difficulty of it. But this morning I realized that I could avoid special cases and the use of an if-statement if I had an appropriate auxiliary variable. Amazingly enough, when I reread Cohen's section 10.5, this is exactly what I found, with one additional trick. The key to problems of this type seems to be the development on page 167 of Cohen's book, where he strengthens the invariant by introducing a new variable. But he doesn't just introduce a new variable, he also updates it just before updating the other variables, in a sequential composition. This allows the new variable to be initialized properly, and allows it to stay "in sync" (top of p. 168) with the progress of the loop counter. I tried this, and was pleasantly surprised with the result. It's much simpler than directly adapting Tim's solution to 10.13 (which I also did, but wasn't very happy with). I also produced a third solution that uses various special cases but it turned out to be very ugly. Anyway, if you haven't done this problem yet, please read over Cohen's section 10.5 carefully, and try to adapt it. If you're stuck, I can send you a more explicit hint (e.g., the additional invariant, or help you with a proof). Also, I think you will be much better off at this point solving these verification problems on-line. I think it would take much more time to write them out long-hand. Gary From leavens@cs.uiowa.edu Sun Apr 22 18:15:36 2001 MIME-Version: 1.0 Date: Sun, 22 Apr 2001 18:15:41 -0500 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Kevin Lillis CC: leavens@cs.iastate.edu Subject: Re: Running JML Content-Type: text/plain; charset=us-ascii Kevin, It looks to me like you forgot to unjar the Java source files. You need to have the Java source files available for JML to work. The javac compiler doesn't need them. Gary Kevin Lillis wrote: > Gary, > > I downloaded the file JML.2.5.zip and installed JML. I believe I made the > appropriate changes to the batch files. > > To test it I entered the specification given on page 2 of "Preliminary > Design of JML" which was handed out in class. > > The specification I entered is: > > public class IntMathOps { > /*@ public normal_behavior > @ requires y >= 0; > @ ensures \result * \result <= y > @ && y < (\result + 1) * (\result + 1); > @*/ > public static int isqrt(int y) { > return (int) Math.sqrt(y); > } > } > > When I run JML I get the following error: > > Type checking IntMathOps.java ... > edu.iastate.cs.jml.models.JMLNoSuchElementException: Map not defined at > Object > { (String, PlaceHolder java.lang.String) (System, PlaceHolder > java.lang.System) > (Character, PlaceHolder java.lang.Character) } > > Start type checking IntMathOps.java > IntMathOps.java:8:(Col 29): Undefined Variable Math > IntMathOps.java:8:(Col 29): Dot operation not supported on Unknown Math > IntMathOps.java:8:(Col 34): Undefined Variable sqrt > IntMathOps.java:0:(Col 0): Improper Cast from type boolean to type int > IntMathOps.java had 4 type error(s) > > I'm not sure why Math is undefined. If I run the file through javac it > compiles with no errors. > > Any ideas? > > Thanks > > Kevin Lillis From leavens@cs.uiowa.edu Mon Apr 23 15:13:27 2001 MIME-Version: 1.0 Date: Mon, 23 Apr 2001 15:14:20 -0500 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Kevin Lillis Subject: Re: Environment Space Content-Type: text/plain; charset=us-ascii Kevin, I think that you may want to adjust the DOS properties of the jml.bat file to increase the environment space. Use explorer, right click on the jml.bat file, and go to properties, the memory page, and change the size of the environment it gets. Gary Kevin Lillis wrote: > Gary, > > I've modified my environment so I have 1024 bytes of Environment space when > in a DOS window. > > When I run JML for the first time in a DOS window I receive no error > messages. However, upon every subsequent execution of JML I receive an "Out > of environment space" Error. The JML program seems to report the presence > or absence of errors in my file properly even with the Environment Space > error. > > If I just ignore the error can I rely on the output regarding my > specification file? > > Thanks > > Kevin Lillis > > -----Original Message----- > From: Gary T. Leavens [mailto:leavens@cs.uiowa.edu] > Sent: Monday, April 23, 2001 9:42 AM > To: Kevin Lillis > Subject: Re: Running JML > > Kevin, > > Great, glad to hear it. > > Gary > > Kevin Lillis wrote: > > > BINGO! > > > > I unjarred the source files and now JML run fine. > > > > Thanks > > > > Kevin Lillis > > > > -----Original Message----- > > From: Gary T. Leavens [mailto:leavens@cs.uiowa.edu] > > Sent: Sunday, April 22, 2001 6:16 PM > > To: Kevin Lillis > > Cc: leavens@cs.iastate.edu > > Subject: Re: Running JML > > > > Kevin, > > > > It looks to me like you forgot to unjar the Java source files. You need > > to have the Java source files available for JML to work. The javac > compiler > > doesn't need them. > > > > Gary > > > > Kevin Lillis wrote: > > > > > Gary, > > > > > > I downloaded the file JML.2.5.zip and installed JML. I believe I made > the > > > appropriate changes to the batch files. > > > > > > To test it I entered the specification given on page 2 of "Preliminary > > > Design of JML" which was handed out in class. > > > > > > The specification I entered is: > > > > > > public class IntMathOps { > > > /*@ public normal_behavior > > > @ requires y >= 0; > > > @ ensures \result * \result <= y > > > @ && y < (\result + 1) * (\result + 1); > > > @*/ > > > public static int isqrt(int y) { > > > return (int) Math.sqrt(y); > > > } > > > } > > > > > > When I run JML I get the following error: > > > > > > Type checking IntMathOps.java ... > > > edu.iastate.cs.jml.models.JMLNoSuchElementException: Map not defined at > > > Object > > > { (String, PlaceHolder java.lang.String) (System, PlaceHolder > > > java.lang.System) > > > (Character, PlaceHolder java.lang.Character) } > > > > > > Start type checking IntMathOps.java > > > IntMathOps.java:8:(Col 29): Undefined Variable Math > > > IntMathOps.java:8:(Col 29): Dot operation not supported on Unknown Math > > > IntMathOps.java:8:(Col 34): Undefined Variable sqrt > > > IntMathOps.java:0:(Col 0): Improper Cast from type boolean to type int > > > IntMathOps.java had 4 type error(s) > > > > > > I'm not sure why Math is undefined. If I run the file through javac it > > > compiles with no errors. > > > > > > Any ideas? > > > > > > Thanks > > > > > > Kevin Lillis From leavens@cs.uiowa.edu Mon Apr 23 23:25:18 2001 MIME-Version: 1.0 Date: Mon, 23 Apr 2001 23:26:04 -0500 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Elise Anderson Subject: Re: Hw 7 questions Content-Type: text/plain; charset=us-ascii Elise, Elise Anderson wrote: > 3. lcm(a,b) = (a * b) / gcd(a,b) and I am wondering > how to do this in a specification? Can I just say > gcd(a,b)? No, that's not built-in to Java or the JML models. You can specify a pure model method that computes gcd, however, and use that. > 6. Does this problem mean: > > input 2 output ** input 5 output ***** > or > input 2 output * input 5 output * The first one is the right one. For input 2, you get ** as output. > 7. How should the output look? > input (2, 6, 4) > output ** > ****** > **** Yes, that seems reasonable. > 10. These problems are always hard since I have not > coded in such a long time. I will try to find > something. Recall that problem 10 isn't due tomorrow (Tuesday :-) > 11. What does this question mean? What exactly is > being requested? This asks you to add a "for_example" clause to the JML specification. I'll explain in class tomorrow. > Misc. Can I assume that all of these methods are > static? Yes. Good questions. Gary From leavens@cs.uiowa.edu Tue Apr 24 00:25:17 2001 MIME-Version: 1.0 Date: Tue, 24 Apr 2001 00:25:59 -0500 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Rex Gray CC: leavens@cs.iastate.edu Subject: Re: Homework Question Content-Type: text/plain; charset=us-ascii Rex, Yes, you can use java.lang.Math functions (assuming we had specified them as "pure"). The problem is probably that you haven't unjarred the Java source files. The JML checker needs these in order to type check things in java.lang.Math. See the README.txt file in the release for what to do if this isn't clear, but if you're getting the same kind of errors that Kevin Lillis was (see the q_and_a.txt file from the course web page), then that's the problem. Gary Rex Gray wrote: > Professor Leavens, > > I had thought that I could reference java.lang.Math functions inside of an > ensures clause. I want to use max() and abs(). Of course, the jml checker > doesn't like it. It does accept my spec. when I define local versions of > max() and abs(). > > These functions have no side effects. I should be able to use them, > shouldn't I? > > Rex From leavens@cs.uiowa.edu Mon Apr 30 11:01:55 2001 MIME-Version: 1.0 Date: Mon, 30 Apr 2001 11:02:32 -0500 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Kevin Lillis Subject: Re: public invariants Content-Type: text/plain; charset=us-ascii Kevin, Kevin Lillis wrote: > Dr. Leavens, > > If I have a public_invariant, do I also need to repeatedly state that > condition in the ensures clauses of the different methods? > > For example, if I have the following invariant: > > //@ public invariant length == deg + 1; > > It would seem that a method that can assign to both length and degree could > be specified as: > > /*@ public normal_behavior > @ assignable length, deg; > @ ensures deg == 0; > @ ensures_redundantly length == 1; > @*/ > public void changeBoth(); > > This seems ok since the invariant provides an additional requirement on > length, namely that length == deg + 1 Yes, that's exactly right. Gary From leavens@cs.uiowa.edu Mon Apr 30 11:08:26 2001 MIME-Version: 1.0 Date: Mon, 30 Apr 2001 11:09:04 -0500 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Kevin Lillis CC: leavens@cs.iastate.edu Subject: Re: JMLObjectSequence Content-Type: text/plain; charset=us-ascii Kevin, you wrote: > When trying to use JMLObjectSequence for the polynomial specification I am > having trouble using specific values for the objects in the sequence. I > can't store values of type int and can't compare objects to int values. > Should I be using type Integer instead? Remember first that this is now an extra-credit problem. When using JMLObjectSequence you will have to store the numbers in Integer objects, since int's aren't values in Java, and when you extract them, you have to downcast the Object returned. The way this is done is demonstrated in the WineList example in the notes. There, for example, the recommend method is downcasting the result of prices.itemAt(R) to a Float, and then using floatValue: /*@ public normal_behavior @ forall int R; @ ensures \result.equals((String)names.itemAt(R)) @ && 0 <= R && R < prices.length() @ && ((String)names.itemAt(R)).indexOf(name) != -1 @ && ((Float)prices.itemAt(R)).floatValue() @ == (\max int i; @ 0 <= i && i < prices.length() @ && ((String)names.itemAt(R)).indexOf(name) != -1; @ ((Float)prices.itemAt(i)).floatValue()); @ ensures_redundantly \result != null; @*/ public abstract String recommend(String name); > I completed the specification with an array of int values and it seemed > straightforward. What are the advantages writing the specification using > JMLObjectSeqence? > The type JMLObjectSequence has more operations than arrays in Java; for example, it has operations to concatenate sequences. These are sometimes useful in specification to specify things at a higher level of abstraction. However, it is inconvenient to have to deal with conversions to and from the object types and the downcasting... Gary From leavens@cs.uiowa.edu Mon Apr 30 15:50:36 2001 MIME-Version: 1.0 Date: Mon, 30 Apr 2001 15:51:26 -0500 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Timothy VanFosson Subject: Re: problem 14 Content-Type: text/plain; charset=us-ascii Tim, you wrote: > I'm a little fuzzy on what's required for problem 14. Am I correct in > assuming that you want a public specification for the interface to a > Rational class and a private specification for the implementation of the > interface, which will have depends, represents, and, perhaps, additional > invariant clauses. Yes, although you don't have to have them in separate files. While you can do a separate interface and implementation class, you can also just do a class and include both the model and implementation in the same .java file. > Am I correct in assuming too that since the invariant clause holds for all > permissible, final states of objects of the class, that I need not include > it in the ensures clauses for any of my methods (simply make sure that both > my implementation and any ensures clause I have is consistent with it)? Yes, that's right. Gary From leavens@cs.uiowa.edu Mon Apr 30 20:30:03 2001 MIME-Version: 1.0 Date: Mon, 30 Apr 2001 20:30:46 -0500 From: "Gary T. Leavens" Reply-To: leavens@cs.uiowa.edu X-Accept-Language: en,de,fr To: Elise Anderson CC: leavens@cs.iastate.edu Subject: Re: Rational Numbers on HW7 Content-Type: text/plain; charset=us-ascii Elise, you wrote: > One of my questions may not have been too clear. I > wanted to know if the division method is dividing two > rational numbers or is it dividing the numerator by > the denominator? Of course, the design is up to you. But I would like you to include a division of one rational number by another rational number. You can also include other divisions (e.g., a rational by an integer), if you want, but it's not necessary. > When we talk about rational number, do we include: > > maximum integer and minimum integer? > If you wish, you can include a largest and smallest rational as constants. You should be able to make a rational such as the maximum integer divided by 1. > a/b, where a & b are integers and b != 0? Yes, this is basically what a rational number is abstractly, a pair of integers, with the denominator not equal to zero. > And when you say division, you are talking about > getting a decimal value for a/b, correct? No, I mean dividing one rational number by another, producing a rational number as a result. E.g., 2/3 divided by 1/7 is 14/3. Does that help? Gary