home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #26 / NN_1992_26.iso / spool / comp / theory / 2352 < prev    next >
Encoding:
Text File  |  1992-11-07  |  1.6 KB  |  35 lines
  1. Newsgroups: comp.theory
  2. Path: sparky!uunet!zaphod.mps.ohio-state.edu!darwin.sura.net!udel!sbcs.sunysb.edu!sbcs!stark
  3. From: stark@cs.sunysb.edu (Gene Stark)
  4. Subject: Re: Synthesizing loop invariants -- unsolvable?
  5. In-Reply-To: dsims@don.ece.uc.edu's message of Thu, 5 Nov 1992 23: 06:48 GMT
  6. Message-ID: <STARK.92Nov6074546@sbstark.cs.sunysb.edu>
  7. Sender: usenet@sbcs.sunysb.edu (Usenet poster)
  8. Nntp-Posting-Host: sbstark
  9. Organization: SUNY at Stony Brook Computer Science Dept.
  10. References: <1992Nov5.230648.23466@babbage.ece.uc.edu>
  11. Date: Fri, 6 Nov 1992 12:45:46 GMT
  12. Lines: 21
  13.  
  14. >I've been thrashing about with the problem of automatically generating
  15. >loop invariants for the purposes of program verification.  Is the general
  16. >case of automatically synthesizing a loop invariant for any given loop
  17. >unsolvable?
  18.  
  19. The standard proof of (Cook) relative completeness for Hoare logics proceeds
  20. by showing how, given a desired postcondition expressed as a formula in a
  21. suitable first-order language, one can can construct a formula expressing
  22. the weakest precondition that will guarantee the postcondition upon
  23. termination.  Finding these weakest preconditions includes the problem of
  24. finding loop invariants.  The proof actually constructs the formulas, so
  25. the problem of synthesizing loop invariants is solvable.  However, the
  26. formulas themselves are in no way guaranteed to be "simple" or "understandable"
  27. as they involve a number-theoretic encoding of possible program executions.
  28.  
  29. For more information, a good reference is: "Mathematical Theory of Program
  30. Correctness", by de Bakker.
  31.  
  32.                             - Gene Stark
  33.  
  34.  
  35.