BABYL OPTIONS: -*- rmail -*- Version: 5 Labels: Note: This is the header of an rmail file. Note: If you are seeing it in rmail, Note: it means the file has no messages in it.  1,, Mail-from: From leavens@cs.iastate.edu Tue May 25 13:02:46 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id NAA03005; Tue, 25 May 1999 13:02:45 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id NAA24743; Tue, 25 May 1999 13:02:39 -0500 (CDT) Date: Tue, 25 May 1999 13:02:39 -0500 (CDT) Message-Id: <199905251802.NAA24743@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jgurney@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: Majordomo server *** EOOH *** Return-Path: Date: Tue, 25 May 1999 13:02:39 -0500 (CDT) From: "Gary T. Leavens" To: jgurney@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: Majordomo server Jason, Dave Madsen said you knew how to set up a mailing list on the majordomo server so users can subscribe and unsubscribe themselves. Can you tell me how to do it? Gary  1, answered,, Mail-from: From jgurney@cs.iastate.edu Tue May 25 13:17:44 1999 Return-Path: Received: from crow (crow.cs.iastate.edu [129.186.3.98]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with SMTP id NAA03222 for ; Tue, 25 May 1999 13:17:44 -0500 (CDT) Message-Id: <4.1.19990525130923.00a90860@imap.cs.iastate.edu> X-Sender: jgurney@imap.cs.iastate.edu X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Tue, 25 May 1999 13:17:32 -0500 To: "Gary T. Leavens" From: Jason L Gurney Subject: Re: Majordomo server In-Reply-To: <199905251802.NAA24743@larch.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" *** EOOH *** Return-Path: X-Sender: jgurney@imap.cs.iastate.edu X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Tue, 25 May 1999 13:17:32 -0500 To: "Gary T. Leavens" From: Jason L Gurney Subject: Re: Majordomo server In-Reply-To: <199905251802.NAA24743@larch.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" At 01:02 PM 5/25/99 -0500, you wrote: >Jason, > >Dave Madsen said you knew how to set up a mailing list on the majordomo >server so users can subscribe and unsubscribe themselves. Can you tell >me how to do it? > > Gary It would probably be something that I would have to set up. If you give me the list name I could begin working on it. ---------------------------------------------------------------------- Jason L. Gurney Systems Analyst jgurney@cs.iastate.edu Systems Support Group Computer Science Department 108 Atanasoff Iowa State University Office Phone: 294-7214 ----------------------------------------------------------------------  1,, Mail-from: From madsen@cs.iastate.edu Tue May 25 08:43:59 1999 Return-Path: Received: from sentinel (sentinel.cs.iastate.edu [129.186.3.131]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with SMTP id IAA28277; Tue, 25 May 1999 08:43:58 -0500 (CDT) Message-Id: <4.1.19990525084125.00a23280@imap.cs.iastate.edu> X-Sender: madsen@imap.cs.iastate.edu X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Tue, 25 May 1999 08:43:57 -0500 To: "Gary T. Leavens" , madsen@cs.iastate.edu From: Dave Madsen Subject: Re: jml-interest mailing list. Cc: leavens@cs.iastate.edu In-Reply-To: <199905250140.UAA15466@larch.cs.iastate.edu> References: <4.1.19990524144854.00a73100@imap.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" *** EOOH *** Return-Path: X-Sender: madsen@imap.cs.iastate.edu X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Tue, 25 May 1999 08:43:57 -0500 To: "Gary T. Leavens" , madsen@cs.iastate.edu From: Dave Madsen Subject: Re: jml-interest mailing list. Cc: leavens@cs.iastate.edu In-Reply-To: <199905250140.UAA15466@larch.cs.iastate.edu> References: <4.1.19990524144854.00a73100@imap.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" At 08:40 PM 5/24/99 -0500, Gary T. Leavens wrote: >Dave, > >We don't have any list server that people can automagically subscribe to >by sending an email message with the right format? We do have a majordomo server that I believe will allow people to subscribe and unsubscribe themselves. The person to talk to about this is jgurney@cs.iastate.edu, who maintains the majordomo server. Dave --- Dave R. Madsen, Systems Administrator Computer Science Department, Iowa State University http://www.cs.iastate.edu/~madsen - madsen@cs.iastate.edu  1,, Mail-from: From leavens@cs.iastate.edu Tue May 25 14:11:05 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id OAA03916; Tue, 25 May 1999 14:11:04 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id OAA25330; Tue, 25 May 1999 14:10:58 -0500 (CDT) Date: Tue, 25 May 1999 14:10:58 -0500 (CDT) Message-Id: <199905251910.OAA25330@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jgurney@cs.iastate.edu CC: leavens@cs.iastate.edu In-reply-to: <4.1.19990525130923.00a90860@imap.cs.iastate.edu> (message from Jason L Gurney on Tue, 25 May 1999 13:17:32 -0500) Subject: Re: Majordomo server *** EOOH *** Return-Path: Date: Tue, 25 May 1999 14:10:58 -0500 (CDT) From: "Gary T. Leavens" To: jgurney@cs.iastate.edu CC: leavens@cs.iastate.edu In-reply-to: <4.1.19990525130923.00a90860@imap.cs.iastate.edu> (message from Jason L Gurney on Tue, 25 May 1999 13:17:32 -0500) Subject: Re: Majordomo server Jason, > At 01:02 PM 5/25/99 -0500, you wrote: > >Jason, > > > >Dave Madsen said you knew how to set up a mailing list on the majordomo > >server so users can subscribe and unsubscribe themselves. Can you tell > >me how to do it? > > > > Gary > > It would probably be something that I would have to set up. If you give me > the list name I could begin working on it. Thanks. I would like to call the mailing list jml-interest@cs.iastate.edu if that works. Gary  1,, Mail-from: From jgurney@cs.iastate.edu Tue May 25 16:04:22 1999 Return-Path: Received: from crow (crow.cs.iastate.edu [129.186.3.98]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with SMTP id QAA06086 for ; Tue, 25 May 1999 16:04:21 -0500 (CDT) Message-Id: <4.1.19990525160043.00a8f6f0@imap.cs.iastate.edu> X-Sender: jgurney@imap.cs.iastate.edu X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Tue, 25 May 1999 16:04:13 -0500 To: "Gary T. Leavens" From: Jason L Gurney Subject: Re: Majordomo server In-Reply-To: <199905251910.OAA25330@larch.cs.iastate.edu> References: <4.1.19990525130923.00a90860@imap.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" *** EOOH *** Return-Path: X-Sender: jgurney@imap.cs.iastate.edu X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Tue, 25 May 1999 16:04:13 -0500 To: "Gary T. Leavens" From: Jason L Gurney Subject: Re: Majordomo server In-Reply-To: <199905251910.OAA25330@larch.cs.iastate.edu> References: <4.1.19990525130923.00a90860@imap.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" This is the first list I have created from scratch so your patience is appreciated. I believe the list is set up correctly and users may subscribe/unsubscribe by sending mail to mdomo@cs.istate.edu with no subject and a body consisting of: subscribe/unsubscribe jml-interest-list end Also, who would you like to be allowed to post messages to this list? Jason At 02:10 PM 5/25/99 -0500, you wrote: >Jason, > >> At 01:02 PM 5/25/99 -0500, you wrote: >> >Jason, >> > >> >Dave Madsen said you knew how to set up a mailing list on the majordomo >> >server so users can subscribe and unsubscribe themselves. Can you tell >> >me how to do it? >> > >> > Gary >> >> It would probably be something that I would have to set up. If you give me >> the list name I could begin working on it. > >Thanks. I would like to call the mailing list > jml-interest@cs.iastate.edu >if that works. > > Gary  1, answered, filed,, Mail-from: From jgurney@cs.iastate.edu Tue May 25 16:04:22 1999 Return-Path: Received: from crow (crow.cs.iastate.edu [129.186.3.98]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with SMTP id QAA06086 for ; Tue, 25 May 1999 16:04:21 -0500 (CDT) Message-Id: <4.1.19990525160043.00a8f6f0@imap.cs.iastate.edu> X-Sender: jgurney@imap.cs.iastate.edu X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Tue, 25 May 1999 16:04:13 -0500 To: "Gary T. Leavens" From: Jason L Gurney Subject: Re: Majordomo server In-Reply-To: <199905251910.OAA25330@larch.cs.iastate.edu> References: <4.1.19990525130923.00a90860@imap.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" *** EOOH *** Return-Path: X-Sender: jgurney@imap.cs.iastate.edu X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Tue, 25 May 1999 16:04:13 -0500 To: "Gary T. Leavens" From: Jason L Gurney Subject: Re: Majordomo server In-Reply-To: <199905251910.OAA25330@larch.cs.iastate.edu> References: <4.1.19990525130923.00a90860@imap.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" This is the first list I have created from scratch so your patience is appreciated. I believe the list is set up correctly and users may subscribe/unsubscribe by sending mail to mdomo@cs.istate.edu with no subject and a body consisting of: subscribe/unsubscribe jml-interest-list end Also, who would you like to be allowed to post messages to this list? Jason At 02:10 PM 5/25/99 -0500, you wrote: >Jason, > >> At 01:02 PM 5/25/99 -0500, you wrote: >> >Jason, >> > >> >Dave Madsen said you knew how to set up a mailing list on the majordomo >> >server so users can subscribe and unsubscribe themselves. Can you tell >> >me how to do it? >> > >> > Gary >> >> It would probably be something that I would have to set up. If you give me >> the list name I could begin working on it. > >Thanks. I would like to call the mailing list > jml-interest@cs.iastate.edu >if that works. > > Gary  1,, Mail-from: From leavens@cs.iastate.edu Tue May 25 20:02:13 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id UAA08927; Tue, 25 May 1999 20:02:12 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id UAA01158; Tue, 25 May 1999 20:02:03 -0500 (CDT) Date: Tue, 25 May 1999 20:02:03 -0500 (CDT) Message-Id: <199905260102.UAA01158@larch.cs.iastate.edu> From: "Gary T. Leavens" To: mdomo@cs.istate.edu CC: leavens@cs.iastate.edu *** EOOH *** Return-Path: Date: Tue, 25 May 1999 20:02:03 -0500 (CDT) From: "Gary T. Leavens" To: mdomo@cs.istate.edu CC: leavens@cs.iastate.edu subscribe jml-interest-list  1,, Mail-from: From leavens@cs.iastate.edu Tue May 25 20:02:59 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id UAA08939; Tue, 25 May 1999 20:02:58 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id UAA01162; Tue, 25 May 1999 20:02:49 -0500 (CDT) Date: Tue, 25 May 1999 20:02:49 -0500 (CDT) Message-Id: <199905260102.UAA01162@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jgurney@cs.iastate.edu CC: leavens@cs.iastate.edu In-reply-to: <4.1.19990525160043.00a8f6f0@imap.cs.iastate.edu> (message from Jason L Gurney on Tue, 25 May 1999 16:04:13 -0500) Subject: Re: Majordomo server *** EOOH *** Return-Path: Date: Tue, 25 May 1999 20:02:49 -0500 (CDT) From: "Gary T. Leavens" To: jgurney@cs.iastate.edu CC: leavens@cs.iastate.edu In-reply-to: <4.1.19990525160043.00a8f6f0@imap.cs.iastate.edu> (message from Jason L Gurney on Tue, 25 May 1999 16:04:13 -0500) Subject: Re: Majordomo server Jason, Thanks. Can we allow anyone who is subscribed (but no others), to post to the list? That seems like a good policy for now. Gary  1, answered,, Mail-from: From jgurney@cs.iastate.edu Wed May 26 09:09:30 1999 Return-Path: Received: from crow (crow.cs.iastate.edu [129.186.3.98]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with SMTP id JAA27737 for ; Wed, 26 May 1999 09:09:29 -0500 (CDT) Message-Id: <4.1.19990526090703.00a97780@imap.cs.iastate.edu> X-Sender: jgurney@imap.cs.iastate.edu X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Wed, 26 May 1999 09:09:21 -0500 To: "Gary T. Leavens" From: Jason L Gurney Subject: Re: Majordomo server In-Reply-To: <199905260102.UAA01162@larch.cs.iastate.edu> References: <4.1.19990525160043.00a8f6f0@imap.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" *** EOOH *** Return-Path: X-Sender: jgurney@imap.cs.iastate.edu X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Wed, 26 May 1999 09:09:21 -0500 To: "Gary T. Leavens" From: Jason L Gurney Subject: Re: Majordomo server In-Reply-To: <199905260102.UAA01162@larch.cs.iastate.edu> References: <4.1.19990525160043.00a8f6f0@imap.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" The list appears to be set up correctly. Please ensure that when users post/subscribe/unsubscribe they do so from the same account (mailing address) to help avoid bounces. If any problems arise, let me know. Jason At 08:02 PM 5/25/99 -0500, you wrote: >Jason, > >Thanks. Can we allow anyone who is subscribed (but no others), >to post to the list? That seems like a good policy for now. > > Gary  1,, Mail-from: From leavens@cs.iastate.edu Wed May 26 10:49:00 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id KAA01557; Wed, 26 May 1999 10:48:59 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id KAA08715; Wed, 26 May 1999 10:48:54 -0500 (CDT) Date: Wed, 26 May 1999 10:48:54 -0500 (CDT) Message-Id: <199905261548.KAA08715@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jgurney@cs.iastate.edu CC: leavens@cs.iastate.edu In-reply-to: <4.1.19990526090703.00a97780@imap.cs.iastate.edu> (message from Jason L Gurney on Wed, 26 May 1999 09:09:21 -0500) Subject: Re: Majordomo server *** EOOH *** Return-Path: Date: Wed, 26 May 1999 10:48:54 -0500 (CDT) From: "Gary T. Leavens" To: jgurney@cs.iastate.edu CC: leavens@cs.iastate.edu In-reply-to: <4.1.19990526090703.00a97780@imap.cs.iastate.edu> (message from Jason L Gurney on Wed, 26 May 1999 09:09:21 -0500) Subject: Re: Majordomo server Jason, Ok, thanks. I'll let you know if we have difficulties. Gary  1,, Mail-from: From MAILER-DAEMON Tue May 25 20:02:14 1999 Return-Path: Received: from localhost (localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) with internal id UAA08928; Tue, 25 May 1999 20:02:14 -0500 (CDT) Date: Tue, 25 May 1999 20:02:14 -0500 (CDT) From: Mail Delivery Subsystem Message-Id: <199905260102.UAA08928@css-1.cs.iastate.edu> To: MIME-Version: 1.0 Content-Type: multipart/report; report-type=delivery-status; boundary="UAA08928.927680534/css-1.cs.iastate.edu" Subject: Returned mail: Host unknown (Name server: cs.istate.edu: host not found) Auto-Submitted: auto-generated (failure) *** EOOH *** Return-Path: Date: Tue, 25 May 1999 20:02:14 -0500 (CDT) From: Mail Delivery Subsystem To: MIME-Version: 1.0 Content-Type: multipart/report; report-type=delivery-status; boundary="UAA08928.927680534/css-1.cs.iastate.edu" Subject: Returned mail: Host unknown (Name server: cs.istate.edu: host not found) Auto-Submitted: auto-generated (failure) The original message was received at Tue, 25 May 1999 20:02:12 -0500 (CDT) from larch.cs.iastate.edu [129.186.3.5] ----- The following addresses had permanent fatal errors ----- ----- Transcript of session follows ----- 550 ... Host unknown (Name server: cs.istate.edu: host not found) Press C-c C-c here for "message/delivery-status" data Return-Path: Date: Tue, 25 May 1999 20:02:03 -0500 (CDT) From: "Gary T. Leavens" To: mdomo@cs.istate.edu CC: leavens@cs.iastate.edu subscribe jml-interest-list  -=- MIME -=-  This is a MIME-encapsulated message --UAA08928.927680534/css-1.cs.iastate.edu The original message was received at Tue, 25 May 1999 20:02:12 -0500 (CDT) from larch.cs.iastate.edu [129.186.3.5] ----- The following addresses had permanent fatal errors ----- ----- Transcript of session follows ----- 550 ... Host unknown (Name server: cs.istate.edu: host not found) --UAA08928.927680534/css-1.cs.iastate.edu Content-Type: message/delivery-status Reporting-MTA: dns; css-1.cs.iastate.edu Received-From-MTA: DNS; larch.cs.iastate.edu Arrival-Date: Tue, 25 May 1999 20:02:12 -0500 (CDT) Final-Recipient: RFC822; mdomo@cs.istate.edu Action: failed Status: 5.1.2 Remote-MTA: DNS; cs.istate.edu Last-Attempt-Date: Tue, 25 May 1999 20:02:14 -0500 (CDT) --UAA08928.927680534/css-1.cs.iastate.edu Content-Type: message/rfc822 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id UAA08927; Tue, 25 May 1999 20:02:12 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id UAA01158; Tue, 25 May 1999 20:02:03 -0500 (CDT) Date: Tue, 25 May 1999 20:02:03 -0500 (CDT) Message-Id: <199905260102.UAA01158@larch.cs.iastate.edu> From: "Gary T. Leavens" To: mdomo@cs.istate.edu CC: leavens@cs.iastate.edu subscribe jml-interest-list --UAA08928.927680534/css-1.cs.iastate.edu--  1,, Mail-from: From leavens@cs.iastate.edu Wed May 26 13:30:51 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id NAA07617; Wed, 26 May 1999 13:30:50 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id NAA10460; Wed, 26 May 1999 13:30:44 -0500 (CDT) Date: Wed, 26 May 1999 13:30:44 -0500 (CDT) Message-Id: <199905261830.NAA10460@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jgurney@cs.iastate.edu CC: leavens@cs.iastate.edu In-reply-to: <4.1.19990526090703.00a97780@imap.cs.iastate.edu> (message from Jason L Gurney on Wed, 26 May 1999 09:09:21 -0500) Subject: Re: Majordomo server error? *** EOOH *** Return-Path: Date: Wed, 26 May 1999 13:30:44 -0500 (CDT) From: "Gary T. Leavens" To: jgurney@cs.iastate.edu CC: leavens@cs.iastate.edu In-reply-to: <4.1.19990526090703.00a97780@imap.cs.iastate.edu> (message from Jason L Gurney on Wed, 26 May 1999 09:09:21 -0500) Subject: Re: Majordomo server error? Jason, I'm getting a failure, detailed below, when I try to subscribe myself. Is this something I did wrong? Gary Return-Path: Date: Tue, 25 May 1999 20:02:14 -0500 (CDT) From: Mail Delivery Subsystem To: MIME-Version: 1.0 Content-Type: multipart/report; report-type=delivery-status; boundary="UAA08928.927680534/css-1.cs.iastate.edu" Subject: Returned mail: Host unknown (Name server: cs.istate.edu: host not found) Auto-Submitted: auto-generated (failure) The original message was received at Tue, 25 May 1999 20:02:12 -0500 (CDT) from larch.cs.iastate.edu [129.186.3.5] ----- The following addresses had permanent fatal errors ----- ----- Transcript of session follows ----- 550 ... Host unknown (Name server: cs.istate.edu: host not found) Press C-c C-c here for "message/delivery-status" data Return-Path: Date: Tue, 25 May 1999 20:02:03 -0500 (CDT) From: "Gary T. Leavens" To: mdomo@cs.istate.edu CC: leavens@cs.iastate.edu subscribe jml-interest-list ^_ -=- MIME -=-  This is a MIME-encapsulated message --UAA08928.927680534/css-1.cs.iastate.edu The original message was received at Tue, 25 May 1999 20:02:12 -0500 (CDT) from larch.cs.iastate.edu [129.186.3.5] ----- The following addresses had permanent fatal errors ----- ----- Transcript of session follows ----- 550 ... Host unknown (Name server: cs.istate.edu: host not found) --UAA08928.927680534/css-1.cs.iastate.edu Content-Type: message/delivery-status Reporting-MTA: dns; css-1.cs.iastate.edu Received-From-MTA: DNS; larch.cs.iastate.edu Arrival-Date: Tue, 25 May 1999 20:02:12 -0500 (CDT) Final-Recipient: RFC822; mdomo@cs.istate.edu Action: failed Status: 5.1.2 Remote-MTA: DNS; cs.istate.edu Last-Attempt-Date: Tue, 25 May 1999 20:02:14 -0500 (CDT) --UAA08928.927680534/css-1.cs.iastate.edu Content-Type: message/rfc822 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id UAA08927; Tue, 25 May 1999 20:02:12 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id UAA01158; Tue, 25 May 1999 20:02:03 -0500 (CDT) Date: Tue, 25 May 1999 20:02:03 -0500 (CDT) Message-Id: <199905260102.UAA01158@larch.cs.iastate.edu> From: "Gary T. Leavens" To: mdomo@cs.istate.edu CC: leavens@cs.iastate.edu subscribe jml-interest-list --UAA08928.927680534/css-1.cs.iastate.edu--  1, answered,, Mail-from: From jgurney@cs.iastate.edu Wed May 26 14:02:31 1999 Return-Path: Received: from crow (crow.cs.iastate.edu [129.186.3.98]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with SMTP id OAA09161 for ; Wed, 26 May 1999 14:02:28 -0500 (CDT) Message-Id: <4.1.19990526140126.00a9aa70@imap.cs.iastate.edu> X-Sender: jgurney@imap.cs.iastate.edu X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Wed, 26 May 1999 14:02:20 -0500 To: "Gary T. Leavens" From: Jason L Gurney Subject: Re: Majordomo server error? In-Reply-To: <199905261830.NAA10460@larch.cs.iastate.edu> References: <4.1.19990526090703.00a97780@imap.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" *** EOOH *** Return-Path: X-Sender: jgurney@imap.cs.iastate.edu X-Mailer: QUALCOMM Windows Eudora Pro Version 4.1 Date: Wed, 26 May 1999 14:02:20 -0500 To: "Gary T. Leavens" From: Jason L Gurney Subject: Re: Majordomo server error? In-Reply-To: <199905261830.NAA10460@larch.cs.iastate.edu> References: <4.1.19990526090703.00a97780@imap.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Dave just caught the problem, the mail was sent to mdomo@cs.istate.edu (notice the missing 'a'). That should solve it. Jason At 01:30 PM 5/26/99 -0500, you wrote: >Jason, > >I'm getting a failure, detailed below, when I try to subscribe myself. >Is this something I did wrong? > > Gary > >Return-Path: >Date: Tue, 25 May 1999 20:02:14 -0500 (CDT) >From: Mail Delivery Subsystem >To: >MIME-Version: 1.0 >Content-Type: multipart/report; report-type=delivery-status; > boundary="UAA08928.927680534/css-1.cs.iastate.edu" >Subject: Returned mail: Host unknown (Name server: cs.istate.edu: host not >found) >Auto-Submitted: auto-generated (failure) > >The original message was received at Tue, 25 May 1999 20:02:12 -0500 (CDT) >from larch.cs.iastate.edu [129.186.3.5] > > ----- The following addresses had permanent fatal errors ----- > > > ----- Transcript of session follows ----- >550 ... Host unknown (Name server: cs.istate.edu: host >not found) > Press C-c C-c here for "message/delivery-status" data >Return-Path: >Date: Tue, 25 May 1999 20:02:03 -0500 (CDT) >From: "Gary T. Leavens" >To: mdomo@cs.istate.edu >CC: leavens@cs.iastate.edu > >subscribe jml-interest-list > -=- MIME -=- >This is a MIME-encapsulated message > >--UAA08928.927680534/css-1.cs.iastate.edu > >The original message was received at Tue, 25 May 1999 20:02:12 -0500 (CDT) >from larch.cs.iastate.edu [129.186.3.5] > > ----- The following addresses had permanent fatal errors ----- > > > ----- Transcript of session follows ----- >550 ... Host unknown (Name server: cs.istate.edu: host >not found) > >--UAA08928.927680534/css-1.cs.iastate.edu >Content-Type: message/delivery-status > >Reporting-MTA: dns; css-1.cs.iastate.edu >Received-From-MTA: DNS; larch.cs.iastate.edu >Arrival-Date: Tue, 25 May 1999 20:02:12 -0500 (CDT) > >Final-Recipient: RFC822; mdomo@cs.istate.edu >Action: failed >Status: 5.1.2 >Remote-MTA: DNS; cs.istate.edu >Last-Attempt-Date: Tue, 25 May 1999 20:02:14 -0500 (CDT) > >--UAA08928.927680534/css-1.cs.iastate.edu >Content-Type: message/rfc822 > >Return-Path: >Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) > by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id UAA08927; > Tue, 25 May 1999 20:02:12 -0500 (CDT) >Received: (from leavens@localhost) > by larch.cs.iastate.edu (8.9.0/8.9.0) id UAA01158; > Tue, 25 May 1999 20:02:03 -0500 (CDT) >Date: Tue, 25 May 1999 20:02:03 -0500 (CDT) >Message-Id: <199905260102.UAA01158@larch.cs.iastate.edu> >From: "Gary T. Leavens" >To: mdomo@cs.istate.edu >CC: leavens@cs.iastate.edu > >subscribe jml-interest-list > >--UAA08928.927680534/css-1.cs.iastate.edu--  1,, Mail-from: From leavens@cs.iastate.edu Wed May 26 14:39:11 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id OAA10758; Wed, 26 May 1999 14:39:10 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id OAA11320; Wed, 26 May 1999 14:39:03 -0500 (CDT) Date: Wed, 26 May 1999 14:39:03 -0500 (CDT) Message-Id: <199905261939.OAA11320@larch.cs.iastate.edu> From: "Gary T. Leavens" To: mdomo@cs.iastate.edu CC: leavens@cs.iastate.edu *** EOOH *** Return-Path: Date: Wed, 26 May 1999 14:39:03 -0500 (CDT) From: "Gary T. Leavens" To: mdomo@cs.iastate.edu CC: leavens@cs.iastate.edu subscribe jml-interest-list  1,, Mail-from: From owner-jml-interest-list@cs.iastate.edu Wed May 26 14:39:14 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id OAA10764; Wed, 26 May 1999 14:39:13 -0500 (CDT) Date: Wed, 26 May 1999 14:39:13 -0500 (CDT) Message-Id: <199905261939.OAA10764@css-1.cs.iastate.edu> To: leavens@cs.iastate.edu From: Majordomo@cs.iastate.edu Subject: Welcome to jml-interest-list Reply-To: Majordomo@cs.iastate.edu *** EOOH *** Return-Path: Date: Wed, 26 May 1999 14:39:13 -0500 (CDT) To: leavens@cs.iastate.edu From: Majordomo@cs.iastate.edu Subject: Welcome to jml-interest-list Reply-To: Majordomo@cs.iastate.edu -- Welcome to the jml-interest-list mailing list! Please save this message for future reference. Thank you. If you ever want to remove yourself from this mailing list, you can send mail to with the following command in the body of your email message: unsubscribe jml-interest-list or from another account, besides leavens@cs.iastate.edu: unsubscribe jml-interest-list leavens@cs.iastate.edu If you ever need to get in contact with the owner of the list, (if you have trouble unsubscribing, or have questions about the list itself) send email to . This is the general rule for most mailing lists when you need to contact a human. Here's the general information for the list you've subscribed to, in case you don't already have it: JML Interest Mailing List.  1,, Mail-from: From Majordomo-Owner@cs.iastate.edu Wed May 26 14:39:16 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id OAA10763; Wed, 26 May 1999 14:39:12 -0500 (CDT) Date: Wed, 26 May 1999 14:39:12 -0500 (CDT) Message-Id: <199905261939.OAA10763@css-1.cs.iastate.edu> To: leavens@cs.iastate.edu From: Majordomo@cs.iastate.edu Subject: Majordomo results Reply-To: Majordomo@cs.iastate.edu *** EOOH *** Return-Path: Date: Wed, 26 May 1999 14:39:12 -0500 (CDT) To: leavens@cs.iastate.edu From: Majordomo@cs.iastate.edu Subject: Majordomo results Reply-To: Majordomo@cs.iastate.edu -- >>>> subscribe jml-interest-list Succeeded.  1,, Mail-from: From leavens@cs.iastate.edu Wed May 26 14:39:50 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id OAA10830; Wed, 26 May 1999 14:39:49 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id OAA11324; Wed, 26 May 1999 14:39:42 -0500 (CDT) Date: Wed, 26 May 1999 14:39:42 -0500 (CDT) Message-Id: <199905261939.OAA11324@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jgurney@cs.iastate.edu CC: leavens@cs.iastate.edu In-reply-to: <4.1.19990526140126.00a9aa70@imap.cs.iastate.edu> (message from Jason L Gurney on Wed, 26 May 1999 14:02:20 -0500) Subject: Re: Majordomo server error? *** EOOH *** Return-Path: Date: Wed, 26 May 1999 14:39:42 -0500 (CDT) From: "Gary T. Leavens" To: jgurney@cs.iastate.edu CC: leavens@cs.iastate.edu In-reply-to: <4.1.19990526140126.00a9aa70@imap.cs.iastate.edu> (message from Jason L Gurney on Wed, 26 May 1999 14:02:20 -0500) Subject: Re: Majordomo server error? Jason, Thanks. Guess I was thinking of some other university (:->). Gary  1,, Mail-from: From owner-jml-interest-list Wed May 26 15:08:31 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id PAA11844 for jml-interest-list-outgoing; Wed, 26 May 1999 15:08:30 -0500 (CDT) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id PAA11840 for ; Wed, 26 May 1999 15:08:27 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id PAA11707; Wed, 26 May 1999 15:08:21 -0500 (CDT) Date: Wed, 26 May 1999 15:08:21 -0500 (CDT) Message-Id: <199905262008.PAA11707@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: test of JML interest list Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Return-Path: Date: Wed, 26 May 1999 15:08:21 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: test of JML interest list Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk This is a test, Gary  1,, Mail-from: From leavens@cs.iastate.edu Wed May 26 15:16:28 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id PAA12164; Wed, 26 May 1999 15:16:27 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id PAA11816; Wed, 26 May 1999 15:16:20 -0500 (CDT) Date: Wed, 26 May 1999 15:16:20 -0500 (CDT) Message-Id: <199905262016.PAA11816@larch.cs.iastate.edu> From: "Gary T. Leavens" To: Majordomo@cs.iastate.edu CC: leavens@cs.iastate.edu *** EOOH *** Return-Path: Date: Wed, 26 May 1999 15:16:20 -0500 (CDT) From: "Gary T. Leavens" To: Majordomo@cs.iastate.edu CC: leavens@cs.iastate.edu unsubscribe jml-interest-list  1,, Mail-from: From Majordomo-Owner@cs.iastate.edu Wed May 26 15:16:31 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id PAA12170; Wed, 26 May 1999 15:16:29 -0500 (CDT) Date: Wed, 26 May 1999 15:16:29 -0500 (CDT) Message-Id: <199905262016.PAA12170@css-1.cs.iastate.edu> To: leavens@cs.iastate.edu From: Majordomo@cs.iastate.edu Subject: Majordomo results Reply-To: Majordomo@cs.iastate.edu *** EOOH *** Return-Path: Date: Wed, 26 May 1999 15:16:29 -0500 (CDT) To: leavens@cs.iastate.edu From: Majordomo@cs.iastate.edu Subject: Majordomo results Reply-To: Majordomo@cs.iastate.edu -- >>>> unsubscribe jml-interest-list Succeeded.  1,, Mail-from: From leavens@cs.iastate.edu Wed May 26 15:18:12 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id PAA12235; Wed, 26 May 1999 15:18:10 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id PAA11825; Wed, 26 May 1999 15:18:03 -0500 (CDT) Date: Wed, 26 May 1999 15:18:03 -0500 (CDT) Message-Id: <199905262018.PAA11825@larch.cs.iastate.edu> From: "Gary T. Leavens" To: Majordomo@cs.iastate.edu CC: leavens@cs.iastate.edu *** EOOH *** Return-Path: Date: Wed, 26 May 1999 15:18:03 -0500 (CDT) From: "Gary T. Leavens" To: Majordomo@cs.iastate.edu CC: leavens@cs.iastate.edu subscribe jml-interest-list end  1,, Mail-from: From owner-jml-interest-list@cs.iastate.edu Wed May 26 15:18:15 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id PAA12241; Wed, 26 May 1999 15:18:14 -0500 (CDT) Date: Wed, 26 May 1999 15:18:14 -0500 (CDT) Message-Id: <199905262018.PAA12241@css-1.cs.iastate.edu> To: leavens@cs.iastate.edu From: Majordomo@cs.iastate.edu Subject: Welcome to jml-interest-list Reply-To: Majordomo@cs.iastate.edu *** EOOH *** Return-Path: Date: Wed, 26 May 1999 15:18:14 -0500 (CDT) To: leavens@cs.iastate.edu From: Majordomo@cs.iastate.edu Subject: Welcome to jml-interest-list Reply-To: Majordomo@cs.iastate.edu -- Welcome to the jml-interest-list mailing list! Please save this message for future reference. Thank you. If you ever want to remove yourself from this mailing list, you can send mail to with the following command in the body of your email message: unsubscribe jml-interest-list or from another account, besides leavens@cs.iastate.edu: unsubscribe jml-interest-list leavens@cs.iastate.edu If you ever need to get in contact with the owner of the list, (if you have trouble unsubscribing, or have questions about the list itself) send email to . This is the general rule for most mailing lists when you need to contact a human. Here's the general information for the list you've subscribed to, in case you don't already have it: JML Interest Mailing List.  1, filed,, Mail-from: From leavens@cs.iastate.edu Wed May 26 16:09:09 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id QAA14281; Wed, 26 May 1999 16:09:06 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id QAA12424; Wed, 26 May 1999 16:08:58 -0500 (CDT) Date: Wed, 26 May 1999 16:08:58 -0500 (CDT) Message-Id: <199905262108.QAA12424@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml@cs.iastate.edu, bart@cs.kun.nl, marieke@cs.kun.nl, joachim@cs.kun.nl, erikpoll@cs.kun.nl, gwdaughe@cca.rockwell.com (Gary_Daugherty), jgdaugh@cedar-rapids.net CC: leavens@cs.iastate.edu Subject: JML interest mailing list *** EOOH *** Return-Path: Date: Wed, 26 May 1999 16:08:58 -0500 (CDT) From: "Gary T. Leavens" To: jml@cs.iastate.edu, bart@cs.kun.nl, marieke@cs.kun.nl, joachim@cs.kun.nl, erikpoll@cs.kun.nl, gwdaughe@cca.rockwell.com (Gary_Daugherty), jgdaugh@cedar-rapids.net CC: leavens@cs.iastate.edu Subject: JML interest mailing list Hi, Bart (Jacobs) had urged me to set up a mailing list for discussions about JML. I've done that (with the help of the local systems people). If you'd like to subscribe, do the following. Users may subscribe by sending mail to Majordomo@cs.istate.edu with no subject and a body consisting of the first two non-blank lines below. subscribe jml-interest-list end You'll receive a confirmation and information about how to unsubscribe. We're planning to allow anyone who's subscribed to post to the list. You can post messages by sending mail to jml-interest-list@cs.iastate.edu Please let me know if you have any problems. Gary  1,, Mail-from: From leavens@cs.iastate.edu Wed May 26 17:37:32 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id RAA17327; Wed, 26 May 1999 17:37:31 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id RAA13390; Wed, 26 May 1999 17:37:23 -0500 (CDT) Date: Wed, 26 May 1999 17:37:23 -0500 (CDT) Message-Id: <199905262237.RAA13390@larch.cs.iastate.edu> From: "Gary T. Leavens" To: leavens@cs.iastate.edu CC: jml@cs.iastate.edu, bart@cs.kun.nl, marieke@cs.kun.nl, joachim@cs.kun.nl, erikpoll@cs.kun.nl, gwdaughe@cca.rockwell.com, jgdaugh@cedar-rapids.net, leavens@cs.iastate.edu In-reply-to: <199905262108.QAA12424@larch.cs.iastate.edu> (leavens@cs.iastate.edu) Subject: Re: JML interest mailing list *** EOOH *** Return-Path: Date: Wed, 26 May 1999 17:37:23 -0500 (CDT) From: "Gary T. Leavens" To: leavens@cs.iastate.edu CC: jml@cs.iastate.edu, bart@cs.kun.nl, marieke@cs.kun.nl, joachim@cs.kun.nl, erikpoll@cs.kun.nl, gwdaughe@cca.rockwell.com, jgdaugh@cedar-rapids.net, leavens@cs.iastate.edu In-reply-to: <199905262108.QAA12424@larch.cs.iastate.edu> (leavens@cs.iastate.edu) Subject: Re: JML interest mailing list Hi, > Users may subscribe by sending mail to Majordomo@cs.istate.edu with no > subject and a body consisting of the first two non-blank lines below. > > subscribe jml-interest-list > end Make sure you use the address Majordomo@cs.iastate.edu, not the one given above which is missing an "a". Sorry for the confusion. Gary  1,, Mail-from: From owner-jml-interest-list Thu May 27 14:26:34 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id OAA28524 for jml-interest-list-outgoing; Thu, 27 May 1999 14:26:31 -0500 (CDT) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id OAA28516; Thu, 27 May 1999 14:26:22 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id OAA24593; Thu, 27 May 1999 14:26:15 -0500 (CDT) Date: Thu, 27 May 1999 14:26:15 -0500 (CDT) Message-Id: <199905271926.OAA24593@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml@cs.iastate.edu, jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: Some proposed additions to JML syntax Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Return-Path: Date: Thu, 27 May 1999 14:26:15 -0500 (CDT) From: "Gary T. Leavens" To: jml@cs.iastate.edu, jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: Some proposed additions to JML syntax Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, I'm thinking about adding the following to JML. 1. A new specification "statement" because: ; to give reasons why some assertion follows from previous ones, as in: assert: x > 0; because: (* theory of integers *); assert: x >= 1; 2. Reverse implication, with syntax <== (to help in calculational reasoning). 3. Some way to do operator reduction over sets or arrays. For example, how would you currently specify, without using a model program, a method that takes an integer array and returns the sum of the elements in the array? Or their product? I'm thinking we could add something like: \+ (int i) [ a[i] | 0 <= i && i < a.length]; Another possibility is to have a class in our models directory with static methods for doing this sort of thing, so we could write: sum(a) But then, what's the specification of that method? (I guess a model program.) Comments? Gary P.S. Clyde checked in a new jml.g last night.  1, filed,, Mail-from: From leavens@cs.iastate.edu Fri May 28 11:35:54 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id LAA09670; Fri, 28 May 1999 11:35:53 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id LAA05236; Fri, 28 May 1999 11:35:48 -0500 (CDT) Date: Fri, 28 May 1999 11:35:48 -0500 (CDT) Message-Id: <199905281635.LAA05236@larch.cs.iastate.edu> From: "Gary T. Leavens" To: Bart.Jacobs@cs.kun.nl CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: <199905280843.KAA26590@pandora.cs.kun.nl> (message from Bart Jacobs on Fri, 28 May 1999 10:43:43 +0200) Subject: Re: JML-Interest: JML syntax *** EOOH *** Return-Path: Date: Fri, 28 May 1999 11:35:48 -0500 (CDT) From: "Gary T. Leavens" To: Bart.Jacobs@cs.kun.nl CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: <199905280843.KAA26590@pandora.cs.kun.nl> (message from Bart Jacobs on Fri, 28 May 1999 10:43:43 +0200) Subject: Re: JML-Interest: JML syntax Bart, > Here at Nijmegen we discussed the JML syntax as > proposed in Gary's mail of may 22. We are not > completely happy with the use of both : and \, > but we couldn't agree on what would be a better > solution: there seem to be conflicting requirements: > to have notation which is both similar to Java > (so that it will be accepted easily) and also different > to prevent conflicts. > > But we can all live with the proposed syntax. Yes, I agree that there are conflicting goals here, but we also couldn't think of a better solution for the syntax. I think we will go ahead with our compromise plan for the syntax then. (Indeed, we have already started doing that, but could have backed out if need be. :->) We are also getting the type checker working here, and I hope to have a release for you before I depart for vacation and Portugal (on June 3). I'll see you at ECOOP. Also, I did find that I may be able to get some small travel grants for collaboration from the US NSF to supplement my grant. I'm starting to work on the paperwork... > The three more recent additions to JML syntax look reasonable. Ok, although I'm still not sure what to do about summation and such. Is there some standard notation in PVS for doing operator reduction (like summing the elements of an array)? > If this language is going to be extended, > you may want to add a choose operator, which picks > an arbitrary element from a non-empty set/predicate. > It is present in most higher order languages of > theorem provers (PVS, Isabelle) If needed, one can restrict > the use of such operator to picking the element from > a singleton set. It is needed to talk about > ``the first element in an array such that ...'' As to the choose operator, if I understand you correctly, you mean getting an arbitrary element that satisfies some predicate. Would it be ok just to have a choose method in our model set types, or does it need to be an operator built-in to the language? I can see that it might need to be an operator, since as a method you'd have to pass an object with a method that implements the desired predicate... What kind of syntax is used in PVS and Isabelle for this? Also, to return to an earlier issue, what did you think of changing the syntax of \thrown(Type) to \exresult(Type)? You had objected that \throws and \thrown were too close for comfort before. Gary  1,, Mail-from: From leavens@cs.iastate.edu Fri May 28 20:01:09 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id UAA26976; Fri, 28 May 1999 20:01:08 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id UAA10263; Fri, 28 May 1999 20:00:58 -0500 (CDT) Date: Fri, 28 May 1999 20:00:58 -0500 (CDT) Message-Id: <199905290100.UAA10263@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: Protection from null in JML *** EOOH *** Return-Path: Date: Fri, 28 May 1999 20:00:58 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: Protection from null in JML Hi, In working on the rewrite of the preliminary design document for JML, I've been revising several specifictions. In doing this, I'm starting to notice two things. 1. many of our specifications don't protect against the values of (model) fields with reference types being null. 2. if you state that the value of a field can't be null in an invariant, that just obligates you to watch out for it in each of the postconditions in which you have the ability to modify that field. For example, here's the specification of Account from the preliminary design document, with suitable protection from the model fields credit and owner being null. -----------Account.jml---------------------------------------- package edu.iastate.cs.jml.docs.prelimdesign; public class Account { public model: USMoney credit; public model: String owner; public invariant: owner != null && credit != null && credit.greaterThanOrEqualTo(new USMoney(0)); public constraint: owner.equals(\old(owner)); public Account(MoneyOps amt, String own); normal_behavior: requires: own != null && amt != null && (new USMoney(1)).lessThanOrEqualTo(amt); modifiable: credit, owner; ensures: credit != null && credit.equals(amt) && owner != null && owner.equals(own); public /*@ pure: @*/ MoneyOps balance(); normal_behavior: ensures: \result.equals(credit); public void payInterest(double rate); normal_behavior: requires: 0.0 <= rate && rate <= 1.0; modifiable: credit; ensures: \old(credit.scaleBy(1.0 + rate)).equals(credit); normal_example: requires: rate == 0.05 && (new USMoney(4000)).equals(credit); ensures: (new USMoney(4200)).equals(credit); public void deposit(MoneyOps amt); normal_behavior: requires: amt != null && amt.greaterThanOrEqualTo(new USMoney(0)); modifiable: credit; ensures: credit != null && credit.equals(\old(credit).plus(amt)); normal_example: requires: credit.equals(new USMoney(40000)) && amt.equals(new USMoney(1)); ensures: credit != null && credit.equals(new USMoney(40001)); public void withdraw(MoneyOps amt); normal_behavior: requires: amt != null && (new USMoney(0)).lessThanOrEqualTo(amt) && amt.lessThanOrEqualTo(credit); modifiable: credit; ensures: credit != null && credit.equals(\old(credit).minus(amt)); normal_example: requires: credit.equals(new USMoney(40001)) && amt.equals(new USMoney(40000)); ensures: credit != null && credit.equals(new USMoney(1)); } -------------------------------------------------------------- You can see that the specification is fairly cluttered with the checking for null. Not only is this pretty distracting, but this seems to be pretty error-prone, as until today I didn't have these (necessary) checks in the specification (and it was written by me)! I don't think that one can easily be more clever about this. You can see in the specification of payInterest that one can use the equals method to check for null in some cases, but this isn't completely satisfactory, since that means that one has to write the thing being defined on the right side of ".equals" instead of the left, as seems to read better. Using a history constraint instead of an invariant doesn't help, as this also imposes an obligation to be proved, but what we want is to abbreviate something that goes in every postcondition. So I propose that we add to JML (yet another) clause, which I will call "assuming:" (suggestions for better names are welcome.) This would be like an invariant clause in its syntax, and in the sense that it would be assumed in data type induction proofs for preconditions. However, unlike an invariant an assumed predicate be available in proofs whenever needed; one could consider that it is implictly added to all postconditions of constructors and methods. In another sense, it's like a represents clause, which one can assume in proofs whenever needed. (My thinking is that we have that capability for concrete fields, why not extend it to abstract fields too?) Using this, one could write Account as follows. -----------proposed Account.jml--------------------------------- package edu.iastate.cs.jml.docs.prelimdesign; public class Account { public model: USMoney credit; public model: String owner; public assuming: owner != null && credit != null; // added ** public invariant: credit.greaterThanOrEqualTo(new USMoney(0)); public constraint: owner.equals(\old(owner)); public Account(MoneyOps amt, String own); normal_behavior: requires: own != null && amt != null // still need these && (new USMoney(1)).lessThanOrEqualTo(amt); modifiable: credit, owner; ensures: credit.equals(amt) && owner.equals(own); public /*@ pure: @*/ MoneyOps balance(); normal_behavior: ensures: \result.equals(credit); public void payInterest(double rate); normal_behavior: requires: 0.0 <= rate && rate <= 1.0; modifiable: credit; ensures: credit.equals(\old(credit.scaleBy(1.0 + rate))); normal_example: requires: rate == 0.05 && credit.equals(new USMoney(4000)); ensures: credit.equals(new USMoney(4200)); public void deposit(MoneyOps amt); normal_behavior: requires: amt != null && amt.greaterThanOrEqualTo(new USMoney(0)); modifiable: credit; ensures: credit.equals(\old(credit.plus(amt))); normal_example: requires: credit.equals(new USMoney(40000)) && amt.equals(new USMoney(1)); ensures: credit.equals(new USMoney(40001)); public void withdraw(MoneyOps amt); normal_behavior: requires: amt != null && (new USMoney(0)).lessThanOrEqualTo(amt) && amt.lessThanOrEqualTo(credit); modifiable: credit; ensures: credit.equals(\old(credit.minus(amt))); normal_example: requires: credit.equals(new USMoney(40001)) && amt.equals(new USMoney(40000)); ensures: credit.equals(new USMoney(1)); } -------------------------------------------------------------- Comments? Gary  1, answered,, Summary-line: 1-Jun joachim@barabas.cs.kun.nl [86] #JML-Interest: JML-Java question Mail-from: From owner-jml-interest-list Tue Jun 1 10:32:58 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id KAA05458 for jml-interest-list-outgoing; Tue, 1 Jun 1999 10:32:56 -0500 (CDT) Received: from barabas.cs.kun.nl (barabas.cs.kun.nl [131.174.33.77]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id KAA05454 for ; Tue, 1 Jun 1999 10:32:52 -0500 (CDT) Received: (from joachim@localhost) by barabas.cs.kun.nl (8.8.7/8.8.7) id RAA19252; Tue, 1 Jun 1999 17:32:45 +0200 From: Joachim van den Berg Message-Id: <199906011532.RAA19252@barabas.cs.kun.nl> Subject: JML-Interest: JML-Java question To: jml-interest-list@cs.iastate.edu Date: Tue, 1 Jun 1999 17:32:45 +0200 (CEST) Cc: joachim@cs.kun.nl Content-Type: text Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Return-Path: From: Joachim van den Berg Subject: JML-Interest: JML-Java question To: jml-interest-list@cs.iastate.edu Date: Tue, 1 Jun 1999 17:32:45 +0200 (CEST) Cc: joachim@cs.kun.nl Content-Type: text Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Dear Gary, et al, I am wondering how the Account.jml example you've send to the JML mailing list (May 28) can be translated into valid Java code. Below I've prefixed all JML statements with the annotation markers. A problem will arise how to translate this JML class. There are two options: 1. JML class --> Java abstract class 2. JML class --> Java interface The latter should be avoided, because a Java interface has no constructors. The former also is no valid translation, because each constructor should have a constructor body (and constructors cannot be declared abstract). Am I missing something? Joachim -- package edu.iastate.cs.jml.docs.prelimdesign; public abstract class Account { //@ public model: USMoney credit; //@ public model: String owner; //@ public invariant: owner != null && credit != null //@ && credit.greaterThanOrEqualTo(new USMoney(0)); //@ public constraint: owner.equals(\old(owner)); public Account(MoneyOps amt, String own); //@ normal_behavior: //@ requires: own != null && amt != null //@ && (new USMoney(1)).lessThanOrEqualTo(amt); //@ modifiable: credit, owner; //@ ensures: credit != null && credit.equals(amt) //@ && owner != null && owner.equals(own); public abstract /*@ pure: @*/ MoneyOps balance(); //@ normal_behavior: //@ ensures: \result.equals(credit); public abstract void payInterest(double rate); //@ normal_behavior: //@ requires: 0.0 <= rate && rate <= 1.0; //@ modifiable: credit; //@ ensures: \old(credit.scaleBy(1.0 + rate)).equals(credit); //@ normal_example: //@ requires: rate == 0.05 && (new USMoney(4000)).equals(credit); //@ ensures: (new USMoney(4200)).equals(credit); public abstract void deposit(MoneyOps amt); //@ normal_behavior: //@ requires: amt != null && amt.greaterThanOrEqualTo(new USMoney(0)); //@ modifiable: credit; //@ ensures: credit != null && credit.equals(\old(credit).plus(amt)); //@ normal_example: //@ requires: credit.equals(new USMoney(40000)) //@ && amt.equals(new USMoney(1)); //@ ensures: credit != null && credit.equals(new USMoney(40001)); public abstract void withdraw(MoneyOps amt); //@ normal_behavior: //@ requires: amt != null && (new USMoney(0)).lessThanOrEqualTo(amt) //@ && amt.lessThanOrEqualTo(credit); //@ modifiable: credit; //@ ensures: credit != null && credit.equals(\old(credit).minus(amt)); //@ normal_example: //@ requires: credit.equals(new USMoney(40001)) //@ && amt.equals(new USMoney(40000)); //@ ensures: credit != null && credit.equals(new USMoney(1)); }  1,, Summary-line: 1-Jun to: joachim@barabas.cs.ku [107] #Re: JML-Interest: JML-Java question Mail-from: From leavens@cs.iastate.edu Tue Jun 1 13:08:16 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id NAA11538; Tue, 1 Jun 1999 13:08:13 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id NAA21128; Tue, 1 Jun 1999 13:08:06 -0500 (CDT) Date: Tue, 1 Jun 1999 13:08:06 -0500 (CDT) Message-Id: <199906011808.NAA21128@larch.cs.iastate.edu> From: "Gary T. Leavens" To: joachim@barabas.cs.kun.nl CC: jml-interest-list@cs.iastate.edu, joachim@cs.kun.nl, leavens@cs.iastate.edu In-reply-to: <199906011532.RAA19252@barabas.cs.kun.nl> (message from Joachim van den Berg on Tue, 1 Jun 1999 17:32:45 +0200 (CEST)) Subject: Re: JML-Interest: JML-Java question *** EOOH *** Return-Path: Date: Tue, 1 Jun 1999 13:08:06 -0500 (CDT) From: "Gary T. Leavens" To: joachim@barabas.cs.kun.nl CC: jml-interest-list@cs.iastate.edu, joachim@cs.kun.nl, leavens@cs.iastate.edu In-reply-to: <199906011532.RAA19252@barabas.cs.kun.nl> (message from Joachim van den Berg on Tue, 1 Jun 1999 17:32:45 +0200 (CEST)) Subject: Re: JML-Interest: JML-Java question Dear Joachim, > I am wondering how the Account.jml example you've send to the > JML mailing list (May 28) can be translated into valid Java code. Below I've > prefixed all JML statements with the annotation markers. In general, if you give a declaration in JML, then the java code in a correct implementation should have the same declaration. > A problem will arise how to translate this JML class. There are two options: > 1. JML class --> Java abstract class > 2. JML class --> Java interface > > The latter should be avoided, because a Java interface has no > constructors. > > The former also is no valid translation, because each constructor should have > a constructor body (and constructors cannot be declared abstract). > > Am I missing something? Yes, since it's declared as a class, and not an abstract class or interface, you must use a class in the implementation, not an abstract class or interface. Just a regular class. In an implementation you have to provide code. A correct implementation might be as follows. Note, I had to change the type of the constructor, and some of the operations, due to binary method problems caused by the Java type system. Gary ---------------------------------------------------- package edu.iastate.cs.jml.docs.prelimdesign; //@ refine: "Account.jml"; public class Account { protected USMoney credit_; protected String owner_; //@ protected depends: credit -> credit_; //@ protected represents: credit -> credit == credit_; //@ protected depends: owner -> owner_; //@ protected represents: owner -> owner == owner_; //@ protected invariant: owner_ != null && credit_ != null; //@ protected invariant: redundantly //@ credit_.greaterThanOrEqualTo(new USMoney(0)); //@ protected constraint: redundantly owner_.equals(\old(owner_)); public Account(USMoney amt, String own) { //@ assume: own != null && amt != null //@ && (new USMoney(1)).lessThanOrEqualTo(amt); credit_ = amt; owner_ = own; } public /*@ pure: @*/ MoneyOps balance() { return credit_; } public void payInterest(double rate) { //@ assume: 0.0 <= rate && rate <= 1.0; credit_ = credit_.scaleBy(1.0 + rate); } public void deposit(MoneyOps amt) { //@ assume: amt != null && amt.greaterThanOrEqualTo(new USMoney(0)); credit_ = credit_.plus(amt); } public void withdraw(MoneyOps amt) { //@ assume: amt != null && (new USMoney(0)).lessThanOrEqualTo(amt) //@ && amt.lessThanOrEqualTo(credit_); credit_ = credit_.minus(amt); } }  1, filed, answered,, Mail-from: From joachim@barabas.cs.kun.nl Wed Jun 2 09:48:25 1999 Return-Path: Received: from barabas.cs.kun.nl (barabas.cs.kun.nl [131.174.33.77]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id JAA26771 for ; Wed, 2 Jun 1999 09:48:24 -0500 (CDT) Received: (from joachim@localhost) by barabas.cs.kun.nl (8.8.7/8.8.7) id QAA20233; Wed, 2 Jun 1999 16:48:17 +0200 From: Joachim van den Berg Message-Id: <199906021448.QAA20233@barabas.cs.kun.nl> Subject: question about the modifiable clause To: leavens@cs.iastate.edu Date: Wed, 2 Jun 1999 16:48:17 +0200 (CEST) Cc: joachim@cs.kun.nl Content-Type: text *** EOOH *** Return-Path: From: Joachim van den Berg Subject: question about the modifiable clause To: leavens@cs.iastate.edu Date: Wed, 2 Jun 1999 16:48:17 +0200 (CEST) Cc: joachim@cs.kun.nl Content-Type: text Dear Gary, I am trying to give semantics to the modifiable clause of JML. In your preliminary report (and in the LCPP manual) you state that if the modifiable (or modifies) clause is omitted, that no objects can have their state modified (page 7). This is in conflict with Leino's thesis. He states on page 97 : 'Without modifies clauses, a procedure would be able to modify anything, ...'. Can you explain why you have chosen another semantics, please ? Joachim  1,, Mail-from: From owner-jml-interest-list Wed Jun 2 13:27:06 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id NAA05517 for jml-interest-list-outgoing; Wed, 2 Jun 1999 13:27:05 -0500 (CDT) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id NAA05513; Wed, 2 Jun 1999 13:26:57 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id NAA04266; Wed, 2 Jun 1999 13:26:50 -0500 (CDT) Date: Wed, 2 Jun 1999 13:26:50 -0500 (CDT) Message-Id: <199906021826.NAA04266@larch.cs.iastate.edu> From: "Gary T. Leavens" To: joachim@barabas.cs.kun.nl CC: joachim@cs.kun.nl, jml-interest-list@cs.iastate.edu In-reply-to: <199906021448.QAA20233@barabas.cs.kun.nl> (message from Joachim van den Berg on Wed, 2 Jun 1999 16:48:17 +0200 (CEST)) Subject: JML-Interest: Re: question about the modifiable clause Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Return-Path: Date: Wed, 2 Jun 1999 13:26:50 -0500 (CDT) From: "Gary T. Leavens" To: joachim@barabas.cs.kun.nl CC: joachim@cs.kun.nl, jml-interest-list@cs.iastate.edu In-reply-to: <199906021448.QAA20233@barabas.cs.kun.nl> (message from Joachim van den Berg on Wed, 2 Jun 1999 16:48:17 +0200 (CEST)) Subject: JML-Interest: Re: question about the modifiable clause Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Dear Joachim, > I am trying to give semantics to the modifiable clause of JML. In your > preliminary report (and in the LCPP manual) you state that if the modifiable > (or modifies) clause is omitted, that no objects can have their state > modified (page 7). This is in conflict with Leino's thesis. He states on > page 97 : 'Without modifies clauses, a procedure would be able to modify > anything, ...'. > > Can you explain why you have chosen another semantics, please ? Mostly it's historical, as our semantics (in some sense) came first. But a large part of it derives from Leino's syntax, which allows any number of requires, modifies, and ensures clauses, and they aren't connected into specifications (behaviors) as in JML. But as a practical matter, if you have just one modifies clause, it had better include everything you can modify, or you have what is likely to be an unimplementable specification. You can also see both as just different defaults. In JML (and Larch/C++), the default is what we write in JML as modifiable: \nothing whereas in Leino's work, the default is modifiable: \everything. On the other hand, you have to be careful with infering things about procedures for which no specification is given. In Leino's work, the default modifies clause, has the right semantics. In JML, to reason about a procedure with a no specification, you have to imagine it has a specification like: behavior: modifiable: \everything; ensures: liberally true; (Again, this is related to the fact that we imagine that a whole specification is omitted, not just a modifiable clause.) As a language designer, I think the JML default goes the right way, however for 2 reasons. 1. The modifiable clause gives a permission to modify (actually, it's fields in JML, not objects, the preliminary design document was wrong), so if you aren't given premission, I think you shouldn't be able to do anything. 2. It's better for reasoning, since you get stronger specifications by default. With Leino's specifications, you have absolutely no frame condition that can help in reasoning if it's omitted. Gary  1,, Mail-from: From leavens@cs.iastate.edu Wed Jun 2 16:45:05 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id QAA13145; Wed, 2 Jun 1999 16:45:04 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id QAA08651; Wed, 2 Jun 1999 16:44:56 -0500 (CDT) Date: Wed, 2 Jun 1999 16:44:56 -0500 (CDT) Message-Id: <199906022144.QAA08651@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: Revised version of "Preliminary Design of JML" TR *** EOOH *** Return-Path: Date: Wed, 2 Jun 1999 16:44:56 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: Revised version of "Preliminary Design of JML" TR Hi, I've just released the revised version of the TR 98-06e (now), "Preliminary Design of JML". You can browse it on the web from the JML web site (http://www.cs.iastate.edu/~leavens/JML.html) or you can download the postscript (1+53 pages) from ftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/TR.ps.gz Comments are welcome, of course. This has the "because:" and "<==" operator, which we haven't implemented yet. I'm still hoping we'll have another "alpha" release before I leave for Europe tomorrow morning, but if not, Clyde Ruby will make a zip file available. Gary  1,, Mail-from: From leavens@cs.iastate.edu Wed Jun 2 17:24:10 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id RAA14667; Wed, 2 Jun 1999 17:24:09 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id RAA09145; Wed, 2 Jun 1999 17:24:01 -0500 (CDT) Date: Wed, 2 Jun 1999 17:24:01 -0500 (CDT) Message-Id: <199906022224.RAA09145@larch.cs.iastate.edu> From: "Gary T. Leavens" To: Peter.Mueller@FernUni-Hagen.de CC: leavens@cs.iastate.edu In-reply-to: <199905061511.RAA12840@sunpoet2.fernuni-hagen.de> (message from Peter Mueller on Thu, 6 May 1999 17:11:37 +0200) Subject: Re: Question about JML *** EOOH *** Return-Path: Date: Wed, 2 Jun 1999 17:24:01 -0500 (CDT) From: "Gary T. Leavens" To: Peter.Mueller@FernUni-Hagen.de CC: leavens@cs.iastate.edu In-reply-to: <199905061511.RAA12840@sunpoet2.fernuni-hagen.de> (message from Peter Mueller on Thu, 6 May 1999 17:11:37 +0200) Subject: Re: Question about JML Peter, You may want to sign up for the "jml-interest-list" email list. See http://www.cs.iastate.edu/~leavens/JML.html for instructions. Also, I've just released the revised version of the TR 98-06e (now), "Preliminary Design of JML". You can browse it on the web from the JML web site (http://www.cs.iastate.edu/~leavens/JML.html) or you can download the postscript (1+53 pages) from ftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/TR.ps.gz See you in Lisbon! I'm leaving tomorrow morning, so we may not be in email contact again before I see you there. Gary  1, filed, answered,, Mail-from: From Bart.Jacobs@cs.kun.nl Wed Jun 2 10:47:22 1999 Return-Path: Received: from pandora.cs.kun.nl (pandora.cs.kun.nl [131.174.33.4]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id KAA29161 for ; Wed, 2 Jun 1999 10:47:21 -0500 (CDT) Received: from hera.cs.kun.nl by pandora.cs.kun.nl via hera.cs.kun.nl [131.174.33.2] with ESMTP id RAA13250 (8.8.8/4.4); Wed, 2 Jun 1999 17:47:17 +0200 (MET DST) Message-Id: <199906021547.RAA13250@pandora.cs.kun.nl> X-Mailer: exmh version 2.0.3 3/22/1999 To: "Gary T. Leavens" cc: Bart.Jacobs@cs.kun.nl Subject: Re: JML syntax status In-reply-to: Your message of "Fri, 21 May 1999 12:44:15 CDT." <199905211744.MAA21238@ren.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Wed, 02 Jun 1999 17:47:17 +0200 From: Bart Jacobs *** EOOH *** Return-Path: X-Mailer: exmh version 2.0.3 3/22/1999 To: "Gary T. Leavens" cc: Bart.Jacobs@cs.kun.nl Subject: Re: JML syntax status In-reply-to: Your message of "Fri, 21 May 1999 12:44:15 CDT." <199905211744.MAA21238@ren.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Wed, 02 Jun 1999 17:47:17 +0200 From: Bart Jacobs Hi Gary, I have been a bit slow in replying to mails. > Woulud it be better to use \exresult(Type) instead of \thrown(Type)? > Perhaps that would be less confusing. Yes, that would be better. > Also, I did find that I may be able to get some small travel grants > for collaboration from the US NSF to supplement my grant. I'm > starting to work on the paperwork... I have made several phone calls here, but there seems to be nothing available for supporting the kind of cooperation we plan. So I guess I will have to do this with existing funds on this side. > Ok, although I'm still not sure what to do about summation and such. > Is there some standard notation in PVS for doing operator reduction > (like summing the elements of an array)? No, there is no standard operator. There should be more on this, but I cannot help you. > As to the choose operator, if I understand you correctly, you mean > getting an arbitrary element that satisfies some predicate. Would it > be ok just to have a choose method in our model set types, or does it > need to be an operator built-in to the language? I can see that it > might need to be an operator, since as a method you'd have to pass an > object with a method that implements the desired predicate... What > kind of syntax is used in PVS and Isabelle for this? Yes, I am thinking of a built-in operator. In PVS functional notation is used, to that choose(S) is a member of S, provided S is non-empty. The choice is ``deterministic'' in the sense that you can prove choose(S) = choose(S), by reflexivity. One could argue that the left and right hand sides might return different arguments. It can be avoided by letting choose only work (appropriately) on singleton sets. > So I propose that we add to JML (yet another) clause, which I will > call "assuming:" (suggestions for better names are welcome.) This > would be like an invariant clause in its syntax, and in the sense that > it would be assumed in data type induction proofs for preconditions. > However, unlike an invariant an assumed predicate be available in > proofs whenever needed; one could consider that it is implictly added > to all postconditions of constructors and methods. In another sense, > it's like a represents clause, which one can assume in proofs whenever > needed. (My thinking is that we have that capability for concrete > fields, why not extend it to abstract fields too?) The semantics of your assuming is not so clear to me. It is very important for verification to have all these != null statements. What about making ``owner != null && credit != null'' an abbreviation, say ``OCNN'' (for owner-credit-non-null), and put OCNN everywhere you need it. This has a clear semantics. What do you think? Have a nice holiday, and see you in Lisbon, Bart.  1, filed,, Mail-from: From owner-jml-interest-list Wed Jun 2 18:00:14 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id SAA16064 for jml-interest-list-outgoing; Wed, 2 Jun 1999 18:00:13 -0500 (CDT) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id SAA16060; Wed, 2 Jun 1999 18:00:05 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id RAA09481; Wed, 2 Jun 1999 17:59:57 -0500 (CDT) Date: Wed, 2 Jun 1999 17:59:57 -0500 (CDT) Message-Id: <199906022259.RAA09481@larch.cs.iastate.edu> From: "Gary T. Leavens" To: Bart.Jacobs@cs.kun.nl CC: Bart.Jacobs@cs.kun.nl, jml-interest-list@cs.iastate.edu In-reply-to: <199906021547.RAA13250@pandora.cs.kun.nl> (message from Bart Jacobs on Wed, 02 Jun 1999 17:47:17 +0200) Subject: JML-Interest: Re: JML syntax status Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Return-Path: Date: Wed, 2 Jun 1999 17:59:57 -0500 (CDT) From: "Gary T. Leavens" To: Bart.Jacobs@cs.kun.nl CC: Bart.Jacobs@cs.kun.nl, jml-interest-list@cs.iastate.edu In-reply-to: <199906021547.RAA13250@pandora.cs.kun.nl> (message from Bart Jacobs on Wed, 02 Jun 1999 17:47:17 +0200) Subject: JML-Interest: Re: JML syntax status Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Bart, > > Would it be better to use \exresult(Type) instead of \thrown(Type)? > > Perhaps that would be less confusing. > > Yes, that would be better. Ok, I'll introduce that syntax, and we'll phase out \thrown(Type), unless someone else objects. > > Ok, although I'm still not sure what to do about summation and such. > > Is there some standard notation in PVS for doing operator reduction > > (like summing the elements of an array)? > > No, there is no standard operator. There should be more on this, > but I cannot help you. Ok, we'll keep thinking about this. > > As to the choose operator, if I understand you correctly, you mean > > getting an arbitrary element that satisfies some predicate. Would it > > be ok just to have a choose method in our model set types, or does it > > need to be an operator built-in to the language? I can see that it > > might need to be an operator, since as a method you'd have to pass an > > object with a method that implements the desired predicate... What > > kind of syntax is used in PVS and Isabelle for this? > > Yes, I am thinking of a built-in operator. In PVS functional > notation is used, to that choose(S) is a member of S, provided > S is non-empty. The choice is ``deterministic'' in the sense > that you can prove choose(S) = choose(S), by reflexivity. One > could argue that the left and right hand sides might return > different arguments. It can be avoided by letting choose only > work (appropriately) on singleton sets. It sounds like we can just add a choose operation to the set types, so you can write S.choose() in JML. Does that seem right. More about assuming: later. See you in Lisbon. Gary  1,, Mail-from: From leavens@cs.iastate.edu Wed May 26 16:09:09 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id QAA14281; Wed, 26 May 1999 16:09:06 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id QAA12424; Wed, 26 May 1999 16:08:58 -0500 (CDT) Date: Wed, 26 May 1999 16:08:58 -0500 (CDT) Message-Id: <199905262108.QAA12424@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml@cs.iastate.edu, bart@cs.kun.nl, marieke@cs.kun.nl, joachim@cs.kun.nl, erikpoll@cs.kun.nl, gwdaughe@cca.rockwell.com (Gary_Daugherty), jgdaugh@cedar-rapids.net CC: leavens@cs.iastate.edu Subject: JML interest mailing list *** EOOH *** Return-Path: Date: Wed, 26 May 1999 16:08:58 -0500 (CDT) From: "Gary T. Leavens" To: jml@cs.iastate.edu, bart@cs.kun.nl, marieke@cs.kun.nl, joachim@cs.kun.nl, erikpoll@cs.kun.nl, gwdaughe@cca.rockwell.com (Gary_Daugherty), jgdaugh@cedar-rapids.net CC: leavens@cs.iastate.edu Subject: JML interest mailing list Hi, Bart (Jacobs) had urged me to set up a mailing list for discussions about JML. I've done that (with the help of the local systems people). If you'd like to subscribe, do the following. Users may subscribe by sending mail to Majordomo@cs.istate.edu with no subject and a body consisting of the first two non-blank lines below. subscribe jml-interest-list end You'll receive a confirmation and information about how to unsubscribe. We're planning to allow anyone who's subscribed to post to the list. You can post messages by sending mail to jml-interest-list@cs.iastate.edu Please let me know if you have any problems. Gary  1,, Mail-from: From owner-jml-interest-list Tue Jun 8 04:04:11 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id EAA11576 for jml-interest-list-outgoing; Tue, 8 Jun 1999 04:04:03 -0500 (CDT) Received: from pandora.cs.kun.nl (pandora.cs.kun.nl [131.174.33.4]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id EAA11572 for ; Tue, 8 Jun 1999 04:04:00 -0500 (CDT) Received: from hera.cs.kun.nl by pandora.cs.kun.nl via hera.cs.kun.nl [131.174.33.2] with SMTP for id LAA29141 (8.8.8/4.4); Tue, 8 Jun 1999 11:03:58 +0200 (MET DST) Date: Tue, 8 Jun 1999 11:03:58 +0200 (MET DST) From: Erik Poll To: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: Protection from null in JML In-Reply-To: <199905290100.UAA10263@larch.cs.iastate.edu> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Return-Path: Date: Tue, 8 Jun 1999 11:03:58 +0200 (MET DST) From: Erik Poll To: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: Protection from null in JML In-Reply-To: <199905290100.UAA10263@larch.cs.iastate.edu> MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi all, > 2. if you state that the value of a field can't be null in an invariant, > that just obligates you to watch out for it in each of the > postconditions in which you have the ability to modify that field. I don't get this. Why can't you just state that a (model) field are not null in the invariant ? Concretely, in the example > public class Account { > > public model: USMoney credit; > public model: String owner; > > public invariant: owner != null && credit != null > && credit.greaterThanOrEqualTo(new USMoney(0)); > > public Account(MoneyOps amt, String own); > normal_behavior: > requires: own != null && amt != null > && (new USMoney(1)).lessThanOrEqualTo(amt); > modifiable: credit, owner; > ensures: credit != null && credit.equals(amt) > && owner != null && owner.equals(own); I'd say that there is no reason to include credit != null and owner != null in the post-condition here, as it's already in the invariant. Cheers, Erik  1,, Mail-from: From leavens@cs.iastate.edu Sun Jun 20 09:45:09 1999 Return-Path: Received: from ren.cs.iastate.edu (leavens@ren.cs.iastate.edu [129.186.3.41]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id JAA08758; Sun, 20 Jun 1999 09:45:07 -0500 (CDT) Received: (from leavens@localhost) by ren.cs.iastate.edu (8.9.0/8.9.0) id JAA14007; Sun, 20 Jun 1999 09:45:04 -0500 (CDT) Date: Sun, 20 Jun 1999 09:45:04 -0500 (CDT) Message-Id: <199906201445.JAA14007@ren.cs.iastate.edu> From: "Gary T. Leavens" To: erikpoll@cs.kun.nl CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Tue, 8 Jun 1999 11:03:58 +0200 (MET DST)) Subject: Re: JML-Interest: Protection from null in JML *** EOOH *** Return-Path: Date: Sun, 20 Jun 1999 09:45:04 -0500 (CDT) From: "Gary T. Leavens" To: erikpoll@cs.kun.nl CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Tue, 8 Jun 1999 11:03:58 +0200 (MET DST)) Subject: Re: JML-Interest: Protection from null in JML Erik, et al, > Date: Tue, 8 Jun 1999 11:03:58 +0200 (MET DST) > From: Erik Poll > > > 2. if you state that the value of a field can't be null in an invariant, > > that just obligates you to watch out for it in each of the > > postconditions in which you have the ability to modify that field. > > I don't get this. Why can't you just state that a (model) field > are not null in the invariant ? Concretely, in the example > > > public class Account { > > > > public model: USMoney credit; > > public model: String owner; > > > > public invariant: owner != null && credit != null > > && credit.greaterThanOrEqualTo(new USMoney(0)); > > > > public Account(MoneyOps amt, String own); > > normal_behavior: > > requires: own != null && amt != null > > && (new USMoney(1)).lessThanOrEqualTo(amt); > > modifiable: credit, owner; > > ensures: credit != null && credit.equals(amt) > > && owner != null && owner.equals(own); > > I'd say that there is no reason to include credit != null and owner != null > in the post-condition here, as it's already in the invariant. > > Erik I think that this is a basic disagreement on the meaning of invariants. My interpretation is that an invariant is something you need to prove holds (i.e., you have to prove that it's preserved by all public methods and established by all constructors). I believe that you are saying that the invariant is an abbreviation. I think that we want to have both things in JML, a way to state properties that follow from the specification and a way to abbreviate properties that would otherwise have to be repeatedly mentioned. My understanding is tht the common name for the properties that follow (and would thus have to be proved in a verification to be preserved) is "invariant". What I'm proposing is that we have another clause for stating properties that are implicitly conjoined to pre and postconditions, which I'd call "assuming". Gary  1,, Mail-from: From leavens@cs.iastate.edu Fri Jun 25 14:16:03 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id OAA11737; Fri, 25 Jun 1999 14:16:02 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id OAA11456; Fri, 25 Jun 1999 14:15:54 -0500 (CDT) Date: Fri, 25 Jun 1999 14:15:54 -0500 (CDT) Message-Id: <199906251915.OAA11456@larch.cs.iastate.edu> From: "Gary T. Leavens" To: erikpoll@cs.kun.nl CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Thu, 24 Jun 1999 15:04:50 +0200 (MET DST)) Subject: Re: JML-Interest: invariant vs assuming *** EOOH *** Return-Path: Date: Fri, 25 Jun 1999 14:15:54 -0500 (CDT) From: "Gary T. Leavens" To: erikpoll@cs.kun.nl CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Thu, 24 Jun 1999 15:04:50 +0200 (MET DST)) Subject: Re: JML-Interest: invariant vs assuming Erik, I'm sorry for taking so long to respond to this, but I'm going to have to put it off for a few more days, as I've been fighting deadlines on papers and also working on getting out type checker for JML going. More about this later... Others should feel free to chip in. Gary > Date: Thu, 24 Jun 1999 15:04:50 +0200 (MET DST) > From: Erik Poll > MIME-Version: 1.0 > Content-Type: TEXT/PLAIN; charset=US-ASCII > Sender: owner-jml-interest-list@cs.iastate.edu > Precedence: bulk > > On Sun, 20 Jun 1999, Gary T. Leavens wrote: > > > I think that this is a basic disagreement on the meaning of invariants. > > Yes, there was: what all of us here think of as invariants are exactly > what you call "assuming" clauses. > > > I think that we want to have both things in JML > > Do we really need both ? We've been discussing invariant and assuming > clauses here in Nijmegen, and we can't really see the point in having > both. If we have assuming clauses, do we still need invariant clauses? > Can't we get by just using assuming clauses ? > > If one simply replaces "invariant" with "assuming" in a specification, > the specification becomes a bit weaker. (See example 2 below.) > However, we can't readily think of a situation where this would be > a problem. Are there cases where it is really essential to have an > invariant-clause, and an assuming-clause won't do ? > > If not, two advantages of dropping invariant-clauses would be: > > - The meaning of an assuming-clause seems to be conceptually simpler > than of an invariant-clause. > (The precise proof obligation for an invariant-clause is not quite > clear to me; see example 1 below.) > > - The notions of "invariant" and "assuming" are quite similar. > If we have both, many people won't grasp the difference and start > confusing them. > > Cheers, > Erik > > -------------------------------------------------------------- > > Example 1 > > Consider some class A, with invariant Inv and a method m > > public class A { > public invariant: Inv > .... > > public m(...) > requires Pre > modifiable x > ensures Post > > }; > > To prove that an implementation of m meets this specification we have > to prove > m may only modify x (i) > and > Pre before m => Post after m (ii) > > I'm a bit sloppy writing down (ii), but I guess it's clear what I mean. > > We also have to prove something for Inv. I see two possibilities: > > (a) prove for the implementation of m that > > (Pre /\ Inv) before m => Inv after m (iii(a)) > > (b) prove that for _any_ implementation of m > > (Pre /\ Inv) before m /\ (i) /\ (ii) => Inv after m (iii(b)) > > Which is correct ? > > I hope the difference between (a) and (b) is clear. iii(b) is a stronger > property than iii(a). To prove iii(b) we don't have to look at the > implementation of m, only at its specification. It seems to me that > in the Account-example, as well as the other examples in the JML-paper, > one can always prove this stronger property. Also, the description of > invariant in the Larch/C++ documentation suggests something along the > lines of iii(b), as it talks about invariants being 'redundant' in some > sense. > > -------------------------------------------------------------- > > Example 2 > > Now consider the class A', where we use "assuming" instead of "invariant": > > public class A' { > public assuming: Inv > .... > > public m(...) > requires Pre > modifiable x > ensures Post > > }; > > To prove that the method m of A' meets its specification we have to prove > > m may only modify x (i) > and > (Pre /\ Inv) before m => (Post /\ Inv) after m (ii') > > Now there is a difference between the proof obligation for A', i /\ ii', > and the proof obligation for A, ie. i /\ ii /\ iii(a). > > (The same thing holds if we take for iii(b) instead of iii(a)) > > To be precise, we have > ii /\ iii(a) => ii' > > and ii' => iii(a) > > but NOT ii' => ii > > So A is a stronger specification that A'. The easy way to see this > is that ii', unlike ii, does not say anything about what happens if > Inv does not hold before calling m. > > (If we take iii(b) instead of iii(a) then A will still be stronger > than A', since iii(b) is stronger than iii(a).) > > However, the difference between A and A' is small, and I can't easily > imagine a situation where it would be of interest. (I'd say that we're > never interested in what m does if the property Inv doesn't hold; so > the fact that A' is weaker than A is not important.) > > Can you think of a situation where you'd want to insist on the > stronger specification A instead of A' ? If not, there doesn't > seem to be much point in having both the notions of "invariant" > and "assuming", and only the latter would do. > >  1,, Mail-from: From leavens@cs.iastate.edu Thu Jul 1 00:08:53 1999 Return-Path: Received: from ren.cs.iastate.edu (leavens@ren.cs.iastate.edu [129.186.3.41]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id AAA07930; Thu, 1 Jul 1999 00:08:50 -0500 (CDT) Received: (from leavens@localhost) by ren.cs.iastate.edu (8.9.0/8.9.0) id AAA06620; Thu, 1 Jul 1999 00:08:44 -0500 (CDT) Date: Thu, 1 Jul 1999 00:08:44 -0500 (CDT) Message-Id: <199907010508.AAA06620@ren.cs.iastate.edu> From: "Gary T. Leavens" To: erikpoll@cs.kun.nl CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Thu, 24 Jun 1999 15:04:50 +0200 (MET DST)) Subject: Re: JML-Interest: invariant vs assuming *** EOOH *** Return-Path: Date: Thu, 1 Jul 1999 00:08:44 -0500 (CDT) From: "Gary T. Leavens" To: erikpoll@cs.kun.nl CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Thu, 24 Jun 1999 15:04:50 +0200 (MET DST)) Subject: Re: JML-Interest: invariant vs assuming Erik, (Sorry this has taken so long to answer. I have been trying to get a release of JML ready, I took a trip to Boston to see some family, and there were various deadlines on July 1.) Your analysis seems right to me. That is I think that we should just have an invariant: clause, and there doesn't seem to be any need to add assuming:. It seems clear that we first need to define the proof obligations for correctness of classes with invariants. I believe that your pointing me to the details in the Larch/C++ reference manual is a good thing, as I have somehow become confused about the meaning of invariant: clauses in JML. I agree now that they are essentially the same as what I had thought assuming: was for, and that we shouldn't have to write assertions that are redundant with invariants in pre and postconditions. My reading of the Larch/C++ manual, which I think matches what you were saying, is that, given a JML specification of the form: > public class A { > public invariant: Inv; > ... > public T m(...) behavior: > requires: Pre; > modifiable: x; > ensures: Post; > }; To prove that an implementation of the form public class A { ... public T m(...) { S; } } meets this specification we have to prove something like: S may modify at most x and its dependents (i) and Inv && Pre {S} Inv && Post (ii) where the notation "P {S} Q" is a Hoare-triple, which is the equivalent of the JML annotation: //@ assert Inv && Pre; S; //@ assert Inv && Post; (We should also prove termination, and also we can assume that the invariant holds for each object of type A.) This means, for example, if an invariant states that some field f is not null invariant: f != null; then we don't have to repeat that in the pre and postconditions of the public methods of the class. Comments? I'll try to revise our examples based on this... Gary  1, answered,, Mail-from: From owner-jml-interest-list Thu Jun 24 08:04:58 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id IAA15948 for jml-interest-list-outgoing; Thu, 24 Jun 1999 08:04:56 -0500 (CDT) Received: from pandora.cs.kun.nl (pandora.cs.kun.nl [131.174.33.4]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id IAA15944 for ; Thu, 24 Jun 1999 08:04:52 -0500 (CDT) Received: from hera.cs.kun.nl by pandora.cs.kun.nl via hera.cs.kun.nl [131.174.33.2] with SMTP for id PAA10353 (8.8.8/4.4); Thu, 24 Jun 1999 15:04:50 +0200 (MET DST) Date: Thu, 24 Jun 1999 15:04:50 +0200 (MET DST) From: Erik Poll To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: invariant vs assuming In-Reply-To: <199906201445.JAA14007@ren.cs.iastate.edu> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Return-Path: Date: Thu, 24 Jun 1999 15:04:50 +0200 (MET DST) From: Erik Poll To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: invariant vs assuming In-Reply-To: <199906201445.JAA14007@ren.cs.iastate.edu> MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk On Sun, 20 Jun 1999, Gary T. Leavens wrote: > I think that this is a basic disagreement on the meaning of invariants. Yes, there was: what all of us here think of as invariants are exactly what you call "assuming" clauses. > I think that we want to have both things in JML Do we really need both ? We've been discussing invariant and assuming clauses here in Nijmegen, and we can't really see the point in having both. If we have assuming clauses, do we still need invariant clauses? Can't we get by just using assuming clauses ? If one simply replaces "invariant" with "assuming" in a specification, the specification becomes a bit weaker. (See example 2 below.) However, we can't readily think of a situation where this would be a problem. Are there cases where it is really essential to have an invariant-clause, and an assuming-clause won't do ? If not, two advantages of dropping invariant-clauses would be: - The meaning of an assuming-clause seems to be conceptually simpler than of an invariant-clause. (The precise proof obligation for an invariant-clause is not quite clear to me; see example 1 below.) - The notions of "invariant" and "assuming" are quite similar. If we have both, many people won't grasp the difference and start confusing them. Cheers, Erik -------------------------------------------------------------- Example 1 Consider some class A, with invariant Inv and a method m public class A { public invariant: Inv .... public m(...) requires Pre modifiable x ensures Post }; To prove that an implementation of m meets this specification we have to prove m may only modify x (i) and Pre before m => Post after m (ii) I'm a bit sloppy writing down (ii), but I guess it's clear what I mean. We also have to prove something for Inv. I see two possibilities: (a) prove for the implementation of m that (Pre /\ Inv) before m => Inv after m (iii(a)) (b) prove that for _any_ implementation of m (Pre /\ Inv) before m /\ (i) /\ (ii) => Inv after m (iii(b)) Which is correct ? I hope the difference between (a) and (b) is clear. iii(b) is a stronger property than iii(a). To prove iii(b) we don't have to look at the implementation of m, only at its specification. It seems to me that in the Account-example, as well as the other examples in the JML-paper, one can always prove this stronger property. Also, the description of invariant in the Larch/C++ documentation suggests something along the lines of iii(b), as it talks about invariants being 'redundant' in some sense. -------------------------------------------------------------- Example 2 Now consider the class A', where we use "assuming" instead of "invariant": public class A' { public assuming: Inv .... public m(...) requires Pre modifiable x ensures Post }; To prove that the method m of A' meets its specification we have to prove m may only modify x (i) and (Pre /\ Inv) before m => (Post /\ Inv) after m (ii') Now there is a difference between the proof obligation for A', i /\ ii', and the proof obligation for A, ie. i /\ ii /\ iii(a). (The same thing holds if we take for iii(b) instead of iii(a)) To be precise, we have ii /\ iii(a) => ii' and ii' => iii(a) but NOT ii' => ii So A is a stronger specification that A'. The easy way to see this is that ii', unlike ii, does not say anything about what happens if Inv does not hold before calling m. (If we take iii(b) instead of iii(a) then A will still be stronger than A', since iii(b) is stronger than iii(a).) However, the difference between A and A' is small, and I can't easily imagine a situation where it would be of interest. (I'd say that we're never interested in what m does if the property Inv doesn't hold; so the fact that A' is weaker than A is not important.) Can you think of a situation where you'd want to insist on the stronger specification A instead of A' ? If not, there doesn't seem to be much point in having both the notions of "invariant" and "assuming", and only the latter would do.  1,, Mail-from: From leavens@cs.iastate.edu Fri Jul 2 21:15:54 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id VAA10046; Fri, 2 Jul 1999 21:15:51 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id VAA08737; Fri, 2 Jul 1999 21:15:41 -0500 (CDT) Date: Fri, 2 Jul 1999 21:15:41 -0500 (CDT) Message-Id: <199907030215.VAA08737@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu, Peter.Mueller@FernUni-Hagen.de, stata@pa.dec.com, rustan@pa.dec.com Subject: Release 1.0 of JML is now available *** EOOH *** Return-Path: Date: Fri, 2 Jul 1999 21:15:41 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu, Peter.Mueller@FernUni-Hagen.de, stata@pa.dec.com, rustan@pa.dec.com Subject: Release 1.0 of JML is now available Hi, There is now a release of JML, including a type checker, available from the web page for JML http://www.cs.iastate.edu/~leavens/JML.html or by anonymous ftp from ftp://ftp.cs.iastate.edu/pub/leavens/JML/ Please do let me know if you have trouble getting it, understanding what to do, or if it dies, doesn't work right, doesn't do what you want, is too painful to use, etc. This is what an alpha release is all about. Thanks to Clyde Ruby and especially to Anand Ganapathy for all their help on the software making up the release. Gary  1, forwarded,, Mail-from: From leavens@cs.iastate.edu Fri Jul 9 15:06:25 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id PAA02371; Fri, 9 Jul 1999 15:06:24 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id PAA13429; Fri, 9 Jul 1999 15:06:17 -0500 (CDT) Date: Fri, 9 Jul 1999 15:06:17 -0500 (CDT) Message-Id: <199907092006.PAA13429@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: Russell's paradox and set comprehensions in JML *** EOOH *** Return-Path: Date: Fri, 9 Jul 1999 15:06:17 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: Russell's paradox and set comprehensions in JML Hi, In the current release of JML, the model set types have a notion of "level" that is meant to try to avoid Russell's paradox. That is, we want to try to make the set comprhensions like the following illegal. JMLObjectSet r = new JMLObjectSet { JMLObjectSet s | s != null && !(s.has(s)) }; Because then r.has(r) can't be either true or false: - if r.has(r) were true, then r shouldn't be in r, by the characteristic predicate. - if r.has(r) were false, then r should be in r, by the characteristic predicate. (If you haven't seen this before, you may need to think about this a bit...) Now our scheme with levels was intended to desugar the above definition of r into something like: JMLObjectSet r = new JMLObjectSet { JMLObjectSet s | s.level <= 1 && s != null && !(s.has(s)) }; from which it would follow that r.has(r) is false, because the level of r would be 2. That seemed good at first, but Clyde Ruby was worried about it. In discussions with him, it came out that we could construct the following set, even with the levels... JMLObjectSet r2 = new JMLObjectSet { JMLObjectSequence s | s != null && s.length() == 1 && s.itemAt(0) instanceof JMLObjectSet && !( ((JMLObjectSet)(s.itemAt(0))) .has(s.itemAt(0)) ) } Then you have the problematic formula: r2.has(new JMLObjectSequence(r2)) which you can also argue can't be either true or false. Well, this is pretty unsatisfactory. (Especially since I've been complaining in public about Russell's paradox and the OCL :->). What to do? One alternative is the version of set theory promoted by von Neuman, Bernays, and Goedel. In this version set comprehensions would not yield sets at all; rather they would yield "meta-sets" (called "classes", classically :->). Meta-sets would not be considered to be Java objects. The problem with this is that JML is heavily biased towards having mathematics objects reified as Java objects, and this would be an exception. Because of that, we'd have to add several more kinds of expressions and types... which seems like too much work and irregular to boot. So we rejected this alternative. Instead, we propose to adopt the ZF solution, namely to only allow set comprehensions that filter other sets. That is, the syntax of a set comprehension would be roughly: new { | . has ( ) && } for example, one could write new JMLObjectSet { Integer x | myIntegerSet.has(x) && even(x) } (assuming myIntegerSet and even are defined appropriately). The type of the would have to be the same as the given, and the used would be the same as the one declared in the . Of course, this poses a problem in constructing big sets. We plan to get around this by doing two things: - having some statically defined big sets, like the set of all Integer objects as predefined static fields in the set classes. (Of course, we can't have any sets that are too big, like the set of all JMLObjectSets! So we have to limit these to just sets of atomic values, like integers, characters, although strings seem okay.) - Adding some operations, like cartesian product, to sets that seem necessary to gain the ability to construct larger sets from smaller ones. (We should also add the choose operation at the same time to sets.) Comments? Gary  1, answered,, Mail-from: From erikpoll@cs.kun.nl Thu Jul 15 07:24:50 1999 Return-Path: Received: from pandora.cs.kun.nl (pandora.cs.kun.nl [131.174.33.4]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id HAA24512 for ; Thu, 15 Jul 1999 07:24:49 -0500 (CDT) Received: from hera.cs.kun.nl by pandora.cs.kun.nl via hera.cs.kun.nl [131.174.33.2] with SMTP for id OAA28072 (8.8.8/4.4); Thu, 15 Jul 1999 14:24:25 +0200 (MET DST) Date: Thu, 15 Jul 1999 14:24:25 +0200 (MET DST) From: Erik Poll To: "Gary T. Leavens" Subject: Re: JML-Interest: Russell's paradox and set comprehensions in JML In-Reply-To: <199907092006.PAA13429@larch.cs.iastate.edu> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII *** EOOH *** Return-Path: Date: Thu, 15 Jul 1999 14:24:25 +0200 (MET DST) From: Erik Poll To: "Gary T. Leavens" Subject: Re: JML-Interest: Russell's paradox and set comprehensions in JML In-Reply-To: <199907092006.PAA13429@larch.cs.iastate.edu> MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII > Instead, we propose to adopt the ZF solution, namely to only allow set > comprehensions that filter other sets. That is, the syntax of a > .. .. .. > Comments? No comments really. We talked about it here and your proposal seems to be the sensible thing to do. Erik  1,, Mail-from: From leavens@cs.iastate.edu Thu Jul 15 11:50:30 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id LAA28456; Thu, 15 Jul 1999 11:50:29 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id LAA11491; Thu, 15 Jul 1999 11:50:23 -0500 (CDT) Date: Thu, 15 Jul 1999 11:50:23 -0500 (CDT) Message-Id: <199907151650.LAA11491@larch.cs.iastate.edu> From: "Gary T. Leavens" To: erikpoll@cs.kun.nl CC: leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Thu, 15 Jul 1999 14:24:25 +0200 (MET DST)) Subject: Re: JML-Interest: Russell's paradox and set comprehensions in JML *** EOOH *** Return-Path: Date: Thu, 15 Jul 1999 11:50:23 -0500 (CDT) From: "Gary T. Leavens" To: erikpoll@cs.kun.nl CC: leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Thu, 15 Jul 1999 14:24:25 +0200 (MET DST)) Subject: Re: JML-Interest: Russell's paradox and set comprehensions in JML Eric, Ok, thanks, for letting me know. We are going ahead with it then. Gary  1,, Mail-from: From owner-jml-interest-list Mon Jul 19 21:25:12 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id VAA05079 for jml-interest-list-outgoing; Mon, 19 Jul 1999 21:25:08 -0500 (CDT) Received: from ren.cs.iastate.edu (leavens@ren.cs.iastate.edu [129.186.3.41]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id VAA05075 for ; Mon, 19 Jul 1999 21:25:06 -0500 (CDT) Received: (from leavens@localhost) by ren.cs.iastate.edu (8.9.0/8.9.0) id VAA15441; Mon, 19 Jul 1999 21:25:01 -0500 (CDT) Date: Mon, 19 Jul 1999 21:25:01 -0500 (CDT) Message-Id: <199907200225.VAA15441@ren.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: Grammar changes to JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Return-Path: Date: Mon, 19 Jul 1999 21:25:01 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: Grammar changes to JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, We're planning to change the grammar for nondeterministic if statements (part of the refinement calculus). Formerly, the grammar was as follows. if { assume: P1; S1; } || { assume P2; S2; } else { S3 } we plan to change it to the following, so that it will be clearer as a statement and distinct from the usual if. if: { assume: P1; S1 } or: { assume: P2; S2 } else: { assume: P3; S3 } We are also planning to add keywords initializer: and static_initializer: to the language, to allow one to specify the effect of the Java (1.1) initializer and static initalizer blocks. Comments? Gary  1, answered,, Mail-from: From joachim@cicero.cs.kun.nl Fri Jul 30 02:42:29 1999 Return-Path: Received: from cicero.cs.kun.nl (cicero.cs.kun.nl [131.174.33.247]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id CAA21907 for ; Fri, 30 Jul 1999 02:42:27 -0500 (CDT) Received: from localhost (joachim@localhost) by cicero.cs.kun.nl (8.9.3/8.9.3) with ESMTP id JAA05321 for ; Fri, 30 Jul 1999 09:42:06 +0200 Date: Fri, 30 Jul 1999 09:42:06 +0200 (CEST) From: Joachim van den Berg To: "Gary T. Leavens" Subject: questions about the JML grammar (fwd) Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII *** EOOH *** Return-Path: Date: Fri, 30 Jul 1999 09:42:06 +0200 (CEST) From: Joachim van den Berg To: "Gary T. Leavens" Subject: questions about the JML grammar (fwd) MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Hi Gary, I'll only send a copy to you. Maybe it is confusing to post this on the JML interest list twice. Joachim ---------- Forwarded message ---------- Date: Wed, 21 Jul 1999 05:03:26 +0200 (CEST) From: Joachim van den Berg To: jml-interest-list@cs.iastate.edu Subject: questions about the JML grammar Dear Gary, et al, I would like to discuss some grammar rules that I don't understand. I have some questions about the grammar as it is in the preliminary design paper, version TR #98-06f. * On page 42, the production rule history_constraint is defined as: history_constraint ::= constraint: [ redundantly ] predicate [ for: constrained-set ] ; constrained-set ::= | method-name [ , method-name ]* | \everything What I don't understand about these rules is why a constrained set is defined in terms of method-names (which includes identifiers), and not in terms of identifiers only. I have searched for an example where you use this constrained set, but I couldn't find it. * On page 43 the production rules spec-case and spec-case-seq are defined. According to these definitions you can write (weird?) behavior specifications like: behavior: requires: true; { requires: true; ensures: true; } Is this what you want? I would propose the following production rules: spec-case-seq ::= | { spec-case-seq } | spec-case-seq also: spec-case | spec-case spec-case ::= | [ model-var-decl ]* [ requires-clause ]* [ measured-clause ]* [ when-clause ]* [ modifiable-clause ]* ensures-clause [ ensures-clause ]* where you exclude these kind of examples. * On page 43 the production rules model-var-decl and decl-pred. Due to these production rules is the initially production rule (used in production rule field on page 41) redundant. You have already removed it in the electronic version. * On page 47 in production rule specification-statement Are the non-terminals behavior and invariant necessary? With this rule you can write examples like: void m () { if (true) { //@ behavior: //@ ensures: true; return; } } Again, is this what you want? And if this is what you want, can you explain its semantics. That's it for now. Thanks in advance, Joachim  1,, Mail-from: From owner-jml-interest-list Fri Jul 30 11:08:00 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id LAA27632 for jml-interest-list-outgoing; Fri, 30 Jul 1999 11:07:56 -0500 (CDT) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id LAA27628; Fri, 30 Jul 1999 11:07:51 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id LAA14831; Fri, 30 Jul 1999 11:07:45 -0500 (CDT) Date: Fri, 30 Jul 1999 11:07:45 -0500 (CDT) Message-Id: <199907301607.LAA14831@larch.cs.iastate.edu> From: "Gary T. Leavens" To: joachim@cicero.cs.kun.nl CC: jml-interest-list@cs.iastate.edu In-reply-to: (message from Joachim van den Berg on Fri, 30 Jul 1999 09:42:06 +0200 (CEST)) Subject: JML-Interest: Re: questions about the JML grammar (fwd) Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Return-Path: Date: Fri, 30 Jul 1999 11:07:45 -0500 (CDT) From: "Gary T. Leavens" To: joachim@cicero.cs.kun.nl CC: jml-interest-list@cs.iastate.edu In-reply-to: (message from Joachim van den Berg on Fri, 30 Jul 1999 09:42:06 +0200 (CEST)) Subject: JML-Interest: Re: questions about the JML grammar (fwd) Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Dear Joachim, et al, Sorry, Joachim, I really didn't see this before... > I would like to discuss some grammar rules that I don't understand. I have > some questions about the grammar as it is in the preliminary design paper, > version TR #98-06f. > > > * On page 42, the production rule history_constraint is defined as: > > history_constraint ::= > constraint: [ redundantly ] predicate [ for: constrained-set ] ; > > constrained-set ::= > | method-name [ , method-name ]* > | \everything > > What I don't understand about these rules is why a constrained set is > defined in terms of method-names (which includes identifiers), and not > in terms of identifiers only. I have searched for an example where you > use this constrained set, but I couldn't find it. Clyde and I were just changing that grammar (and the one for callable clauses) yesterday to be as you suggest. The new grammar will be: history-constraint ::= constraint: [ redundantly ] predicate [ for: constrained-list ] ; constrained-list ::= method-name-list | \everything method-name-list ::= method-name [ , method-name ] ... method-name ::= method-ref [ ( [ param-disambig-list ] ) ] method-ref ::= method-ref-start [ . ident ] ... method-ref-start ::= ident | this | super callable-clause ::= callable: [ redundantly ] callable-methods-list ; callable-methods-list ::= method-name-list | \everything | \nothing Clyde is working on some real examples that use this... > * On page 43 the production rules spec-case and spec-case-seq are defined. > According to these definitions you can write (weird?) behavior > specifications like: > > behavior: > requires: true; > { > requires: true; > ensures: true; > } > > Is this what you want? Yes, this is really what we want. Here's a good example. public Object getItem(Object item) throws JMLListException; normal_behavior: requires: has(item); { requires: item != null; ensures: \result == (itemAt(indexOf(item))); also: requires: item == null; ensures: \result == null; } exceptional_behavior: requires: !has(item); ensures: \throws(JMLListException); Without having requires clauses that spans several cases, you'd have to repeat the requires clause (in this case, has(item)) several times, in each case. One should view this as syntactic sugar, however. So in a parser, you might expand this abbreviation before proceeding to type checking or semantic processing. > * On page 43 the production rules model-var-decl and decl-pred. > Due to these production rules is the initially production rule (used in > production rule field on page 41) redundant. You have already removed it > in the electronic version. Yes, initially will no longer be a separate clause. > * On page 47 in production rule specification-statement > Are the non-terminals behavior and invariant necessary? > With this rule you can write examples like: > > void m () { > if (true) { > //@ behavior: > //@ ensures: true; > return; > } > } > > Again, is this what you want? And if this is what you want, can you > explain its semantics. Ok, the behavior is the most fundamental specification statement. In general, the form: behavior: requires: P; modifiable: x, y; ensures: Q; means that, if P holds at the point of execution, then the statment transforms the state, by possibly modifying the variables named in the modifiable clause (x, y in this schematic example) to make the predicate Q hold. As a proof obligation, it means that in a correct implementation, some statement has to go there that achieves this effect (i.e., that refines this specification). This is inspired by the refinement calculus. Another way to look at it is, that wp. behavior: requires: P; modifiable: x, y; ensures: Q; .R is P, if Q ==> R. The invariant as a specification statement means that the given assertion is to hold for the remainder of its scope. It is sugar for repeating that assertion after every following statement in its scope. We're hoping to make another release soon... Gary  1,, Mail-from: From leavens@cs.iastate.edu Mon Aug 9 15:43:24 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id PAA11934; Mon, 9 Aug 1999 15:43:22 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id PAA07767; Mon, 9 Aug 1999 15:43:14 -0500 (CDT) Date: Mon, 9 Aug 1999 15:43:14 -0500 (CDT) Message-Id: <199908092043.PAA07767@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: instance: keyword in JML *** EOOH *** Return-Path: Date: Mon, 9 Aug 1999 15:43:14 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: instance: keyword in JML Hi, We're adding a keyword, "instance:", to JML so that in the declaration of interfaces, one can declare fields that are supposed to be in implementations of the interface. These would have to be model: fields, as Java assumes that all fields (that are not methods), declared in an interface are static. The idea of the "instance:" keyword is to allow one to cancel this implicit staticness of a field in an interface. Here's an example. In the following, the field MAX_SIZE is implicitly static (and public), but because size is declared as instance:, it acts like a non-static field (an instance variable). package edu.iastate.cs.jml.samples.stacks; public interface BoundedThing { //@ model: int MAX_SIZE; // implicitly static //@ model: instance: int size; //@ invariant: MAX_SIZE > 0 && 0 <= size && size <= MAX_SIZE; //@ constraint: MAX_SIZE == \old(MAX_SIZE); int getSizeLimit(); //@ normal_behavior: //@ ensures: \result == MAX_SIZE; boolean isEmpty( ); //@ normal_behavior: //@ ensures: \result <==> size == 0; boolean isFull(); //@ normal_behavior: //@ ensures: \result <==> size == MAX_SIZE; Object clone () throws CloneNotSupportedException; //@ behavior: //@ ensures: \returns ==> \result instanceof BoundedThing //@ && size == ((BoundedThing)\result).size; } Comments? Gary  1,, Mail-from: From leavens@cs.iastate.edu Tue Aug 10 16:14:02 1999 Return-Path: Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id QAA01389; Tue, 10 Aug 1999 16:14:02 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id QAA18896; Tue, 10 Aug 1999 16:13:53 -0500 (CDT) Date: Tue, 10 Aug 1999 16:13:53 -0500 (CDT) Message-Id: <199908102113.QAA18896@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: Adding summations and other reductions to JML, bag comprehensions *** EOOH *** Return-Path: Date: Tue, 10 Aug 1999 16:13:53 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: Adding summations and other reductions to JML, bag comprehensions Hi, Just a note to let you know some things we're thinking about here, and to try to solicit some input. In JML, we are would like to be able to succinctly say something like, the sum of all integers satisfying some predicate, or the sum from i = 1 to n of some formula. There isn't a good way to do this currently, except by writing a model method. Similarly, we are adding bags (multisets) to the model types. Is there some good notation for the equivalent of set comprehensions for bags? I believe in Z bags are thought of as integer-valued functions and so a bag comprehension is written as a lambda-expression. Do we want that in JML? Gary  1,, Mail-from: From owner-jml-interest-list Fri Aug 13 16:21:49 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id QAA25509 for jml-interest-list-outgoing; Fri, 13 Aug 1999 16:21:38 -0500 (CDT) Received: from larch.cs.iastate.edu (larch.cs.iastate.edu [129.186.3.5]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id QAA25504; Fri, 13 Aug 1999 16:21:32 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id QAA00759; Fri, 13 Aug 1999 16:21:24 -0500 (CDT) Date: Fri, 13 Aug 1999 16:21:24 -0500 (CDT) Message-Id: <199908132121.QAA00759@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: New release of JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Return-Path: Date: Fri, 13 Aug 1999 16:21:24 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: New release of JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, I've made a new release of JML, 1.1, which is available from the ftp directory ftp://ftp.cs.iastate.edu/pub/leavens/JML/ The release files don't have the antlr subdirectory in them; this is sufficient for running the checker, but (I think) not for recreating it. Let me know if that, or anything else, causes problems. The document and examples have all been updated. See the file BUGS.txt in the top directory of the release for the outstanding bugs (of which there are several). Gary  1,, Mail-from: From leavens@cs.iastate.edu Wed Aug 18 22:36:02 1999 Return-Path: Received: from ren.cs.iastate.edu (leavens@ren.cs.iastate.edu [129.186.3.41]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id WAA19002; Wed, 18 Aug 1999 22:36:00 -0500 (CDT) Received: (from leavens@localhost) by ren.cs.iastate.edu (8.9.0/8.9.0) id WAA17093; Wed, 18 Aug 1999 22:35:55 -0500 (CDT) Date: Wed, 18 Aug 1999 22:35:55 -0500 (CDT) Message-Id: <199908190335.WAA17093@ren.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu, jml@cs.iastate.edu CC: leavens@cs.iastate.edu, stata@pa.dec.com, rustan@pa.dec.com Subject: Possible changes to the JML grammar, comments and reaction sought *** EOOH *** Return-Path: Date: Wed, 18 Aug 1999 22:35:55 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu, jml@cs.iastate.edu CC: leavens@cs.iastate.edu, stata@pa.dec.com, rustan@pa.dec.com Subject: Possible changes to the JML grammar, comments and reaction sought Hi, I'm spending the week at Compaq SRC in Palo Alto trying to see if we can merge our specification language JML with the annotation language ESC/Java developed here at SRC. The advantage is to allow for a wider range of tools that might be able to usefully use the JML syntax. ESC/Java, as you may know, has a pretty powerful lint-like static checker. We are developing a proposal to change both languages. I'll give you the part that affects JML below. (ESC/Java is also agreeing to make many changes, but I won't list those here, as they would be of less interest to you.) I'm very interested in your reactions to each of these potential changes. Especially I'd like to hear from the people in Nijmegen about them (if you're not on vacation as I write this...), and from Al Baker. Here's a brief description of the proposed changes to JML. - ESC/Java requires a whole syntactic construct in a //@ comment, whereas in JML the construct can be split over multiple lines. In JML, //@ is simply ignored by the JML parser, as are /*@ and @*/. (This would solve the problem Joachim pointed out about the brackets, incidently.) JML would be changed to be like ESC in this respect. - JML uses keywords that end with a colon (:) for the most part, e.g., "requires:" and "ensures:" vs. ESC/Java's "requires" and "ensures". This is to simplify the parser and avoid reserving too many Java identifiers. JML be changed to eliminate these colons and to only recognize these keywords within annotations and outside of pred-expressions. (I have tested this, and it would work.) - ESC/Java has .spec files with the annotation syntax - Currently, JML allows method specifications to appear after the end of a method signature, including the semicolon in an interface. public int foo(); normal_be