Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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