--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on March 2013 ---
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>