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_behavior: ensures ...; In ESC/Java, such specications may come before the method signature, or before the semicolon. JML would change this to follow ESC/Java. - ESC/Java has expressions made with type, typeof, elemtype, and <: JML will add \type, \typeof, \elemtype, and <: - ESC/Java has LBLNEG and LBLPOS for labeling assertions. JML will add \lblneg and \lblpos - ESC/Java has "spec_public" as a modifier, JML will add this. - ESC/Java has an "axiom" pragma. JML will add axiom declarations in places where declarations are permitted. - ESC/Java has "defined_if" and "uninitialized" pragmas for declarations. JML will add these. - JML will no longer permit specification statements other than assert, assume, and (the new) set inside Java implementations. - In ESC/Java, exceptions can be specified using exsures clauses. This would be added to JML. - In ESC/Java one can use "also_modifies" to state variables that can be modified by a subclass. This will be added to JML as a sugar for "modifiable redundantly". (The check would be that these do follow from the dependencies declared.) - In ESC/Java, a requires clause alone can be a specification. This would be added to JML. - JML uses the declaration attribute "model", which can be used to declare abstract, specification-only variables that can depend on concrete variables. ESC/Java has "ghost" which are concrete, specification-only variables. These seem to be scoped differently, as in JML the scope of a model declaration is exactly the same as for a normal Java declaration, but this is not the case for ESC/Java ghost variables. ESC/Java uses a set statement pragma to assign to ghost variables, but in JML there are no special constructs for assigning to model variables. JML will change to mark the abstract model variables declarations as "dependent", and reserve plain "model" variables for ghost variables. (ESC/Java will drop "ghost" in favor of "model".) JML will add a set statement with syntax like: set var = expr; . - JML currently uses the notation \forall (T1 x1, x2; T3 x3) [ pred(x1, x2, x3) ] for universal quantification. ESC/Java uses (forall T1 x1, x2; (forall T3 x3; pred(x1, x2, x3) )) for this. Similarly for existential quantification. We will both change to (\forall T1 x1, x2; T3 x3; pred(x1, x2, x3) ) assuming this can be parsed easily. - ESC/Java has "elemsnonnull" for arrays. JML will add \elemsnonnull. [[[Could it be \non_null_elements instead?]]] - ESC/Java has LS, LS[], classlock, monitored_by, and monitored for dealing with threads. JML will add \ls [[[could it be \lock_set?]]], \classlock, \monitored_by and \monitored. Once again, please post your comments to jml-interest-list@cs.iastate.edu on this. Comments this week (August 19...) would be extremely helpful, but whenever you have time would also be good. Thanks. Gary  1, filed, answered,, Mail-from: From Bart.Jacobs@cs.kun.nl Thu Aug 19 08:08:14 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 IAA25048 for ; Thu, 19 Aug 1999 08:08:12 -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 PAA26766 (8.8.8/1.1); Thu, 19 Aug 1999 15:08:04 +0200 (MET DST) Message-Id: <199908191308.PAA26766@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: assignments to model variables In-reply-to: Your message of "Wed, 18 Aug 1999 22:35:55 CDT." <199908190335.WAA17093@ren.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Thu, 19 Aug 1999 15:08:09 +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: assignments to model variables In-reply-to: Your message of "Wed, 18 Aug 1999 22:35:55 CDT." <199908190335.WAA17093@ren.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Thu, 19 Aug 1999 15:08:09 +0200 From: Bart Jacobs Hi Gary, Here we had some discussion about whether or not one can/should have assignments to model variables in JML. The general feeling was NOT, but we were not completely sure. Can you tell me more. This issue is quite fundamental in semantics. Having assignments to model variables would be a big problem. Bye, Bart.  1, answered,, Mail-from: From owner-jml-interest-list Thu Aug 19 08:05:59 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id IAA25025 for jml-interest-list-outgoing; Thu, 19 Aug 1999 08:05:57 -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 IAA25021 for ; Thu, 19 Aug 1999 08:05:54 -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 PAA26399 (8.8.8/1.1); Thu, 19 Aug 1999 15:05:42 +0200 (MET DST) Message-Id: <199908191305.PAA26399@pandora.cs.kun.nl> X-Mailer: exmh version 2.0.3 3/22/1999 To: jml-interest-list@cs.iastate.edu cc: Bart.Jacobs@cs.kun.nl Subject: Re: JML-Interest: Possible changes to the JML grammar, comments and reaction sought In-reply-to: Your message of "Wed, 18 Aug 1999 22:35:55 CDT." <199908190335.WAA17093@ren.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Thu, 19 Aug 1999 15:05:47 +0200 From: Bart Jacobs Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Return-Path: X-Mailer: exmh version 2.0.3 3/22/1999 To: jml-interest-list@cs.iastate.edu cc: Bart.Jacobs@cs.kun.nl Subject: Re: JML-Interest: Possible changes to the JML grammar, comments and reaction sought In-reply-to: Your message of "Wed, 18 Aug 1999 22:35:55 CDT." <199908190335.WAA17093@ren.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Thu, 19 Aug 1999 15:05:47 +0200 From: Bart Jacobs Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, Here at Nijmegen we are very happy about the plans to team-up with the ESC group at Compaq. It is really good to have a common language. Also, it will give potential users a wider range of options: e.g. do static checking first, and use formal verification (with theorem provers) for the parts that come out as problematic. The proposed syntax changes are OK. It is for us (especially for Joachim) undoable to follow all the syntax changes from day to day, and since we are concentrating on the semantics anyway, we should find some mode where we can proceed with what we do, and adapt to the latest syntax when the dust comes down. Since the specification languages will be merged, we are now more keen than before to see details of the ESC language. Is there a document available? Best wishes to all, Bart.  1,, Mail-from: From leavens@cs.iastate.edu Thu Aug 19 11:13:14 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 LAA28089; Thu, 19 Aug 1999 11:13:13 -0500 (CDT) Received: (from leavens@localhost) by ren.cs.iastate.edu (8.9.0/8.9.0) id LAA03851; Thu, 19 Aug 1999 11:13:09 -0500 (CDT) Date: Thu, 19 Aug 1999 11:13:09 -0500 (CDT) Message-Id: <199908191613.LAA03851@ren.cs.iastate.edu> From: "Gary T. Leavens" To: Bart.Jacobs@cs.kun.nl CC: Bart.Jacobs@cs.kun.nl, leavens@cs.iastate.edu In-reply-to: <199908191308.PAA26766@pandora.cs.kun.nl> (message from Bart Jacobs on Thu, 19 Aug 1999 15:08:09 +0200) Subject: Re: assignments to model variables *** EOOH *** Return-Path: Date: Thu, 19 Aug 1999 11:13:09 -0500 (CDT) From: "Gary T. Leavens" To: Bart.Jacobs@cs.kun.nl CC: Bart.Jacobs@cs.kun.nl, leavens@cs.iastate.edu In-reply-to: <199908191308.PAA26766@pandora.cs.kun.nl> (message from Bart Jacobs on Thu, 19 Aug 1999 15:08:09 +0200) Subject: Re: assignments to model variables Bart, Thanks for the comments about the syntax changes. I am excited about the synergy possibilities too. > Here we had some discussion about whether or not one can/should > have assignments to model variables in JML. The general > feeling was NOT, but we were not completely sure. Can you > tell me more. > > This issue is quite fundamental in semantics. Having > assignments to model variables would be a big problem. I agree that if you have model variables that have dependents, then it's not very clear what it would mean to assign to them. Perhaps it would be like assigning some value (nondeterministically chosen) to their dependents that made this one be the same abstractly as what was assigned. This is the motivation for distinguishing model variables with dependents from those without dependents. The latter cause no problems if you assign to them. Gary  1, filed,, Mail-from: From leavens@cs.iastate.edu Thu Aug 19 11:23:29 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 LAA28215; Thu, 19 Aug 1999 11:23:29 -0500 (CDT) Received: (from leavens@localhost) by ren.cs.iastate.edu (8.9.0/8.9.0) id LAA04261; Thu, 19 Aug 1999 11:23:25 -0500 (CDT) Date: Thu, 19 Aug 1999 11:23:25 -0500 (CDT) Message-Id: <199908191623.LAA04261@ren.cs.iastate.edu> From: "Gary T. Leavens" To: Bart.Jacobs@cs.kun.nl CC: jml-interest-list@cs.iastate.edu, Bart.Jacobs@cs.kun.nl, leavens@cs.iastate.edu In-reply-to: <199908191305.PAA26399@pandora.cs.kun.nl> (message from Bart Jacobs on Thu, 19 Aug 1999 15:05:47 +0200) Subject: Re: JML-Interest: Possible changes to the JML grammar, comments and reaction sought *** EOOH *** Return-Path: Date: Thu, 19 Aug 1999 11:23:25 -0500 (CDT) From: "Gary T. Leavens" To: Bart.Jacobs@cs.kun.nl CC: jml-interest-list@cs.iastate.edu, Bart.Jacobs@cs.kun.nl, leavens@cs.iastate.edu In-reply-to: <199908191305.PAA26399@pandora.cs.kun.nl> (message from Bart Jacobs on Thu, 19 Aug 1999 15:05:47 +0200) Subject: Re: JML-Interest: Possible changes to the JML grammar, comments and reaction sought Bart, Thanks for the comments on the syntax changes. I'm excited about the possibility of synergy too. At some point we do have to stabilize this syntax. I"m hoping that will be soon (before Joachim comes to visit). If everyone agrees, I expect that this would be the last round of major changes. A good strategy will be to identify a stable subset of JML that you want to support for verification purposes. We can help with that after the changes from the current work settle. I'm not sure that the reference manual for ESC/Java is available. But check out http://www.research.digital.com/SRC/esc/Esc.html for more information. Gary  1,, Summary-line: 8-Sep -interest-list@cs.iastate [53] #Abstraction functions instead of abstraction relations Mail-from: From leavens@cs.iastate.edu Wed Sep 8 16:57: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 QAA19615; Wed, 8 Sep 1999 16:57:51 -0500 (CDT) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id QAA00541; Wed, 8 Sep 1999 16:57:44 -0500 (CDT) Date: Wed, 8 Sep 1999 16:57:44 -0500 (CDT) Message-Id: <199909082157.QAA00541@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: Abstraction functions instead of abstraction relations *** EOOH *** Return-Path: Date: Wed, 8 Sep 1999 16:57:44 -0500 (CDT) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: Abstraction functions instead of abstraction relations Hi, Currently, in JML we use abstraction relations to define how model variables relate to concrete variables, for example. However, this makes it difficult to do dynamic checking of such things as preconditions and invariants. The problem is that abstraction relation does not always give any obvious algorithm for computing the value of the model variables from the value of the dependent variables. For example, in the PlusAccount example in the preliminary design document, the "credit" field is determined by the relation given in the following represents clause: represents credit -> credit.equals(savings.plus(checking)); While this particular example is (mathematically) constructive, in general such a relation need not be constructive. And it would be difficult for a tool to extract the definition from equivalent forms of this example, such as. represents credit -> savings.equals(credit.minus(checking)) Therefore, Abhay (who's working on dynamic checking in JML) and I propose that we change the syntax of the represents clause in JML. The idea would be the we force the user to give an abstraction function, which would define the value of the model variable based on the concrete variables it depends on. Possible syntax would be as follows. represents credit = savings.plus(checking); or perhaps represents credit <- savings.plus(checking); Better syntax suggestions are welcome... Gary  1, filed, answered,, Summary-line: 9-Sep Bart.Jacobs@cs.kun.nl [91] #Re: your technical report Mail-from: From Bart.Jacobs@cs.kun.nl Thu Sep 9 09:08:30 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 JAA04204 for ; Thu, 9 Sep 1999 09:08:28 -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 QAA11990 (8.8.8/1.1); Thu, 9 Sep 1999 16:08:19 +0200 (MET DST) Message-Id: <199909091408.QAA11990@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: your technical report In-reply-to: Your message of "Tue, 07 Sep 1999 17:29:27 CDT." <199909072229.RAA19384@larch.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Thu, 09 Sep 1999 16:08:24 +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: your technical report In-reply-to: Your message of "Tue, 07 Sep 1999 17:29:27 CDT." <199909072229.RAA19384@larch.cs.iastate.edu> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Thu, 09 Sep 1999 16:08:24 +0200 From: Bart Jacobs Hi Gary, How are you? > I got your technical report in the mail titled "Java program > verification via a Hoare logic with abrupt termination". Thanks for > sending that, it looks very interesting. OK, let me hear if you have comments. > The semester is just getting underway here, and classes have been > keeping me pretty busy so far. I'm waiting for replies from Raymie > Stata and Rustan Leino on a few outstanding issues. The situation > hasn't changed much from what I sent while I was in California. > However, I can send you an updated list of what the changes being > contemplated are, if you'd like to see them at this point. No, there is no urgency. I will wait until Joachim returns from Iowa. Hopefully we have some stability then. Here I have started elaborating the semantics (in PVS) of some JML files by hand. This will then serve as a blueprint for the automatic translation. I started working on BoundedThing and on BoundedStack. Progress is slow, but steady. A recent application area that we are working on is Java Card. This seems like a good target for formal verification. The programs are small, and the industry seems interested. The API is (currently) about 45 classes. Their translation into PVS is 2.5MB of PVS code! We are planning to do cardlet verification, but also to give a JML specification of the API. This looks like something that can actually be done, and might even have some impact (both for clients and providers). We are planning to put it on the web, once it is finished. About your question: > However, this makes it difficult to do dynamic checking of such things > as preconditions and invariants. The problem is that abstraction > relation does not always give any obvious algorithm for computing the > value of the model variables from the value of the dependent > variables. For example, in the PlusAccount example in the preliminary > design document, the "credit" field is determined by the relation > given in the following represents clause: > represents credit -> credit.equals(savings.plus(checking)); > While this particular example is (mathematically) constructive, in > general such a relation need not be constructive. And it would be > difficult for a tool to extract the definition from equivalent forms > of this example, such as. > represents credit -> savings.equals(credit.minus(checking)) > Therefore, Abhay (who's working on dynamic checking in JML) and I > propose that we change the syntax of the represents clause in JML. > The idea would be the we force the user to give an abstraction > function, which would define the value of the model variable based on > the concrete variables it depends on. Possible syntax would be as > follows. > represents credit = savings.plus(checking); > or perhaps > represents credit <- savings.plus(checking); I haven't looked into reprensents clauses yet, but certainly functions look easier to handle semantically than relations, so I am in favour of this. The one-but-last syntax with = looks OK to me. Bye, Bart. PS. What is the situation with a special issue for FTfJP??  1,, Mail-from: From leavens@cs.iastate.edu Fri Nov 19 16:29: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 QAA10576; Fri, 19 Nov 1999 16:29:04 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id QAA13527; Fri, 19 Nov 1999 16:28:56 -0600 (CST) Date: Fri, 19 Nov 1999 16:28:56 -0600 (CST) Message-Id: <199911192228.QAA13527@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: grammar changes coming to JML *** EOOH *** Return-Path: Date: Fri, 19 Nov 1999 16:28:56 -0600 (CST) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: grammar changes coming to JML Hi, We have been continuing the process of revising the grammar based on our discussions with Raymie Stata, Rustan Leino, and their group at Compaq SRC. I believe that we have now reached some kind of stability here at ISU on these changes. I am trying to produce a revised "preliminary design" document to reflect the grammar changes, but the following is a brief overview. Gary DIFFERENCES BETWEEN ESC/JAVA AND JML $Date: 1999/11/19 19:57:44 $ This reflects discussions from Gary Leavens's visit with Raymie Stata and Rustan Leino at Compaq SRC ending August 20, 1999, some discussion back at Iowa State on Aug 30, 1999, discussions between Gary and Rustan during FM'99 (Sept. 19-25, 1999), and revisions by the JML team (especially thanks to Clyde Ruby) in October and November. A formal grammar is now available, and should be consulted for the details of the syntax. DIFFERENCES FOR WHICH BOTH JML AND ESC/JAVA WILL CHANGE - ESC/Java uses /*@ ... */ while JML uses /*@ ... @*/ for C-style annotations. Esc/Java and JML will both make the last @ optional. (Note: there's no way to nest C-style comments within such an annotation, because the Java parser does not allow nested comments.) - Currently, JML allows method specifications to appear after the end of a method signature, including the semicolon in an interface. public int foo(); normal_behavior ensures ...; In ESC/Java, such specications may come before the method signature, or before the semicolon or open brace that follows. ESC/Java will change to conform to JML by allowing specifications to appear after the ";" in a method signature. (It already allows specifications before the opening brace that starts a method body.) It may do this by adding a notion of "post-modifier", which attaches to the preceeding declaration. JML will change to allow specifications to appear within javadoc comments in the form /** ...

     ...
    
