Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Questions on wp about _Bool, inductive predicates and Coq

Le 15.05.2014 13:09, Lo?c Correnson a ?crit?:
> It is also my guess. Have also a look to frama-c -print-*-path
> options, -share and -wp-share options.

Everything seems normal about the path but since I found a workaround 
it's hard
to test it now.

> Of course, this is the nature of inductive types, indeed.
> You should also consider the following methodology :
> 
> 1. Declare in Coq your inductive predicate, in a self-consistent Coq 
> module.
> 
> 2. Declare an *abstract* predicate in ACSL, and state the useful
> lemmas you want to USE for proving your code.
> 
> 3. Define 	a WP-driver (WP ? 2.3.10) that informs WP to link the ACSL
> predicate to your Coq module.
> 
> And then, your done in a very sound way.
> This can be generalized for types and many other interesting things.

This seems to be an interesting methodology, that offers a lot of 
possibilities.


Thanks for yours answers.


Guillaume Davy