---
layout: fc_discuss_archives
title: Message 4 from Frama-C-discuss on July 2009
---
[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