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] WG: binary_search example

  • Subject: [Frama-c-discuss] WG: binary_search example
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
  • Date: Fri, 3 Jul 2009 20:11:59 +0200
  • References: <39F47C6991B94BF48D9977758F7143EB@AHARDPLACE> <42050C88D59E144CA358159FF0E6018B090554@TITAN.first.fraunhofer.de> <A03822123729484AAE337B69D8410649@AHARDPLACE> <42050C88D59E144CA358159FF0E6018B090555@TITAN.first.fraunhofer.de> <F4F4BC16C89C449D86958B3F987B2D0F@AHARDPLACE> <42050C88D59E144CA358159FF0E6018B090556@TITAN.first.fraunhofer.de> <2D3B91FDEC164A7F9FAF39C1542677F0@AHARDPLACE> <42050C88D59E144CA358159FF0E6018B090557@TITAN.first.fraunhofer.de> <7C72AD5B7615453F8AED3F70A370B855@AHARDPLACE>
Hello,

I am trying to prove the numerous binary_search examples you provided with 
your sources.

But I would like to know which example under what configuration was proven 
and if there is a necessary integer call like exact or bounded to get a full 
proof.

So far, I am unable to prove even the lemma you created along with the 
algorithm.

(Lithium, Vista, any Prover)

Sincerely

Christoph