Блог

Я верю, что могу генерировать доказательства, используя why3 с различными доказательствами,

1. frama-c -wp -wp-prover cvc4 -wp-rte -wp-out proof swap.c
2. frama-c -wp -wp-prover z3-ce -wp-rte -wp-out proof swap.c
3. frama-c -wp -wp-prover alt-ergo -wp-rte -wp-out proof swap.c

Это создает различные файлы «почему». Я хотел бы подтвердить обязательства по доказательству с помощью внешней программы. Похоже, что каждое обязательство по доказательству находится в другом формате; ШепелявитьКлоджур и ОКамл? Что именно это за формат? Правильно ли, что это доказательства и их достаточно, чтобы показать, что контракт/доказательство верны, не доказывая, что Z3, alt-ergo и т. Д. Верны?

своп.c

Для руководства по wp,

 int h = 42;
/*@
  requires valid(a) amp;amp; valid(b);
  assigns *a, *b;
  ensures *a == old(*b) amp;amp; *b == old(*a);
*/
void swap(int* a, int* b)
{
    int tmp = *a;
    *a = *b;
    *b = tmp;
}

int main()
{
    int a = 24;
    int b = 37;

    //@ assert h == 42;

    swap(amp;a, amp;b);

    //@ assert a == 37 amp;amp; b == 24;
    //@ assert h == 42;
    
    return 0;
}
 

Это прекрасно работает, и графический интерфейс frama-c показывает мне, как разрабатывать контракты и аннотации.

Альтер-эрго

 (* WP Task for Prover Alt-Ergo,2.4.1 *) (* this is the prelude for Alt-Ergo, version >= 2.4.0 *) (* this is a prelude for Alt-Ergo integer arithmetic *) (* this is a prelude for Alt-Ergo real arithmetic *) type string

logic match_bool : bool, 'a, 'a -> 'a

axiom match_bool_True :   (forall z:'a. forall z1:'a. (match_bool(true, z, z1) = z))
 

Полное доказательство усечено для краткости.

z3-ce

 (* WP Task for Prover Z3,4.8.11,counterexamples *) ;;; generated by SMT-LIB2 driver ;;; SMT-LIB2 driver: bit-vectors, common part ;;; generated by SMT-LIB strings ;;; generated by SMT-LIB strings (set-option :produce-models true) ;;; SMT-LIB2: integer arithmetic ;;; SMT-LIB2: real arithmetic (declare-sort uni 0)

(declare-sort ty 0)

(declare-fun sort (ty uni) Bool)

(declare-fun witness (ty) uni)
 

Полное доказательство усечено для краткости.

Я должен признать, что я не совсем уверен, что полностью понимаю, чего вы хотите достичь здесь, но вот ответы на ваши вопросы:

Похоже, что каждое обязательство по доказательству находится в другом формате; Lisp и OCaml? Что именно это за формат?

Эти файлы представляют формулы, которые выдаются проверяющим, которых вы просите запустить Frama-C. Формат зависит от проверяющего. Если я правильно помню, для многих проверяющих это будет smtlib или tptp, но некоторые проверяющие, такие как Alt-Ergo, также могут получать пользовательский вывод. Создание файла описано в файлах драйверов Why3, как упомянуто (довольно кратко) в разделе 12.4 руководства Why3.

Правильно ли, что это доказательства ?

Нет, это формулы, которые должны быть проверены проверяющим, для которого они были сгенерированы.

и достаточно ли, чтобы показать, что контракт/доказательство верны, не доказывая, что Z3, alt-ergo и т. Д. Верны?

Нет. Если в проверяющих, которые вы используете, есть ошибка, они могут ошибочно сообщить вам, что данное обязательство по доказательству является действительным. Некоторые проверяющие могут предоставить трассировку проверки (например, если вы настроите драйвер для использования get-proof команды smtlib), но, насколько я знаю, формат такой трассировки зависит от проверяющих, так что, вероятно, будет сложно проверить ее внешним инструментом.