home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #26 / NN_1992_26.iso / spool / comp / theory / 2362 < prev    next >
Encoding:
Internet Message Format  |  1992-11-08  |  3.2 KB
  1. Path: sparky!uunet!ogicse!das-news.harvard.edu!cantaloupe.srv.cs.cmu.edu!deutsch
  2. From: deutsch+@cs.cmu.edu (Alain Deutsch)
  3. Newsgroups: comp.theory
  4. Subject: Re: Synthesizing loop invariants -- unsolvable?
  5. Message-ID: <BxB9xH.3ty.2@cs.cmu.edu>
  6. Date: 6 Nov 92 20:22:26 GMT
  7. Article-I.D.: cs.BxB9xH.3ty.2
  8. References: <1992Nov5.230648.23466@babbage.ece.uc.edu>
  9. Sender: news@cs.cmu.edu (Usenet News System)
  10. Organization: School of Computer Science, Carnegie Mellon
  11. Lines: 83
  12. Nntp-Posting-Host: proof.ergo.cs.cmu.edu
  13.  
  14. Problem: explain why invariants are not computable in general.
  15.  
  16. Sketch: Consider a   program P  and  its operational  semantics defined by  a
  17. Kripke structure:
  18.  
  19.     (State, -->, V)
  20.  
  21. where State is  a set  of  states   (usually infinite because   of  integers,
  22. recursion or dynamic allocation); --> is a transition relation on State and V
  23. is a valuation function which maps each state \gamma  to the set V(\gamma) of
  24. atomic formulae true in this state.
  25.  
  26. Now because of the obvious isomorphism between program predicates and sets of
  27. states (a predicate \Phi can be represented by the set of  states in which it
  28. is true), the strongest global invariant is by definition the  sets of states
  29. that can be reached from some set of initial I through the transitive closure
  30. of the transition relation -->, which by [Pa69,Cl79,Co81] can be  computed as
  31. a fixpoint, using the notation post(-->)(X) = {y | x \in X  ^  x --> y}:
  32.  
  33.            *
  34.  SGI[P]  = post(--> )(I)
  35.  
  36.          = lfp(\lambda X. I \cup post(-->)(X))
  37.  
  38.  
  39. This least fixpoint  is well defined, as it  is the fixpoint   of a monotonic
  40. operator on the (obviously complete) lattice of sets of states.
  41.  
  42. Now because the lattice of sets of  states has ordinal height \omega whenever
  43. the sets of states is infinite, it follows that the computation of this least
  44. fixpoint can require up to \omega iterations. Hence  SGI[P] is not computable
  45. this way.
  46.  
  47. Another argument, less intuitive but probably stronger, based on Godel second
  48. incompleteness theorem, appears in section 7.4.2.3.3 of [Co90].
  49.  
  50. References:
  51.  
  52. @Article{Park69,
  53.   author =      "Park,D.M.R.",
  54.   title =      "Fixpoint induction and proof program properties",
  55.   journal =      "Machine {Intelligence}",
  56.   year =      1969,
  57.   volume =      5,
  58.   pages =      "59--78",
  59.   note =      "Edinburgh University Press"
  60. }
  61.  
  62. @Article{Clarke79,
  63.   author =      "Clarke,E.M.",
  64.   title =      "Program Invariants as Fixedpoints",
  65.   journal =      "Computing",
  66.   year =      1979,
  67.   volume =      21,
  68.   pages =      "273--294"
  69. }
  70.  
  71. @InProceedings{Cousot81,
  72.   author =      "Cousot,P.",
  73.   booktitle =      "Program Flow Analysis: Theory and Applications",
  74.   title =      "Semantic foundations of program analysis",
  75.   publisher =      "Prentice-Hall",
  76.   year =      1981,
  77.   pages =      "303--342"
  78. }
  79.  
  80. @InBook{Cousot90,
  81.   author =      "Cousot,P.",
  82.   title =      "Methods and Logics for Proving Programs",
  83.   pages =        "841--994",
  84.   chapter =      "15",
  85.   editor =      "van Leeuwen,J.",
  86.   booktitle =      "Formal Models and Semantics",
  87.   publisher =      "Elsevier Science Publisher \& The MIT Press",
  88.   year =      1990,
  89.   volume =      "B",
  90.   note =         "ISBN 0-444-88074-7"
  91. }
  92. -- 
  93. ----
  94. Alain Deutsch, Research Associate
  95. Carnegie Mellon University -- School of Computer Science
  96. Pittsburgh, PA 15213-3891, USA.
  97.