--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on March 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] A small plugin to specific which coq strategy to use per block annotation



Hi everybody,

I just committed a plugin that allows to specify for code annotations (spec of blocks) which coq strategy to apply. I hope it can be useful for some of you.

Strategies should be declared as ACSL terms and you should declare the predicate use_strategy:

/*@ axiomatic ellipsoids_proof_tactics {
  @   type ellipsoids_tactics = Intuition | Tactic2;
  @   predicate use_strategy (ellipsoids_tactics t);
  @ }
*/

Then each block specification can use the following grammar extension:

/*@ requires x < 0;
  @ ensures \result <= 0; 
*/
int plus_one (int x) {
int y,z;
/*@ ensures y <= 0; 
  @ PROOF_TACTIC (use_strategy (Intuition));
*/
{
y = x + 1;
}
/*@ ensures z <= 0; 
  @ PROOF_TACTIC (use_strategy (Tactic2));
*/
{
z = 2 * y;
}
return z;
}


The plugin will call WP on each of those block annotations and update the default coq strategy with the specified proof tactic.

URL: https://github.com/ploc/wp-local-tactic

For the moment only block specification are concerned and *not* function specifications.


Cheers

pl
-- 
Pierre-Lo?c Garoche
Research Scientist @ ONERA
pierre-loic.garoche at onera.fr - pierre-loic-garoche at uiowa.edu
http://www.onera.fr/staff/pierre-loic-garoche/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: Digital signature
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130312/79b73b3d/attachment.pgp>