Какие l oop инварианты использовать для целочисленного логарифма? - PullRequest
Новая
       79

Какие l oop инварианты использовать для целочисленного логарифма?

3 голосов
/ 11 февраля 2020

Поскольку у меня есть первые шаги в C формальной проверке с Frama- C, я пытаюсь формально проверить целочисленную двоичную функцию логарифма, записанную следующим образом: 

//@ logic integer pow2(integer n) = (n == 0)? 1 : 2 * pow2(n - 1);

/*@
    requires n > 0;
    assigns \nothing;
    ensures pow2(\result) <= \old(n) < pow2(\result + 1);
 */
unsigned int log2(size_t n)
{
    unsigned int res = 0;
    while (n > 1) {
        n /= 2;
        ++res;
    }
    return res;
}

Я использую Frama- C 20.0 (Calcium), с командой frama-c-gui -rte -wp file.c (у меня почему-то нет плагина Jess ie). Я проверил пост-условие для удержания до n = 100 000 000 (с использованием утверждений стандартной библиотеки), но эта функция не проходит проверку формально, несмотря на все мои усилия, и в учебниках Frama- C обычно используются тривиальные варианты l oop это уменьшение (а не деление пополам) каждой итерации, поэтому не так близко к тому, что я пытаюсь сделать.

Я пробовал следующие аннотации кода, некоторые из которых, вероятно, не нужны: 

//@ logic integer pow2(integer n) = (n == 0)? 1 : 2 * pow2(n - 1);

/*@
    requires n > 0;
    assigns \nothing;
    ensures pow2(\result) <= \old(n) < pow2(\result + 1);
 */
unsigned int log2(size_t n)
{
    unsigned int res = 0;
    /*@
        loop invariant 0 < n <= \at(n, Pre);
        loop invariant \at(n, Pre) < n * pow2(res + 1);
        loop invariant pow2(res) <= \at(n, Pre);
        loop invariant res > 0 ==> 2 * n <= \at(n, Pre);
        loop invariant n > 1 ==> pow2(res + 1) <= \at(n, Pre);
        loop invariant res <= pow2(res);
        loop assigns n, res;
        loop variant n;
     */
    while (n > 1) {
    L:
        n /= 2;
        //@ assert 2 * n <= \at(n, L);
        ++res;
        //@ assert res == \at(res, L) + 1;
    }
    //@ assert n == 1;
    return res;
}

Аннотации, которые не могут быть проверены, являются l oop инвариантами 2 и 5 (оба Alt-Er go 2.3.0 и Z3 4.8.7 timeout). Что касается инварианта 2, сложность, по-видимому, связана с целочисленным делением, но я не уверен, что добавить, чтобы WP мог это доказать. Что касается инварианта 5, WP может доказать, что он установлен, но не сохранен. Для этого может потребоваться свойство, способное захватывать то, что происходит, когда n становится 1, но я не уверен, что может сработать.

Как я могу указать недостающую информацию для проверки этих инвариантов l oop, и есть ли другой Frama- C анализ, который позволил бы мне легче найти l oop инвариантов?

Спасибо за внимание.

1 Ответ

1 голос
/ 12 февраля 2020

Как общее замечание, часто хорошей идеей будет называть ваши аннотации, особенно когда вы начинаете иметь несколько инвариантов l oop для одного l oop. Это позволит вам быстрее выявлять неисправности (см. Пример ниже, хотя вы можете не соглашаться с выбранными мной именами).

Теперь вернемся к вашим проблемам: главное в том, что ваш инвариант 2 слишком слабый Если n в текущем l oop нечетно, вы не можете установить sh, что неравенство выполняется на следующем шаге. С более жесткой границей, а именно \at(n,Pre) < (n+1) * pow2(res), гипотеза в начале текущего шага достаточно сильна, чтобы доказать, что инвариант выполняется в конце шага, при условии, что мы знаем, что res не будет переполнено (в противном случае 1+res в конечном итоге станет 0, и неравенство больше не будет сохраняться).

Для этого я использовал промежуточную функцию-призрак, чтобы доказать, что n < pow2(n) для любого unsigned, что позволяет мне, благодаря инварианту pow2_lower ниже, чтобы гарантировать, что res_bound сохраняется на любом шаге l oop.

Наконец, небольшое замечание по pow2: здесь это не имеет значения, так как аргументы являются unsigned, следовательно, неотрицательны, но в общем случае аргумент integer может быть отрицательным, поэтому вы можете захотеть сделать определение более надежным, возвращая 1 всякий раз, когда n<=0.

В целом, следующая программа полностью доказана с Frama- C 20 и Alt-Er go (frama-c -wp -wp-rte file.c). Есть еще два утверждения, которые, по-видимому, необходимы, чтобы направлять Alt-Er go в поиске доказательства. 

#include "stddef.h"

/*@ logic integer pow2(integer n) = n<=0?1:2*pow2(n-1); */

/*@ ghost
/@ assigns \nothing;
   ensures n < pow2(n);
@/
void lemma_pow2_bound(unsigned n) {
  if (n == 0) return;
  lemma_pow2_bound(n-1);
  return;
}
*/

/*@
    requires n > 0;
    assigns \nothing;
    ensures pow2(\result) <= \old(n) < pow2(\result + 1);
 */
unsigned int log2(size_t n)
{
    unsigned int res = 0;
    /*@
        loop invariant n_bound: 0 < n <= \at(n, Pre);
        loop invariant pow2_upper: \at(n, Pre) < (n+1) * pow2(res);
        loop invariant pow2_lower: n*pow2(res) <= \at(n, Pre);
        loop invariant res_bound: 0 <= res < \at(n,Pre);
        loop assigns n, res;
        loop variant n;
     */
    while (n > 1) {
    L:
        /*@ assert n % 2 == 0 || n % 2 == 1; */
        n /= 2;
        /*@ assert 2*n <= \at(n,L); */
        res++;
        /*@ ghost lemma_pow2_bound(res); */
    }
    //@ assert n == 1;
    return res;
}
...