--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on December 2014 ---
Hello, Le 08/12/2014 10:49, Debasmita Lohar a ?crit : > I am looking for a tool that computes weakest precondition of a program. Another option would be to use Why3 directly, instead of Frama-C. For example, on attached program, if you run: mkdir out why3 prove -o out -P alt-ergo compute.mlw Then in directory out/ you have generated VC: """ $ tail -3 out/compute-Compute-WP_parameter_f.why goal WP_parameter_f : (forall x:int. (((0 <= x) and (x <= 10)) -> ((1 <= (x + 1)) and ((x + 1) <= 11)))) """ Why3 can be found here: http://why3.lri.fr/ There is also a dedicated mailing-list if you have questions. For sake of completness, SPARK 2014 also generates VCs in a subdirectory: http://www.spark-2014.org/ Best regards, david -- David MENTR? - Research engineer, Ph.D. Formal Methods and tools MITSUBISHI ELECTRIC R&D Centre Europe (MERCE) Phone: +33 2 23 45 58 29 / Fax: +33 2 23 45 58 59 http://www.fr.mitsubishielectric-rce.eu -------------- next part -------------- module Compute use import int.Int let f x requires { 0 <= x <= 10 } ensures { 1 <= result <= 11 } = x + 1 end