home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #26 / NN_1992_26.iso / spool / comp / theory / 2350 < prev    next >
Encoding:
Internet Message Format  |  1992-11-07  |  1.7 KB
  1. Path: sparky!uunet!europa.asd.contel.com!emory!swrinde!zaphod.mps.ohio-state.edu!uwm.edu!spool.mu.edu!sgiblab!munnari.oz.au!comp.vuw.ac.nz!waikato.ac.nz!aukuni.ac.nz!cs18.cs.aukuni.ac.nz!jeremy
  2. Newsgroups: comp.theory
  3. Subject: Re: Synthesizing loop invariants -- unsolvable?
  4. Message-ID: <1992Nov6.053549.1408@cs.aukuni.ac.nz>
  5. From: jeremy@cs.aukuni.ac.nz (Jeremy Gibbons)
  6. Date: Fri, 6 Nov 1992 05:35:49 GMT
  7. References: <1992Nov5.230648.23466@babbage.ece.uc.edu>
  8. Organization: Computer Science Dept. University of Auckland
  9. Cc: jeremy@cs.aukuni.ac.nz
  10. Lines: 28
  11.  
  12. In <1992Nov5.230648.23466@babbage.ece.uc.edu> dsims@don.ece.uc.edu (David Sims) writes:
  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. >I suspect it is but cannot come up with a proof.  Any help would be
  20. >appreciated.
  21.  
  22. Of course it's solvable; "true" is an invariant of every loop. :-)
  23.  
  24. Seriously, the halting problem reduces to finding a *variant*, so you can't
  25. write a program to find variants. Presumably the question you meant to ask
  26. was, is the problem of finding an invariant sufficiently strong to
  27. establish a given postcondition, assuming termination, computable? (This is
  28. equivalent to checking partial correctness of while-programs, right?) My
  29. intuition is also that it is uncomputable, but I too can't come up with a
  30. proof off the top of my head.
  31.  
  32. Jeremy
  33.  
  34. ---
  35. Jeremy Gibbons <jeremy@cs.aukuni.ac.nz>         tel: +64 9 373 7599
  36.    Department of Computer Science,              fax: +64 9 373 7453
  37.    University of Auckland, Private Bag 92019, Auckland, New Zealand.
  38.  
  39.  
  40.