Which is the easiest way to find a valid Invariant for a While Program in the Hoare program correctness verification?
Is there a "guided" way to do that?

  • 3
    $\begingroup$ If you want "a valid invariant" you can always use "True". What you probably mean is a valid invariant that helps you to prove easily (!) about a program whatever you need to prove. That's non-computable in general. $\endgroup$ Feb 6, 2015 at 21:05
  • 1
    $\begingroup$ I think it would help if you gave an example of a program and what you want to prove about it and also if you describe what you know about deriving invariants. Try the Dafny: rise4fun.com/dafny/Hello and Interproc: pop-art.inrialpes.fr/interproc/interprocweb.cgi web-interfaces for two examples of many many tools out there. $\endgroup$
    – Vijay D
    Feb 7, 2015 at 2:43
  • $\begingroup$ If you read the Manna+Pnueli book, they will talk about the basics of synthesizing invariants in a semi-automatic fashion using "top-down" or "bottom-up" methods. The programs that Vijay D mentions are also good approaches but on restricted/pre-defined types of invariants. $\endgroup$
    – Sriram S
    Dec 13, 2015 at 18:20


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.