--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on March 2015 ---
Hello, 2015-03-10 5:05 GMT+01:00 Wenrui Meng <wenrui at seas.upenn.edu>: > > I didn't find much related examples resource for beginner. Can any one point > out examples by WP plug? > I forgot that I had been mad enough to attempt such a thing, but you can find here https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:tutorial:lifo-2014 the material of the seminar that I gave at Orl?ans University last October, which includes a example on a search on binary trees. Note that the intermediate lemmas cannot currently be proved, as WP generates an incomplete axiomatization of the inductive predicates. ** Disclaimer: what follows here is quite technical, you can skip it in a first reading** More precisely, WP does not take into account the fact that such predicates are least fixpoints, in the sense that to establish that P(x) is true, one of the cases in the inductive definition has to hold. Reportedly, generating such inversion axioms tends to confuse automated theorem provers, but the Coq output could be enhanced to take inductive predicates fully into account. Failing that, it is not possible to complete the proof (writing explicitely the missing axioms will be needed at some point). Best regards, -- E tutto per oggi, a la prossima volta Virgile