From leavens@larch.cs.iastate.edu Wed Nov 24 01:04:52 2004 Date: Wed, 24 Nov 2004 01:04:52 -0600 (CST) From: Gary T. Leavens To: tdras@cs.iastate.edu Subject: Re: JML Hi Tyler, On Mon, 22 Nov 2004 tdras@cs.iastate.edu wrote: > Dr. Leavens, > > What's the difference between using //@ and /*@ in JML? They seem to be > interchangable, but I really can't tell. As in Java, //@ is a single line annotation, that is the annotation area extends to the end of the line. When you use /*@, the annotation extends until the next @*/. 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@larch.cs.iastate.edu Sun Nov 28 18:10:08 2004 Date: Sun, 28 Nov 2004 18:10:08 -0600 (CST) From: Gary T. Leavens To: Tyler Rasmussen Subject: Re: JML Questions Hi Tyler, On Sun, 28 Nov 2004, Tyler Rasmussen wrote: > We needed to implement the compareTo() function from Comparable. We looked > back at the answers to practice test 1 and found the following code > (slightly modified to fit our program): > > > > /*@ also > > @ requires o instanceof Major; > > @ ensures \result == compareTo((Major)o); > > @ also > > @ requires !(o instanceof Major); > > @ signals (ClassCastException e) e != null; > > @*/ > > > > We know that the also keyword is used for situations where it is inheriting > methods, so that explains the first also. Is the second also used as and > "OR" situation? Technically, "also" is more like an "and" than an "or". It means that the method must satisfy both specifications. A method satisifies a specification if, when the precondition holds, it terminates in a state where the postcondition holds. But when the requires clauses are disjoint (as here), you can think of it as "or" if that helps you. > Could the code, for example, be expanded to this (in order > to totally follow the requirements of compareTo() as specified by Java > 1.4.2): > > > > /*@ also > > @ requires o instanceof Major; > > @ ensures \result == compareTo((Major)o); > > @ also > > @ requires !(o instanceof Major); > > @ signals (ClassCastException e) e != null; > > @ also > > @ requires o == null; > > @ signals (NullPointerException e) e != null; > > @*/ > If you do that, you should instead write: /*@ also @ requires o != null && o instanceof Major; @ ensures \result == compareTo((Major)o); @ also @ requires o != null && !(o instanceof Major); @ signals (ClassCastException e) e != null; @ also @ requires o == null; @ signals (NullPointerException e) e != null; @*/ But it's not necessary to specify this exceptional behavior, you can simply make it a precondition that o isn't null. > If also is in effect an "OR" clause, can that also be used in other > situations where the methods aren't inherited? Yes, you can use "also" to do case analysis in general. > For example: > > > > /** > > * Gets the Vector of all the Departments in the College. > > * @return The Vector of all the Departments in the College. > > */ > > /*@ requires d == null; > > @ ensures \result == null; You probably mean \result != null above, right? > @ also > > @ requires d != null > > @ ensures (\forall int i; i >=0 && i < d.size(); \result.get(i) > instanceof Department); > > @*/ > > public /*@ pure @*/ Vector getAllDepartments(){ > > return d; > > } yes, you can do that. > Are there any other keywords that would be helpful (like \forall, which has > been helpful in our Vector classes)? There is \exists, which is similar. I'm not sure what you need... > Is there any way in Eclipse to run our program using the JML Compiler to do > run-time checks? Yes, you can download the JML/Eclipse plugin. See the JML website's downloads page. > Is there any way in Eclipse to create the JUnit files from the JML? Or can > this only be run in the command line? Yes, that's also in the Eclipse plugin. 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@larch.cs.iastate.edu Fri Dec 3 00:13:50 2004 Date: Fri, 3 Dec 2004 00:13:50 -0600 (CST) From: Gary T. Leavens To: Dan Hrivnak Subject: Re: Practice test from Spring 2003 question... Hi Dan, On Thu, 2 Dec 2004, Dan Hrivnak wrote: > I can't find solutions to any of the old tests online, but I'm trying > to work on them anyway. On problem 2 of this test, it seems that > either answer would work, though I am leaning towards (b). Could you > either send me a solution or explain this answer? Yes, I think they are more fun without answers :-). Yes, the answer is (b) for that test. The Reservation object will be interacting with the TripLeg object more anyway. (In addition, controller's aren't supposed to do too many interesting things like that, or they become incohesive...) Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 ---------------- From leavens@cs.iastate.edu Tue Dec 7 21:28:50 2004 Date: Tue, 7 Dec 2004 21:28:51 -0600 (CST) From: Gary T. Leavens To: Michael Roberts Cc: cs362s@cs.iastate.edu Subject: Re: Hw 9 and JML specs Hi Michael, On Tue, 7 Dec 2004, Michael Roberts wrote: > Hi, > Our group is working on the JML specifications required by homework 9 and > we're running into a few difficulties. Since most of our classes are closely > tied the filesystem or playing sound files it's difficult to write any > formally specified JML and the informal comments that I write don't seem to > add much to the javadocs. For example: > > /** Logs the playing of a song. > * > * @param songTitle The title of the song that was played. > */ > //@ requires songTitle != null; > //@ ensures (* The log has recorded that the song was played*); > public void logPlay(String songTitle) > > Any suggestions? I suggest that you not write javadocs for such methods. The homework allows this: Your code should be clearly written and indented, and should include either javadoc documentation comments or JML specifications. > Also I'm trying use \return as a parameter to a function in a jml spec and I > can't figure out a way to do that that makes the JML checker happy. Here's > what I'm trying to do: > > //@ ensures collections.contains(\return); It should be \result, not \return. I'm sure that's the problem. > Finally I was wondering if there was a way to configure the plugin so that > when you type /*@ and hit return it will generate a jml comment, similar to > what eclipse does when you hit return after typing /** for a javadoc comment. There probably is, but it hasn't been done yet. I put in a feature request for this. Sorry. What I do in the mean time is start by copying another JML comment and then editing it. Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 ---------------------------- From leavens@cs.iastate.edu Sat Dec 11 17:36:01 2004 Date: Sat, 11 Dec 2004 17:36:02 -0600 (CST) From: Gary T. Leavens To: Robert Dyer Cc: Com S 362 students and staff -- Aaron Becker , com_s_362@cs.iastate.edu, Staff for Com S 362 -- Kun Liang , Matthew Ring , Dan Hrivnak , Jacob Huber , Josh Solyntjes , Gary Leavens , Matt Hall , William Gerald Hoffa Subject: Re: HW10 question: can use laptop or transparencies Hi Robert, (and 362 students), On Sat, 11 Dec 2004, Robert Dyer wrote: > I was wondering if we can use something like an overhead or maybe >even a computer projector for our presentation of Homework 10. We >are going to need to explain some about our design and I figured it >would be easiest to just show a scaled down (ie, some >attributes/methods removed) version of our design class diagram and >then explain it from that. > > Let me know if this is possible, and if so what we can use. It >wouldn't be hard to make transparencies or I could bring in my >laptop, either way would be wonderful. Thanks. Right. I was planning to send an email about this, so thanks for asking. This year, since we have 10 groups and 2 hours, we could take about 12 minutes per group. Since you are supposed to limit yourselves to 10 minutes, we could use 2 minutes for set-up time. In other words, it would be okay to use the overhead or laptop projection. This may be especially helpful for showing the class diagram, screen shots, etc. So feel free to use the overhead on a laptop. If some group wants to do that but doesn't have a laptop of their own, please send me powerpoint or PDF files ahead of time, and you can use my laptop during the presentation on Thursday. 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