Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Full-Name: Joshua D. Guttman
Posted-Date: Thu, 17 Jun 93 17:06:14 -0400
Date: Thu, 17 Jun 93 17:06:14 -0400
From: guttman@linus.mitre.org
Message-Id: <9306172106.AA03337@circe.mitre.org>
To: info-hol@ted.cs.uidaho.edu
Cc: parnas%triose.eng.mcmaster.CA@nnsc.nsf.net
Subject: Re: Parnas: "some theorems we should prove"

I formalized and proved the theorems using IMPS, an Interactive Mathematical
Proof System.  They were very routine to formalize, and extremely easy to
prove.  Almost half the proofs consisted only of a call to the Imps simplifier.
None of the others required any ingenuity, or more than half a dozen steps.  I
also proved a few lemmas about the floor operator; a couple of these were
slightly more involved.  

I found that the Imps logic with its partial functions made the formalization
quite simple and straightforward.  For instance, square root can be defined in
the expected way, and it can be proved that the square root is well-defined for
non-negative arguments.  I think that this genuine piece of mathematical
content was left out of the PVS formalization.  

Total elapsed human time to do this exercise was about two hours using the
first version of the Parnas paper.  When the revised version was mentioned, I
realized that my patch to the defective Figure 15 was not the intended version.
So I spent another hour or so, most of which was spent puzzling whether the
condition given really characterized "palindrome".

I will ask Jeff Joyce if I can post the Imps theory file and a latex file
showing all of the theorems on the UBC ftp server.  Then you will be able to
look at them in detail.

  Josh