The Coq mailing list

[Julien Narboux <jnarboux AT narboux.fr>]

On 02/11/2011 19:12, Andrew Pennebaker wrote:

Thanks all, especially for the Frama-C link.

Adam, would Coq-based solutions be .vo files for obfuscation? <- That can't be right; a secret proof is no proof.

For anyone who hasn't used QuickCheck, its forAll function is a bit of a misnomer. Perhaps it should be named forRelativelyFewTestCasesConsideringTheInfiniteExpanseOfNumbers.

Aye, Haskell and Coq don't completely overlap, since Coq is implemented in OCaml. But QuickCheck isn't only in Haskell; there's already a port for OCaml.

Jesper: Exactly. QuickCheck could serve as a way to detect trivial counterexamples in a Coq proof. I'd like to try porting QuickCheck to Coq, but first I need to learn how to use Coq (hence the Peirce's Law thread).

You can have a look to the implementations of QuickCheck and Nitpick in Isabelle by Tobias Nipkow, Stefen Berghofer and Jasmin Christian Blanchette.

Tom, which file in the rippling package, and which lines? I don't know where to begin looking, since I don't expect Sean to use the naming conventions of QuickCheck, since forAll would overlap with Coq's forall.

Cheers,

Andrew Pennebaker

www.yellosoft.us

On Wed, Nov 2, 2011 at 9:28 AM, Claude Marche <Claude.Marche AT inria.fr> wrote:

Hi,

Generally speaking, moving directly from unit testing to Coq proof seems to me a giant leap in the universe of formal methods.

Anyway, If you are interested in verifying complex behavior of C programs using Coq, then you need some front-end above Coq since Coq does not understand C code natively.
I'd like to suggest to look at the Frama-C environment for static analysis of C code, and in particular its two deductive verification plugins WP (http://frama-c.com/wp.html) and Jessie (http://krakatoa.lri.fr/, also handles Java code). Both of them are able to produce proof obligations in the Coq syntax, but also several other provers, with various degree of automation.

Hope this helps,

- Claude

Le 01/11/2011 18:33, Andrew Pennebaker a écrit :

I'm familiar with programming, and I'm familiar with formal methods, but I have trouble understanding the various Coq tutorials.

What prevents me from cheating by assuming enough hypotheses that my goal is reached?

How can Coq A) prove that an algorithm for reversing a string is correct and B) prove that a C implementation of the algorithm is correct?

I'm used to unit testing my programs with QuickCheck, a probabilistic verifier that brute forces properties such as propReversible :: String -> Bool (Haskell notation). How easy would it be to refactor QuickCheck tests into Coq tests? If Coq verifies that my C code is correct, how should I provide "certificates" of verification? Is it enough to provide a code comment to a URL of a .v file?

Cheers,

Andrew Pennebaker

www.yellosoft.us