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] Incremental verification

  • Subject: [Frama-c-discuss] Incremental verification
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Mon, 04 Oct 2010 14:13:06 +0200
Hi,

this is a proposal for a feature: When writing and verifying code, you
typically do the following:

  repeat 
    change some lines in your code or specification
    run Jessie 
  until verified

I'd like to considerably reduce the time needed for Jessie in this loop.
The Visual Studio plugin for Spec# has a feature that lets the verifier
run each time the content of the buffer has been changed. This gives
immediate feedback and greatly improves productivity because you can
very quickly narrow down the reason why the code doesn't verify. Is a
similar feature possible for Frama-C/Jessie? For example, Frama-C may
watch the source file. Each time a change is detected, Jessie is run
again, but only for the parts that changed. Thus, contracts for
unaltered functions that had previously been verified don't have to be
verified again, which will save a lot of time. Caching of proofs and
failed proofs may also speed up Jessie.
-- 
Regards,
Boris