*/ which, of course, will appear before the method signature. ESC/Java already has such comments, but will change from using and to and . [[[At ISU, we are also investigating the use of the usual Java doclet style using keywords like @requires, etc.]]] - JML and ESC/Java will use \not_modified( SRL ) in predicates (see below for SRL grammar) instead of "\unmodified", because Java treats \u as an escape sequence for a unicode character. - ESC/Java has "elemsnonnull" for arrays. ESC/Java and JML will both use "\nonnullelements" for this. - ESC/Java has expressions made with TYPE, type, typeof, elemtype, and <: JML will add \TYPE, \type(Type), \typeof(Expr), \elemtype(Expr), and <: (Also, note that the notion of type is necessary because not all expressions in Java have reference types; for example the value types int and char.) - JML uses the notation \forall (T1 x1, x2; T3 x3) [ pred(x1, x2, x3) ] for universal quantification. ESC/Java uses (forall T1 x1, x2; (forall T3 x3; pred(x1, x2, x3) )) for this. Similarly for existential quantification. Because of parsing problems with what we orignally agreed to, we will both change to a syntax like ESC/Java's, but with parentheses around the declarations. (The last semicolon in the declarations is optional.) (\forall (T1 x1, x2; T3 x3;) pred(x1, x2, x3) ) - JML uses the declaration attribute "model", which can be used to declare abstract, specification-only variables that can depend on concrete variables. ESC/Java has "ghost" which are concrete, specification-only variables. These seem to be scoped differently, as in JML the scope of a model declaration is exactly the same as for a normal Java declaration, but this is not the case for ESC/Java ghost variables. ESC/Java uses the "set" pragma to assign to ghost variables, but in JML there are no special constructs for assigning to model variables. ESC/Java will change to have "model" declarations, and to make the scope of ghost variable declarations the same scoping as normal Java declarations. JML will change to have "ghost" variable declarations, and add a "set" statement. (At one point we considered changing with a "dependent" and "instance" keyword, but that was dropped.) - In JML, loop invariants and termination functions are specified with the syntax (adapted from RESOLVE): //@ maintaining ...loop_inv... //@ decreasing ...termination_fun... while (...cond...) do { ...statements... } while in ESC/Java this would be written as follows. while (...cond...) do { //@ loop_invariant ...loop_inv...; ...statements... } and there is no termination function. We agreed that both languages would use the following syntax: //@ loop_invariant ...loop_inv... //@ decreases ...termination_fun... while (...cond...) do { ...statements... } but for JML we will also retain the old syntax as an option. - JML and ESC/Java will adopt a new, combined specification syntax. The following gives the flavor of what we agreed on, although the actual grammar is more complex, and the yacc file should be consulted for the details. The idea is that a specification would use either S or ES depending on whether the method is an override; if there are, then ES must be used, otherwise S must be used. Several nonterminals below are written so that there are no empty productions. S ::= [ SC [also SC]* ] RS "specifications" ES ::= also S "extending specs" | and [let MVD+] RS | and [let MVD+] RS ::= ::= M* E* X* [D] SE+ | M* E* X* D | M* E* X+ | M* E+ | M+ SC ::= "spec case" | | SE ::= | "spec extra" ::= [let MVD+] [] | [let MVD+] [] `{[' SC [also SC]* `]}' | [let MVD+] ::= R* * MB+ | R* * | R+ ::= behavior | normal_behavior NSC | exceptional_behavior XSC XSC ::= [let MVD+] [] M* X+ [D] SE* "exceptional spec case" | [let MVD+] [] `{[' XSC [also XSC]* `]}' NSC ::= [let MVD+] [] M* E+ [D] SE* "normal spec case" | [let MVD+] [] M+ [D] SE* | [let MVD+] [] `{[' NSC [also NSC]* `]}' RS ::= [] "redundant specs" | ::= implies_that ISC [also ISC]* ISC ::= [implication] | normal_implication NSC | exceptional_implication XSC ::= for_example [also ]* example ::= [example] [] | normal_example [] M* E+ [D] | normal_example [] M+ [D] | exceptional_example [] M* X [D] MVD ::= model [] ; ::= [,]* ::= [] [ = ] ::= initially : | readable_if : | monitored_by : MB ::= measured_by [redundantly] : ; M ::= modifiable [redundantly] : SRL ; SRL ::= SR [, SR]* SR ::= | [ ] | \nothing | \everything | \reach( ) ::= | `*' | .. E ::= ensures [redundantly] : ; X ::= exsures [redundantly] : ( [] ) [] ; | signals [redundantly] : ( [] ) [] ; D ::= diverges [redundantly] : ; Note that the addition of "signals" as an alternative to "exsures", and the use of {[ and ]} as brackets for spec case sequences are recent changes proposed by the JML team, which also proposes making a colon mandatory before a predicate, expression or SRL. [[[The alternative is to use keywords like "ensures_redundantly" and to take out the colons completely. Note that there aren't colons following keywords like "normal_behavior", or "also" anymore.]]] The defaults are requires: true; modifiable: \nothing; ensures: true; exsures: true; diverges: false; (Also, for JML, callable: \everything; and accessible: \everything;) DIFFERENCES FOR WHICH JML WILL CHANGE - 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 @*/. - 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 delete many of these colons, and to make them tokens instead of parts of the keywords. JML will also be changed to only recognize keywords within annotations and outside of spec-expressions (and in .jml files). - ESC/Java has .spec files with the annotation syntax. - ESC/Java has LS, LS[], classlock, monitored_by, and monitored for dealing with threads. JML will add \lockset, \classlock(Expr), and syntax for "monitored_by" and "monitored" on declarations of fields. - ESC/Java has LBLNEG and LBLPOS for labeling assertions. JML will add the syntax (\label name Expr) and (\lblpos name Expr). - ESC/Java has "spec_public" as a modifier, JML will add this, as well as "spec_protected". - ESC/Java has an "axiom" pragma. JML will add "axiom" declarations in places where declarations are permitted. - ESC/Java has "readable_if" (formerly "defined_if") and "uninitialized" pragmas for declarations. JML will add readable_if in the same place where initially could go. JML will also add "unitialized". (The readable_if pragma specifies that the variable only has a meaningful value when then given condition is true. The uninitialized pragma specifies that the value given in the initialization is irrelevant.) - JML will no longer permit specification statements other than assert, assume, and (the new) set inside Java implementations. (These would still be allowed in model programs.) DIFFERENCES WHICH WILL REMAIN (JML AS A SUPERSET OF ESC/JAVA) - JML uses .jml, .jml-refined, and .java-refined files as well as .java files. - JML has .jml and .jml-refined files whose syntax does not require annotation markers. - JML has dependent (abstract) model variables. - JML has model classes, interfaces, or methods. - JML has depends and represents declarations. - JML has history constraints (constraint). - JML has callable and accessible clauses - JML has other refinement calculus and annotation primitives besides the assert and assume that are in ESC/Java choose, because, a nondeterministic if statement (choose_if), and behavior statements (these allow a specification to act as a statement) that can appear only in model programs. - JML has pure class and method annotations for saying when methods have no side effects. - JML allows pure method invocations in assertions. - JML allows new expressions in assertions. - JML has measured_by clauses to give termination functions for recursive methods and specifications. - JML has a notion of refinement of specifications with a "refine" keyword. - JML has model import declarations. - JML has when clauses in specifications for concurrency. DIFFERENCES THAT NEED MORE DISCUSSION Rustan and Gary discussed Eric Hehner's idea of using a time variable, \time, instead of the usual notion of total correctness and variant functions for loops. This actually seems doable, however we're not sure it is a good idea. It does seem to reduce the number of keywords and concepts of language. However, this idea is not widely accepted. There was some question as to what the default specificaton should be when none is given. Once choice is the unit of "also" (see the appendix below). But perhaps it makes more sense now to use the completely default specification (see comments above under the grammar). APPENDIX A technical note: When Gary was at SRC, we noted that the unit of "also"-combination for method specifications is the specification: requires false; (and for this specification the set of variables that can be modified and the postcondition don't matter). Note however that this is not the unit of the "and" combination of specifications.  1,, Mail-from: From owner-jml-interest-list Fri Nov 19 16:29:14 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id QAA10581 for jml-interest-list-outgoing; Fri, 19 Nov 1999 16:29:07 -0600 (CST) 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 QAA10576; Fri, 19 Nov 1999 16:29:04 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id QAA13527; Fri, 19 Nov 1999 16:28:56 -0600 (CST) Date: Fri, 19 Nov 1999 16:28:56 -0600 (CST) Message-Id: <199911192228.QAA13527@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: grammar changes coming to JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Return-Path: Date: Fri, 19 Nov 1999 16:28:56 -0600 (CST) From: "Gary T. Leavens" To: jml-interest-list@cs.iastate.edu CC: leavens@cs.iastate.edu Subject: JML-Interest: grammar changes coming to JML Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, We have been continuing the process of revising the grammar based on our discussions with Raymie Stata, Rustan Leino, and their group at Compaq SRC. I believe that we have now reached some kind of stability here at ISU on these changes. I am trying to produce a revised "preliminary design" document to reflect the grammar changes, but the following is a brief overview. Gary DIFFERENCES BETWEEN ESC/JAVA AND JML $Date: 1999/11/19 19:57:44 $ This reflects discussions from Gary Leavens's visit with Raymie Stata and Rustan Leino at Compaq SRC ending August 20, 1999, some discussion back at Iowa State on Aug 30, 1999, discussions between Gary and Rustan during FM'99 (Sept. 19-25, 1999), and revisions by the JML team (especially thanks to Clyde Ruby) in October and November. A formal grammar is now available, and should be consulted for the details of the syntax. DIFFERENCES FOR WHICH BOTH JML AND ESC/JAVA WILL CHANGE - ESC/Java uses /*@ ... */ while JML uses /*@ ... @*/ for C-style annotations. Esc/Java and JML will both make the last @ optional. (Note: there's no way to nest C-style comments within such an annotation, because the Java parser does not allow nested comments.) - Currently, JML allows method specifications to appear after the end of a method signature, including the semicolon in an interface. public int foo(); normal_behavior ensures ...; In ESC/Java, such specications may come before the method signature, or before the semicolon or open brace that follows. ESC/Java will change to conform to JML by allowing specifications to appear after the ";" in a method signature. (It already allows specifications before the opening brace that starts a method body.) It may do this by adding a notion of "post-modifier", which attaches to the preceeding declaration. JML will change to allow specifications to appear within javadoc comments in the form /** ...

     ...
    
*/ which, of course, will appear before the method signature. ESC/Java already has such comments, but will change from using and to and . [[[At ISU, we are also investigating the use of the usual Java doclet style using keywords like @requires, etc.]]] - JML and ESC/Java will use \not_modified( SRL ) in predicates (see below for SRL grammar) instead of "\unmodified", because Java treats \u as an escape sequence for a unicode character. - ESC/Java has "elemsnonnull" for arrays. ESC/Java and JML will both use "\nonnullelements" for this. - ESC/Java has expressions made with TYPE, type, typeof, elemtype, and <: JML will add \TYPE, \type(Type), \typeof(Expr), \elemtype(Expr), and <: (Also, note that the notion of type is necessary because not all expressions in Java have reference types; for example the value types int and char.) - JML uses the notation \forall (T1 x1, x2; T3 x3) [ pred(x1, x2, x3) ] for universal quantification. ESC/Java uses (forall T1 x1, x2; (forall T3 x3; pred(x1, x2, x3) )) for this. Similarly for existential quantification. Because of parsing problems with what we orignally agreed to, we will both change to a syntax like ESC/Java's, but with parentheses around the declarations. (The last semicolon in the declarations is optional.) (\forall (T1 x1, x2; T3 x3;) pred(x1, x2, x3) ) - JML uses the declaration attribute "model", which can be used to declare abstract, specification-only variables that can depend on concrete variables. ESC/Java has "ghost" which are concrete, specification-only variables. These seem to be scoped differently, as in JML the scope of a model declaration is exactly the same as for a normal Java declaration, but this is not the case for ESC/Java ghost variables. ESC/Java uses the "set" pragma to assign to ghost variables, but in JML there are no special constructs for assigning to model variables. ESC/Java will change to have "model" declarations, and to make the scope of ghost variable declarations the same scoping as normal Java declarations. JML will change to have "ghost" variable declarations, and add a "set" statement. (At one point we considered changing with a "dependent" and "instance" keyword, but that was dropped.) - In JML, loop invariants and termination functions are specified with the syntax (adapted from RESOLVE): //@ maintaining ...loop_inv... //@ decreasing ...termination_fun... while (...cond...) do { ...statements... } while in ESC/Java this would be written as follows. while (...cond...) do { //@ loop_invariant ...loop_inv...; ...statements... } and there is no termination function. We agreed that both languages would use the following syntax: //@ loop_invariant ...loop_inv... //@ decreases ...termination_fun... while (...cond...) do { ...statements... } but for JML we will also retain the old syntax as an option. - JML and ESC/Java will adopt a new, combined specification syntax. The following gives the flavor of what we agreed on, although the actual grammar is more complex, and the yacc file should be consulted for the details. The idea is that a specification would use either S or ES depending on whether the method is an override; if there are, then ES must be used, otherwise S must be used. Several nonterminals below are written so that there are no empty productions. S ::= [ SC [also SC]* ] RS "specifications" ES ::= also S "extending specs" | and [let MVD+] RS | and [let MVD+] RS ::= ::= M* E* X* [D] SE+ | M* E* X* D | M* E* X+ | M* E+ | M+ SC ::= "spec case" | | SE ::= | "spec extra" ::= [let MVD+] [] | [let MVD+] [] `{[' SC [also SC]* `]}' | [let MVD+] ::= R* * MB+ | R* * | R+ ::= behavior | normal_behavior NSC | exceptional_behavior XSC XSC ::= [let MVD+] [] M* X+ [D] SE* "exceptional spec case" | [let MVD+] [] `{[' XSC [also XSC]* `]}' NSC ::= [let MVD+] [] M* E+ [D] SE* "normal spec case" | [let MVD+] [] M+ [D] SE* | [let MVD+] [] `{[' NSC [also NSC]* `]}' RS ::= [] "redundant specs" | ::= implies_that ISC [also ISC]* ISC ::= [implication] | normal_implication NSC | exceptional_implication XSC ::= for_example [also ]* example ::= [example] [] | normal_example [] M* E+ [D] | normal_example [] M+ [D] | exceptional_example [] M* X [D] MVD ::= model [] ; ::= [,]* ::= [] [ = ] ::= initially : | readable_if : | monitored_by : MB ::= measured_by [redundantly] : ; M ::= modifiable [redundantly] : SRL ; SRL ::= SR [, SR]* SR ::= | [ ] | \nothing | \everything | \reach( ) ::= | `*' | .. E ::= ensures [redundantly] : ; X ::= exsures [redundantly] : ( [] ) [] ; | signals [redundantly] : ( [] ) [] ; D ::= diverges [redundantly] : ; Note that the addition of "signals" as an alternative to "exsures", and the use of {[ and ]} as brackets for spec case sequences are recent changes proposed by the JML team, which also proposes making a colon mandatory before a predicate, expression or SRL. [[[The alternative is to use keywords like "ensures_redundantly" and to take out the colons completely. Note that there aren't colons following keywords like "normal_behavior", or "also" anymore.]]] The defaults are requires: true; modifiable: \nothing; ensures: true; exsures: true; diverges: false; (Also, for JML, callable: \everything; and accessible: \everything;) DIFFERENCES FOR WHICH JML WILL CHANGE - 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 @*/. - 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 delete many of these colons, and to make them tokens instead of parts of the keywords. JML will also be changed to only recognize keywords within annotations and outside of spec-expressions (and in .jml files). - ESC/Java has .spec files with the annotation syntax. - ESC/Java has LS, LS[], classlock, monitored_by, and monitored for dealing with threads. JML will add \lockset, \classlock(Expr), and syntax for "monitored_by" and "monitored" on declarations of fields. - ESC/Java has LBLNEG and LBLPOS for labeling assertions. JML will add the syntax (\label name Expr) and (\lblpos name Expr). - ESC/Java has "spec_public" as a modifier, JML will add this, as well as "spec_protected". - ESC/Java has an "axiom" pragma. JML will add "axiom" declarations in places where declarations are permitted. - ESC/Java has "readable_if" (formerly "defined_if") and "uninitialized" pragmas for declarations. JML will add readable_if in the same place where initially could go. JML will also add "unitialized". (The readable_if pragma specifies that the variable only has a meaningful value when then given condition is true. The uninitialized pragma specifies that the value given in the initialization is irrelevant.) - JML will no longer permit specification statements other than assert, assume, and (the new) set inside Java implementations. (These would still be allowed in model programs.) DIFFERENCES WHICH WILL REMAIN (JML AS A SUPERSET OF ESC/JAVA) - JML uses .jml, .jml-refined, and .java-refined files as well as .java files. - JML has .jml and .jml-refined files whose syntax does not require annotation markers. - JML has dependent (abstract) model variables. - JML has model classes, interfaces, or methods. - JML has depends and represents declarations. - JML has history constraints (constraint). - JML has callable and accessible clauses - JML has other refinement calculus and annotation primitives besides the assert and assume that are in ESC/Java choose, because, a nondeterministic if statement (choose_if), and behavior statements (these allow a specification to act as a statement) that can appear only in model programs. - JML has pure class and method annotations for saying when methods have no side effects. - JML allows pure method invocations in assertions. - JML allows new expressions in assertions. - JML has measured_by clauses to give termination functions for recursive methods and specifications. - JML has a notion of refinement of specifications with a "refine" keyword. - JML has model import declarations. - JML has when clauses in specifications for concurrency. DIFFERENCES THAT NEED MORE DISCUSSION Rustan and Gary discussed Eric Hehner's idea of using a time variable, \time, instead of the usual notion of total correctness and variant functions for loops. This actually seems doable, however we're not sure it is a good idea. It does seem to reduce the number of keywords and concepts of language. However, this idea is not widely accepted. There was some question as to what the default specificaton should be when none is given. Once choice is the unit of "also" (see the appendix below). But perhaps it makes more sense now to use the completely default specification (see comments above under the grammar). APPENDIX A technical note: When Gary was at SRC, we noted that the unit of "also"-combination for method specifications is the specification: requires false; (and for this specification the set of variables that can be modified and the postcondition don't matter). Note however that this is not the unit of the "and" combination of specifications.  1,, Mail-from: From owner-jml-interest-list Wed Dec 1 12:33:51 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id MAA26982 for jml-interest-list-outgoing; Wed, 1 Dec 1999 12:33:38 -0600 (CST) 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 MAA26976; Wed, 1 Dec 1999 12:33:31 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id MAA10028; Wed, 1 Dec 1999 12:33:24 -0600 (CST) Date: Wed, 1 Dec 1999 12:33:24 -0600 (CST) Message-Id: <199912011833.MAA10028@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 Wed, 1 Dec 1999 16:37:29 +0100 (CET)) Subject: JML-Interest: JML questions Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Return-Path: Date: Wed, 1 Dec 1999 12:33:24 -0600 (CST) 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 Wed, 1 Dec 1999 16:37:29 +0100 (CET)) Subject: JML-Interest: JML questions Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Joachim, > Here in Nijmegen, we are making progress with the implementation of > JML into our tool. There is some theory generation now, but it is not stable > yet. I will keep you informed about that... Good, thanks. > I have a few questions for you. I hope you can answer them: > > 1. What's the boolean value of predicate > (\forall (int i) 2/i == 0) ? > > For me it's not clear if this predicate terminate normally, or that it > terminates abnormally because of an ArithmeticException (which is not > allowed for predicates). If a predicate would signal an exception, then its value is "unspecified" by JML. An implementation can choose whatever value it likes (perhaps false in this case would be appropriate). For theorem proving, you should not be able to prove it's value is either true or false. I'm not sure how to arrange that. Predicates don't terminate abnormally. > 2. One can write a depends clause like > depends reach (i) -> j > > but what does it mean if i doesn't have reachable objects? > Is i included in the reach construct? We'll need to think more about this... > 3. Here in Nijmegen we have a discussion about the following: > > ensures : a != null && a.length > 0; > > A modeler, we think, will often forget the a != null clause and write > instead: > a.length > 0; > > This a != null clause can be omitted, but then an extra proof obligation > should be generated, to show that a != null in the post-state. What would > you prefer? Good question. I agree that it's easy to forget these checks. I do believe that it's preferable to have the author write this kind of check into the specification, however, since it provides valuable documentation. This is especially true of the requires clause. Is it possible for the checker to give a ``type error'' for such a specification, and say that ``a is not known to be nonnull in the postcondition...'' or something like that, to force the user to write it? This seems no more difficult then generating the extra proof obligation, and has the benefit of making the documentation better. (A tool could perhaps generate the "corrected" specification for the user...) > 4. According to the grammar rule store_ref one can write a modifiable clause > modifiable: i + 1; > > This is not allowed, you probably prevend this semantically. Wouldn't it > be better to rewrite the store_ref rule to something similar like: > > store_ref :== > name > | REACH T_LPAREN name T_RPAREN > | array_range_ref > > (expressions like 'i+1' are not allowed anymore, this would be an > improvement. But now also expressions like 'super.i' are not allowed > anymore, which should be fixed...) That's a good suggestion, we should consider it. It has to do with how we interpret reach, and whether we want to allow user-defined model methods to do things like "reach" does, in returning sets of l-values. Gary  1,, Mail-from: From owner-jml-interest-list Wed Dec 15 10:08:27 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id KAA26425 for jml-interest-list-outgoing; Wed, 15 Dec 1999 10:08:20 -0600 (CST) 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 KAA26421 for ; Wed, 15 Dec 1999 10:08:17 -0600 (CST) Received: from hera.cs.kun.nl by pandora.cs.kun.nl via hera.cs.kun.nl [131.174.33.2] with SMTP for id RAA00596 (8.8.8/3.12); Wed, 15 Dec 1999 17:08:12 +0100 (MET) Date: Wed, 15 Dec 1999 17:08:15 +0100 (MET) From: Erik Poll To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: modifiable clauses for constructors ? 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: Wed, 15 Dec 1999 17:08:15 +0100 (MET) From: Erik Poll To: jml-interest-list@cs.iastate.edu Subject: JML-Interest: modifiable clauses for constructors ? MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Dear jml-ers, In the "Preliminary Design of JML" paper, in the USMoney example (I have the November 1999 version, there it's on page 25), the specifications of the two constructors include modifiable: pennies; i.e. the constructors may modify the instance field pennies. But does it make sense to have a modifiable clause for an instance field in the spec of a constructor ? The question of whether or not the value of pennies in the post-state is equal to its \old value in the pre-state seems meaningless, as there is no old value of pennies in a pre-state to speak of. If one considers the value of pennies to be "modified" by the constructors of USMoney, then by definition a constructor always "modifies" all instance fields. I'd say that only for _static_ fields it make sense to say that a constructor may modify it. Am I missing something ? I noticed for instance that the definition of "pure constructor" also explicitly refers to constructors modifying non-static fields. Cheers, Erik  1,, Mail-from: From owner-jml-interest-list Wed Dec 15 10:19:12 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id KAA26608 for jml-interest-list-outgoing; Wed, 15 Dec 1999 10:19:07 -0600 (CST) Received: from oak.fernuni-hagen.de (oak.fernuni-hagen.de [132.176.114.41]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id KAA26602 for ; Wed, 15 Dec 1999 10:19:03 -0600 (CST) Received: from sunpoet2.fernuni-hagen.de by oak.fernuni-hagen.de via local-channel with ESMTP; Wed, 15 Dec 1999 17:18:37 +0100 Received: (from mueller@localhost) by sunpoet2.fernuni-hagen.de (8.9.1b+Sun/8.9.1) id RAA15243; Wed, 15 Dec 1999 17:18:34 +0100 (MET) Date: Wed, 15 Dec 1999 17:18:34 +0100 (MET) Message-Id: <199912151618.RAA15243@sunpoet2.fernuni-hagen.de> X-Authentication-Warning: sunpoet2.fernuni-hagen.de: mueller set sender to Peter.Mueller@fernuni-hagen.de using -f From: Peter Mueller MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit To: Erik Poll Cc: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: modifiable clauses for constructors ? In-Reply-To: References: X-Mailer: VM 6.32 under Emacs 20.3.1 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Return-Path: Date: Wed, 15 Dec 1999 17:18:34 +0100 (MET) X-Authentication-Warning: sunpoet2.fernuni-hagen.de: mueller set sender to Peter.Mueller@fernuni-hagen.de using -f From: Peter Mueller MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit To: Erik Poll Cc: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: modifiable clauses for constructors ? In-Reply-To: References: X-Mailer: VM 6.32 under Emacs 20.3.1 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi! > I'd say that only for _static_ fields it make sense to say that a > constructor may modify it. Am I missing something ? I noticed for > instance that the definition of "pure constructor" also explicitly > refers to constructors modifying non-static fields. Modifiable-clauses should mention all fields of objects that are allocated in the prestate of a method/constructor and that might be changed during method/constructor execution. That is, there are instance fields that could occur in the modifiable-clause of a constructor if the object to which the field belongs is reachable from (1) a parameter of the constructor or (2) a static field. So it is not sufficient to limit the modifiable-clauses of constructors to static fields. However, I agree that in the example, pennies should not appear in the modifiable-clause. Peter _/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/ _/ Peter Mueller _/ _/ Fernuniversitaet Hagen, Lehrgebiet Praktische Informatik V _/ _/ 58084 Hagen, Feithstr. 142, Raum 1.F13 _/ _/ _/ _/ Tel: 02331-987 4870 _/ _/ Fax: 02331-987 4487 _/ _/ E-Mail: peter.mueller@fernuni-hagen.de _/ _/ WWW: www.informatik.fernuni-hagen.de/pi5/mueller.html _/ _/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/_/  1,, Mail-from: From leavens@cs.iastate.edu Wed Dec 15 11:17: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 LAA27716; Wed, 15 Dec 1999 11:17:14 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id LAA19452; Wed, 15 Dec 1999 11:17:09 -0600 (CST) Date: Wed, 15 Dec 1999 11:17:09 -0600 (CST) Message-Id: <199912151717.LAA19452@larch.cs.iastate.edu> From: "Gary T. Leavens" To: erikpoll@cs.kun.nl, Peter.Mueller@FernUni-Hagen.de CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Wed, 15 Dec 1999 17:08:15 +0100 (MET)) Subject: Re: JML-Interest: modifiable clauses for constructors ? *** EOOH *** Return-Path: Date: Wed, 15 Dec 1999 11:17:09 -0600 (CST) From: "Gary T. Leavens" To: erikpoll@cs.kun.nl, Peter.Mueller@FernUni-Hagen.de CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Wed, 15 Dec 1999 17:08:15 +0100 (MET)) Subject: Re: JML-Interest: modifiable clauses for constructors ? Erik, Peter, et al, > Date: Wed, 15 Dec 1999 17:08:15 +0100 (MET) > From: Erik Poll > > Dear jml-ers, > > In the "Preliminary Design of JML" paper, in the USMoney example (I have the > November 1999 version, there it's on page 25), the specifications of the two > constructors include > > modifiable: pennies; > > i.e. the constructors may modify the instance field pennies. > > But does it make sense to have a modifiable clause for an instance field > in the spec of a constructor ? The question of whether or not the value > of pennies in the post-state is equal to its \old value in the pre-state > seems meaningless, as there is no old value of pennies in a pre-state > to speak of. > > If one considers the value of pennies to be "modified" by the constructors > of USMoney, then by definition a constructor always "modifies" all instance > fields. > > I'd say that only for _static_ fields it make sense to say that a > constructor may modify it. Am I missing something ? I noticed for > instance that the definition of "pure constructor" also explicitly > refers to constructors modifying non-static fields. > From: Peter Mueller > Modifiable-clauses should mention all fields of objects that are allocated in > the prestate of a method/constructor and that might be changed during > method/constructor execution. > That is, there are instance fields that could occur in the > modifiable-clause of a constructor if the object to which the field belongs is > reachable from (1) a parameter of the constructor or (2) a static field. > So it is not sufficient to limit the modifiable-clauses of constructors to > static fields. However, I agree that in the example, pennies should not appear > in the modifiable-clause. Well, I've been using a definition of modification like we had in Larch/C++. This says that (section 6.2) "Mutation of an object means changing its abstract value. This can happen in one of two ways: * the object had a well-defined abstract value that is changed, or * the object had no well-defined abstract value, but it became well-defined." That is, in Java, if a field goes from unassigned to being assigned, that is considered a mutation. (Similarly if it goes from assigned to assigned and the value in it changes, of course.) So the following are mutations: unassigned -> good-value1 good-value1 -> good-value2 The idea is that there is a state change from unassigned to some good value. Quoting from 6.2.3 of the Larch/C++ manual: "Unlike earlier versions of Larch/C++ (and LCL), mutation of an object does not include deallocation or "trashing" it. (The current semantics is based the work of Chalin [Chalin95].) The modifies-clause only concerns objects that: * are allocated in both the pre- and post-states, and * are assigned in the post-state. It says that out of all such objects, only the objects described by the modifies-clause may have their abstract values changed." Now in Java, like C++, a constructor really just initializes storage. This is because it is called after the Java lanugage, due to operator "new", has allocated storage. The contract it makes with the Java system is the one specified. So the storage has already been allocated for the fields by the time a constructor is called. Thus, what we're concrened with is storage that is allocated that goes from having an ill-defined value (unassigned), to one with a good value, due to the initialization. This is, what I'm calling a modification. Thus, almost all constructors will need to list fields in their modifiable clause in JML, and I believe that the preliminary design document is right about these examples. Whether this semantics is intuitive, appropriate, etc. is another question. I agree it's confusing at first, because Java, like C++, gives client code the impression that constructors are allocating storage. But in fact, this is not the case. So I would argue that the proof rules for calling operator "new" and for a constructor call are different, in that the former involves allocation of the object (storage for its fields), and the latter doesn't allocate. If you think about the proof obligations for the constructor code itself, this makes sense. Clearly, you want to allow assignment to the fields in a construtor, and I believe that one sound rule is to not allow assignments to fields that aren't mentioned (perhaps implicitly as dependents) in modifiable clauses. If that's done, and if you don't list the fields in a constructor's specification, then you can't verify constructors. The verification logic just needs a different rule for doing "new C()" than it does for "C()". Does that make sense? (Clearly, we need reference material on JML...) Gary  1,, Mail-from: From owner-jml-interest-list Wed Dec 15 11:17:36 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id LAA27721 for jml-interest-list-outgoing; Wed, 15 Dec 1999 11:17:32 -0600 (CST) 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 LAA27716; Wed, 15 Dec 1999 11:17:14 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id LAA19452; Wed, 15 Dec 1999 11:17:09 -0600 (CST) Date: Wed, 15 Dec 1999 11:17:09 -0600 (CST) Message-Id: <199912151717.LAA19452@larch.cs.iastate.edu> From: "Gary T. Leavens" To: erikpoll@cs.kun.nl, Peter.Mueller@FernUni-Hagen.de CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Wed, 15 Dec 1999 17:08:15 +0100 (MET)) Subject: Re: JML-Interest: modifiable clauses for constructors ? Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Return-Path: Date: Wed, 15 Dec 1999 11:17:09 -0600 (CST) From: "Gary T. Leavens" To: erikpoll@cs.kun.nl, Peter.Mueller@FernUni-Hagen.de CC: jml-interest-list@cs.iastate.edu, leavens@cs.iastate.edu In-reply-to: (message from Erik Poll on Wed, 15 Dec 1999 17:08:15 +0100 (MET)) Subject: Re: JML-Interest: modifiable clauses for constructors ? Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Erik, Peter, et al, > Date: Wed, 15 Dec 1999 17:08:15 +0100 (MET) > From: Erik Poll > > Dear jml-ers, > > In the "Preliminary Design of JML" paper, in the USMoney example (I have the > November 1999 version, there it's on page 25), the specifications of the two > constructors include > > modifiable: pennies; > > i.e. the constructors may modify the instance field pennies. > > But does it make sense to have a modifiable clause for an instance field > in the spec of a constructor ? The question of whether or not the value > of pennies in the post-state is equal to its \old value in the pre-state > seems meaningless, as there is no old value of pennies in a pre-state > to speak of. > > If one considers the value of pennies to be "modified" by the constructors > of USMoney, then by definition a constructor always "modifies" all instance > fields. > > I'd say that only for _static_ fields it make sense to say that a > constructor may modify it. Am I missing something ? I noticed for > instance that the definition of "pure constructor" also explicitly > refers to constructors modifying non-static fields. > From: Peter Mueller > Modifiable-clauses should mention all fields of objects that are allocated in > the prestate of a method/constructor and that might be changed during > method/constructor execution. > That is, there are instance fields that could occur in the > modifiable-clause of a constructor if the object to which the field belongs is > reachable from (1) a parameter of the constructor or (2) a static field. > So it is not sufficient to limit the modifiable-clauses of constructors to > static fields. However, I agree that in the example, pennies should not appear > in the modifiable-clause. Well, I've been using a definition of modification like we had in Larch/C++. This says that (section 6.2) "Mutation of an object means changing its abstract value. This can happen in one of two ways: * the object had a well-defined abstract value that is changed, or * the object had no well-defined abstract value, but it became well-defined." That is, in Java, if a field goes from unassigned to being assigned, that is considered a mutation. (Similarly if it goes from assigned to assigned and the value in it changes, of course.) So the following are mutations: unassigned -> good-value1 good-value1 -> good-value2 The idea is that there is a state change from unassigned to some good value. Quoting from 6.2.3 of the Larch/C++ manual: "Unlike earlier versions of Larch/C++ (and LCL), mutation of an object does not include deallocation or "trashing" it. (The current semantics is based the work of Chalin [Chalin95].) The modifies-clause only concerns objects that: * are allocated in both the pre- and post-states, and * are assigned in the post-state. It says that out of all such objects, only the objects described by the modifies-clause may have their abstract values changed." Now in Java, like C++, a constructor really just initializes storage. This is because it is called after the Java lanugage, due to operator "new", has allocated storage. The contract it makes with the Java system is the one specified. So the storage has already been allocated for the fields by the time a constructor is called. Thus, what we're concrened with is storage that is allocated that goes from having an ill-defined value (unassigned), to one with a good value, due to the initialization. This is, what I'm calling a modification. Thus, almost all constructors will need to list fields in their modifiable clause in JML, and I believe that the preliminary design document is right about these examples. Whether this semantics is intuitive, appropriate, etc. is another question. I agree it's confusing at first, because Java, like C++, gives client code the impression that constructors are allocating storage. But in fact, this is not the case. So I would argue that the proof rules for calling operator "new" and for a constructor call are different, in that the former involves allocation of the object (storage for its fields), and the latter doesn't allocate. If you think about the proof obligations for the constructor code itself, this makes sense. Clearly, you want to allow assignment to the fields in a construtor, and I believe that one sound rule is to not allow assignments to fields that aren't mentioned (perhaps implicitly as dependents) in modifiable clauses. If that's done, and if you don't list the fields in a constructor's specification, then you can't verify constructors. The verification logic just needs a different rule for doing "new C()" than it does for "C()". Does that make sense? (Clearly, we need reference material on JML...) Gary  1, answered,, Mail-from: From owner-jml-interest-list Thu Dec 16 08:46:45 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id IAA16663 for jml-interest-list-outgoing; Thu, 16 Dec 1999 08:46:38 -0600 (CST) 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 IAA16659 for ; Thu, 16 Dec 1999 08:46:36 -0600 (CST) Received: from hera.cs.kun.nl by pandora.cs.kun.nl via hera.cs.kun.nl [131.174.33.2] with SMTP for id PAA21812 (8.8.8/3.12); Thu, 16 Dec 1999 15:46:29 +0100 (MET) Date: Thu, 16 Dec 1999 15:46:34 +0100 (MET) From: Erik Poll To: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: modifiable clauses for constructors ? In-Reply-To: <199912151717.LAA19452@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: Thu, 16 Dec 1999 15:46:34 +0100 (MET) From: Erik Poll To: jml-interest-list@cs.iastate.edu Subject: Re: JML-Interest: modifiable clauses for constructors ? In-Reply-To: <199912151717.LAA19452@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, Gary wrote: > Does that make sense? Yes, I see that one can decompose the statement "new C()" into - "new" that does the allocation, followed by - a constructor call "C()" that does some modification/initialization The instance fields then do exist in the pre-state of the constructor call, so they can (and typically should) be mentioned in a modifiable clause. However, I'm not sure if I understand all the implications of this. (I must say I haven't thought about proof rules for "new" and constructor calls, and of any advantages that the viewpoint above may have there.) The precise 'status' of instance fields in this pre-state of a constructor call is not really clear to me. Maybe it's best to consider a concrete example: class Test { int i ; Test() { ... } } If you say that i has been allocated before a call of the constructor Test(), does this also mean that i has been initialized to the default value for integers - ie. zero - before the constructor is called ? I'd say it should. After all, the Java language spec states explicitly that anything that is allocated is immediately initialized to its standard default value. The idea of variables being "unassigned" seems to be at odds with this Java 'philosophy'. (Indeed, in our formal semantics of Java there is no such thing as an "undefined" value). > Thus, almost all constructors will need to list fields in their > modifiable clause in JML, I was wondering whether it ever makes sense to have a constructor which does not declare _all_ instance fields as modifiable. (And, if this doesn't make sense, whether maybe it should be implicit that a constructor may modify all its instance fields.) In the example below the constructor fails to declare field i as modifiable: class AnotherTest { int i,j ; AnotherTest() \\@ behavior \\@ modifiable: j; } If you take the viewpoint that i is initialized to 0 before the constructor call, then I'd say that the spec above makes sense. It follows from the spec that the i-field of an object created using AnotherTest() will initially be 0. If you take the viewpoint that i is unassigned before the constructor call, then I'd say that the specification above is inconsistent. Whatever the implementation of AnotherTest(), after it's called the field i will have a good value. So any implementation of Test() modifies i, which is not allowed by the spec. By the same reasoning, any constructor specification which fails to declare all instance variables as modifiable would be inconsistent. Erik  1,, Mail-from: From leavens@cs.iastate.edu Thu Dec 16 09:58: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 JAA17825; Thu, 16 Dec 1999 09:58:11 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id JAA29396; Thu, 16 Dec 1999 09:58:06 -0600 (CST) Date: Thu, 16 Dec 1999 09:58:06 -0600 (CST) Message-Id: <199912161558.JAA29396@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, 16 Dec 1999 15:46:34 +0100 (MET)) Subject: Re: JML-Interest: modifiable clauses for constructors ? *** EOOH *** Return-Path: Date: Thu, 16 Dec 1999 09:58:06 -0600 (CST) 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, 16 Dec 1999 15:46:34 +0100 (MET)) Subject: Re: JML-Interest: modifiable clauses for constructors ? Erik, et al, > Date: Thu, 16 Dec 1999 15:46:34 +0100 (MET) > From: Erik Poll > > Gary wrote: > > > Does that make sense? > > Yes, I see that one can decompose the statement "new C()" into > - "new" that does the allocation, followed by > - a constructor call "C()" that does some modification/initialization > The instance fields then do exist in the pre-state of the constructor call, > so they can (and typically should) be mentioned in a modifiable clause. Ok. > The precise 'status' of instance fields in this pre-state of a constructor > call is not really clear to me. > Maybe it's best to consider a concrete example: > > class Test { > > int i ; > > Test() { ... } > } > > If you say that i has been allocated before a call of the constructor Test(), > does this also mean that i has been initialized to the default value for > integers - ie. zero - before the constructor is called ? > > I'd say it should. After all, the Java language spec states explicitly that > anything that is allocated is immediately initialized to its standard default > value. The idea of variables being "unassigned" seems to be at odds with this > Java 'philosophy'. (Indeed, in our formal semantics of Java there is no such > thing as an "undefined" value). Yes, I didn't check the Java Language Specification before writing my reply before. But in Section 12.5, it says just what you suggest: "all the instance variables ... are initialized to their default values..." So your characterization is more accurate for Java. It does also talk about calling the constructor as in a procedure call. > > Thus, almost all constructors will need to list fields in their > > modifiable clause in JML, > > I was wondering whether it ever makes sense to have a constructor which > does not declare _all_ instance fields as modifiable. (And, if this > doesn't make sense, whether maybe it should be implicit that a > constructor may modify all its instance fields.) > In the example below the constructor fails to declare field i as modifiable: > > class AnotherTest { > > int i,j ; > > AnotherTest() > \\@ behavior > \\@ modifiable: j; > } That should be: class AnotherTest { int i,j ; AnotherTest() /*@ behavior @ modifiable: j; @*/ } but yes, this is fine. Now that we know that instance variables are initialized to default values by the language, we can see that new AnotherTest() creates an object where i has the default value. As you say... > If you take the viewpoint that i is initialized to 0 before the constructor > call, then I'd say that the spec above makes sense. It follows from the > spec that the i-field of an object created using AnotherTest() will > initially be 0. Right. > If you take the viewpoint that i is unassigned before the constructor call, > then I'd say that the specification above is inconsistent. Whatever the > implementation of AnotherTest(), after it's called the field i will have > a good value. So any implementation of Test() modifies i, which is not > allowed by the spec. > By the same reasoning, any constructor specification which fails to declare > all instance variables as modifiable would be inconsistent. We don't take this viewpoint. Thanks for clearing this issue up for us. I appreciate it. Gary  1,, Mail-from: From owner-jml-interest-list Mon Dec 20 17:46:46 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id RAA04767 for jml-interest-list-outgoing; Mon, 20 Dec 1999 17:46:42 -0600 (CST) 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 RAA04667; Mon, 20 Dec 1999 17:37:44 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id RAA20165; Mon, 20 Dec 1999 17:36:07 -0600 (CST) Date: Mon, 20 Dec 1999 17:36:07 -0600 (CST) Message-Id: <199912202336.RAA20165@larch.cs.iastate.edu> From: "Gary T. Leavens" To: bart@cs.kun.nl, marieke@cs.kun.nl, joachim@cs.kun.nl, erikpoll@cs.kun.nl, s.j.h.kent@ukc.ac.uk, stata@pa.dec.com, rustan@pa.dec.com, visray@hotmail.com (Rayan), htewis@curry.de (Holger_Tewis), jml-interest-list@cs.iastate.edu CC: jml@cs.iastate.edu Subject: JML-Interest: New Release of JML, 1.3 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Return-Path: Date: Mon, 20 Dec 1999 17:36:07 -0600 (CST) From: "Gary T. Leavens" To: bart@cs.kun.nl, marieke@cs.kun.nl, joachim@cs.kun.nl, erikpoll@cs.kun.nl, s.j.h.kent@ukc.ac.uk, stata@pa.dec.com, rustan@pa.dec.com, visray@hotmail.com (Rayan), htewis@curry.de (Holger_Tewis), jml-interest-list@cs.iastate.edu CC: jml@cs.iastate.edu Subject: JML-Interest: New Release of JML, 1.3 Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Hi, We've just made another release of JML, 1.3, which is available from the JML ftp site: ftp://ftp.cs.iastate.edu/pub/leavens/JML/ in the file JML.1.3.zip or from the JML web page (http://www.cs.iastate.edu/~leavens/JML.html). This release completes the integration of JML's syntax with ESC/Java. There was an interim release, 1.2, which has a syntax that isn't much different than that found in 1.3, but the documentation of 1.3 is much improved over that of 1.2 and earlier releases. (You can browse the documents, and see the new syntax, by starting at the web page.) If you haven't tried release 1.2 before, you should be warned that the syntax is quite different from JML 1.1. See the file esc-jml-diffs.txt in the top directory of the release for details. However, there are even differences in syntax from 1.2, although most of these relate to seldom-used features. We hope that the grammar is fairly stable now, although we do plan to add better support for putting specifications in documentation comments. Major improvements in this release are: - Subclassing contracts (callable and accessible clauses) split out into their own section, because they don't work with "also" - Implications put into their own section (implies_that), and examples put into their own section (for_example) - The meaning of an example now is stronger, and allows it to be used as a test case. - Restricted syntax in the modifiable clause, with new \fields_of syntax for specifying the fields of objects or sets of objects Please let us know your comments on JML, and if you find bugs. There are some already documented bugs in the BUGS.txt file... Also, we have gone to some pain to make development possible (although it may not yet be easy) outside of Iowa State. Since JML is open source, feel free to send us code with bug fixes also! Special thanks to Clyde Ruby for many bug fixes and being the grammar mesiter for JML. Thanks to Raymie Stata and Rustan Leino for conversations that led to the gramar changes. See the preliminary design document for other acknowledgments. Gary  1,, Mail-from: From leavens@cs.iastate.edu Tue Dec 21 18:26: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 SAA24482; Tue, 21 Dec 1999 18:26:05 -0600 (CST) Received: (from leavens@localhost) by larch.cs.iastate.edu (8.9.0/8.9.0) id SAA02621; Tue, 21 Dec 1999 18:25:56 -0600 (CST) Date: Tue, 21 Dec 1999 18:25:56 -0600 (CST) Message-Id: <199912220025.SAA02621@larch.cs.iastate.edu> From: "Gary T. Leavens" To: jml-interest@cs.iastate.edu CC: leavens@cs.iastate.edu, rustan@pa.dec.com Subject: lightweight specifications and the default for JML's modifiable clause *** EOOH *** Return-Path: Date: Tue, 21 Dec 1999 18:25:56 -0600 (CST) From: "Gary T. Leavens" To: jml-interest@cs.iastate.edu CC: leavens@cs.iastate.edu, rustan@pa.dec.com Subject: lightweight specifications and the default for JML's modifiable clause Hi, I'm a bit worried about how the default for JML's modifiable clause interacts with the use of lightweight specifications. Here's the problem. In JML, following the lead of ESC/Java, one can (now) write specifications that include just a requires clause, or just an ensures clause. For example, public abstract class defaults_question { /*@ spec_public @*/ private int x; public void inc_x() //@ requires: x < Integer.MAX_VALUE; { x = x + 1; } } The idea is that you're supposed to say just what is needed in such lightweight specifications, and the result should be an underspecification if anything. However, this seems to interact badly with the default for the modifiable clause, which is modifiable: \nothing; Because of this, in the above example, the implementation given is clearly not correct. Also, the default if one completely omits a specification is to not allow modification, which means that one can never have a correct refinement that permits modification. I wonder if we should have different defaults for lightweight specifications in JML than for the long form of specifications. This seems possible, because one can write a specification using one of the keywords "behavior", "normal_behavior", or "exceptional_behavior", or one can omit these. While the syntax and meaning are currently the same if one uses "behavior" or not, we could perhaps use this distinction to have different defaults for the modifiable clause. I would propose that in a lightweight specifiaction case (no "behavior" or "x_behavior" keyword), and in completely omitted specifications, the default for the modifiable clause would be: modifiable: \everything; while when one of the behavior keywords is used, the default would be modifiable: \nothing; The idea is that, when you use one of the behavior keywords, you are presumably trying to give a complete specification. If you are tring to just say the minimum, you wouldn't use such a keyword. Note that the "also" of "modifiable: \everything;" and some other specification is essentially the other specification. Rustan, when the modifiable clause is omitted in the specification of a method in ESC/Java, does ESC/Java complain when assignments are made in the method? Your thoughts on this subject are welcome. Gary  1,, Mail-from: From rustan@pa.dec.com Tue Dec 21 19:13:23 1999 Return-Path: Received: from mail2.digital.com (mail2.digital.com [204.123.2.56]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id TAA25031; Tue, 21 Dec 1999 19:13:21 -0600 (CST) Received: from neuf.pa.dec.com (neuf.pa.dec.com [16.4.80.69]) by mail2.digital.com (8.9.2/8.9.2/WV2.0g) with SMTP id RAA28224; Tue, 21 Dec 1999 17:13:17 -0800 (PST) Received: by neuf.pa.dec.com; id AA27754; Tue, 21 Dec 1999 17:13:17 -0800 Message-Id: <199912220113.AA27754@neuf.pa.dec.com> To: "Gary T. Leavens" Cc: jml-interest@cs.iastate.edu Subject: Re: lightweight specifications and the default for JML's modifiable clause In-Reply-To: Message of Tue, 21 Dec 1999 18:25:56 -0600 (CST) from "Gary T. Leavens" <199912220025.SAA02621@larch.cs.iastate.edu> Date: Tue, 21 Dec 1999 17:13:17 -0800 From: "K. Rustan M. Leino" X-Mts: smtp *** EOOH *** Return-Path: To: "Gary T. Leavens" Cc: jml-interest@cs.iastate.edu Subject: Re: lightweight specifications and the default for JML's modifiable clause In-Reply-To: Message of Tue, 21 Dec 1999 18:25:56 -0600 (CST) from "Gary T. Leavens" <199912220025.SAA02621@larch.cs.iastate.edu> Date: Tue, 21 Dec 1999 17:13:17 -0800 From: "K. Rustan M. Leino" X-Mts: smtp | From: "Gary T. Leavens" | [...] | public void inc_x() | //@ requires: x < Integer.MAX_VALUE; | { | x = x + 1; | } | [...] | Rustan, when the modifiable clause is omitted in the specification of a | method in ESC/Java, does ESC/Java complain when assignments are made in | the method? ESC/Java is intended for lightweight specifications and it uses "modifiable \nothing" as the default modifies clause. While I'm happy with this choice for ESC/Java, it does turn out that ESC/Java currently does not enforce modifies clauses. Thus, ESC/Java would not complain about the assignment to "x" in your example. We do have a plan for doing partial modifies clause checking, but we've never implemented it. That plan is that "o.f" is allowed to be modified if either "o.f" is mentioned in a modifies clause, "o" is newly allocated, or "o" not a formal parameter or static field. If we did implement this plan, I would still be happy with the choice of "modifiable \nothing" as the default modifies clause. Rustan  1, answered, filed,, Mail-from: From rustan@pa.dec.com Tue Dec 21 19:13:23 1999 Return-Path: Received: from mail2.digital.com (mail2.digital.com [204.123.2.56]) by css-1.cs.iastate.edu (8.9.0/8.9.0) with ESMTP id TAA25031; Tue, 21 Dec 1999 19:13:21 -0600 (CST) Received: from neuf.pa.dec.com (neuf.pa.dec.com [16.4.80.69]) by mail2.digital.com (8.9.2/8.9.2/WV2.0g) with SMTP id RAA28224; Tue, 21 Dec 1999 17:13:17 -0800 (PST) Received: by neuf.pa.dec.com; id AA27754; Tue, 21 Dec 1999 17:13:17 -0800 Message-Id: <199912220113.AA27754@neuf.pa.dec.com> To: "Gary T. Leavens" Cc: jml-interest@cs.iastate.edu Subject: Re: lightweight specifications and the default for JML's modifiable clause In-Reply-To: Message of Tue, 21 Dec 1999 18:25:56 -0600 (CST) from "Gary T. Leavens" <199912220025.SAA02621@larch.cs.iastate.edu> Date: Tue, 21 Dec 1999 17:13:17 -0800 From: "K. Rustan M. Leino" X-Mts: smtp *** EOOH *** Return-Path: To: "Gary T. Leavens" Cc: jml-interest@cs.iastate.edu Subject: Re: lightweight specifications and the default for JML's modifiable clause In-Reply-To: Message of Tue, 21 Dec 1999 18:25:56 -0600 (CST) from "Gary T. Leavens" <199912220025.SAA02621@larch.cs.iastate.edu> Date: Tue, 21 Dec 1999 17:13:17 -0800 From: "K. Rustan M. Leino" X-Mts: smtp | From: "Gary T. Leavens" | [...] | public void inc_x() | //@ requires: x < Integer.MAX_VALUE; | { | x = x + 1; | } | [...] | Rustan, when the modifiable clause is omitted in the specification of a | method in ESC/Java, does ESC/Java complain when assignments are made in | the method? ESC/Java is intended for lightweight specifications and it uses "modifiable \nothing" as the default modifies clause. While I'm happy with this choice for ESC/Java, it does turn out that ESC/Java currently does not enforce modifies clauses. Thus, ESC/Java would not complain about the assignment to "x" in your example. We do have a plan for doing partial modifies clause checking, but we've never implemented it. That plan is that "o.f" is allowed to be modified if either "o.f" is mentioned in a modifies clause, "o" is newly allocated, or "o" not a formal parameter or static field. If we did implement this plan, I would still be happy with the choice of "modifiable \nothing" as the default modifies clause. Rustan  1, answered,, Mail-from: From owner-jml-interest-list Wed Dec 22 10:31:44 1999 Return-Path: Received: (from mdomo@localhost) by css-1.cs.iastate.edu (8.9.0/8.9.0) id KAA06195 for jml-interest-list-outgoing; Wed, 22 Dec 1999 10:31:33 -0600 (CST) 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 KAA06190; Wed, 22 Dec 1999 10:31:27 -0600 (CST) Received: (from leavens@localhost) by ren.cs.iastate.edu (8.9.0/8.9.0) id KAA23932; Wed, 22 Dec 1999 10:31:24 -0600 (CST) Date: Wed, 22 Dec 1999 10:31:24 -0600 (CST) Message-Id: <199912221631.KAA23932@ren.cs.iastate.edu> From: "Gary T. Leavens" To: rustan@pa.dec.com, jml-interest@cs.iastate.edu CC: leavens@cs.iastate.edu In-reply-to: <199912220113.AA27754@neuf.pa.dec.com> (rustan@pa.dec.com) Subject: JML-Interest: Re: lightweight specifications and the default for JML's modifiable clause Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk *** EOOH *** Return-Path: Date: Wed, 22 Dec 1999 10:31:24 -0600 (CST) From: "Gary T. Leavens" To: rustan@pa.dec.com, jml-interest@cs.iastate.edu CC: leavens@cs.iastate.edu In-reply-to: <199912220113.AA27754@neuf.pa.dec.com> (rustan@pa.dec.com) Subject: JML-Interest: Re: lightweight specifications and the default for JML's modifiable clause Sender: owner-jml-interest-list@cs.iastate.edu Precedence: bulk Rustan, et al, I wonder if having a default for the modifiable clause in lightweight specifications be "not specified" would be better. This could be interpreted as "everything" for purposes of formal verification, and it would turn off checking in static analysis tools like ESC/Java. That way we wouldn't lose information that the modifiable clause simply wasn't specified, instead of trying to choose a default. Rustan, while I understand that you would be happy with "modifiable: \nothing" as the default, even for lightweight specifications even if you did enforce it, I'm not so sure it fits with your philosophy. Doing that would effectively mean people would have to specify the modifiable clause for everything that made assignments. That doesn't seem so lightweight. Gary > Cc: jml-interest@cs.iastate.edu > Date: Tue, 21 Dec 1999 17:13:17 -0800 > From: "K. Rustan M. Leino" > X-Mts: smtp > > > | From: "Gary T. Leavens" > | [...] > | public void inc_x() > | //@ requires: x < Integer.MAX_VALUE; > | { > | x = x + 1; > | } > | [...] > | Rustan, when the modifiable clause is omitted in the specification of a > | method in ESC/Java, does ESC/Java complain when assignments are made in > | the method? > > ESC/Java is intended for lightweight specifications and it uses "modifiable > \nothing" as the default modifies clause. While I'm happy with this > choice for ESC/Java, it does turn out that ESC/Java currently does > not enforce modifies clauses. Thus, ESC/Java would not complain > about the assignment to "x" in your example. > > We do have a plan for doing partial modifies clause checking, but > we've never implemented it. That plan is that "o.f" is allowed to > be modified if either "o.f" is mentioned in a modifies clause, "o" > is newly allocated, or "o" not a formal parameter or static field. > If we did implement this plan, I would still be happy with the choice > of "modifiable \nothing" as the default modifies clause. > > Rustan >