--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on April 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Is it possible to "save"/reuse proofs?



mån 2019-04-15 klockan 11:56 +0200 skrev Loïc Correnson:
> Hi Tomas,
> 
> I think you didn’t miss anything at all.
> There is not (yet) any cache mechanism in WP to reuse previous proofs
> from one session to the other.
> Although, we are working to implement such a feature, among many
> others !

Sounds promising :)

> In the short term, there are several workarounds you can try to
> improve the situation.
> From my point of view, a proof requiring 30s timeout is far too
> complex, so try either to:
> 
> 1. decompose the proof of the assertion by applying tactics into the
> TIP (Frama-C/Gui, WP proof panel)
> Sometimes, by a simple split or range tactic, you can decompose a
> very complex proof into smaller, simpler ones.

I did this in this case, performing just a single computation in each
statement and breaking up the assertions accordingly. This worked well
to speed things up

> 2. make intermediate assertions, and/or write ACSL lemmas. Once you
> are convinced into your lemmas, you can silent their proofs by
> turning them into axioms, or add `-wp-prop=- at lemmas` on your command
> line.

Yes, I've found the turn-lemmas-into-axioms approach useful. Or as I
like to call it: the "because I say so"-method

> 3. use ghost functions to implement the so-called techniques of
> lemma-functions to decompose the proof into smaller ones.

I read about ghost functions just the other day. I will have to give
them a try some time

Thanks for the tips, most useful

/Tomas