<p>Which is the easiest way to find a valid <strong>Invariant</strong> for a <em>While Program</em> in the Hoare program correctness verification? <br>
Is there a "guided" way to do that?</p>

CC BY-SA 3.0
2015-02-06T21:05:00.200Z
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.
Martin Berger
CC BY-SA 3.0
2015-02-07T02:43:41.627Z
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: http://rise4fun.com/dafny/Hello and Interproc: http://pop-art.inrialpes.fr/interproc/interprocweb.cgi web-interfaces for two examples of many many tools out there.
Vijay D
CC BY-SA 3.0
2015-12-13T18:20:08.110Z
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.
Sriram S
<linear-programming><model-checking><correctness>
Hoare program correctness
Nk SP
# Hoare program correctness

(Asked by: username_0 on 2015-02-06)

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?

**Tags:** linear-programming, model-checking, correctness

> **Comments:**
> **username_1**: 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.  
> **username_2**: 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: http://rise4fun.com/dafny/Hello and Interproc: http://pop-art.inrialpes.fr/interproc/interprocweb.cgi web-interfaces for two examples of many many tools out there.  
> **username_3**: 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 username_2 mentions are also good approaches but on restricted/pre-defined types of invariants.  

---

## 0 answers

