--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on May 2014 ---
[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