Dafny: быстрое вычисление экспоненты (циклы)

Я пытаюсь реализовать и скомпилировать алгоритм Fast Exponential в Dafny, но столкнулся с парой проблем.

Контекст:

  • Весь код доступен ниже;
  • Сама лемма о быстрой экспоненте (FastExp) является итеративной;
  • Функция exp используется для проверки правильности вычислений (эта функция рекурсивно выполняет традиционную экспоненту);
  • Я не буду вдаваться в то, как выполняется математика, работает она или нет. Это не проблема, математика верна.

Теперь основные проблемы, с которыми я сталкиваюсь:

  1. Я не знаю, что добавить в уменьшение и инварианты цикла;
  2. Постусловия леммы FastExp могут не выполняться;

Я был бы рад, если бы кто-нибудь помог мне с этой простой (я предполагаю) проблемой.

Заранее спасибо.

function isEven(a: int): bool
    requires a >= 0;
{
    if a == 0 then      true 
    else if a == 1 then false 
    else                isEven(a - 2)
}

function exp(x: int, n: int): int
    requires n > 0;
{
    if n == 1 then
        x
     else 
        x * exp(x, n-1)
}

lemma FastExp(x: int, n: int) returns (r: int)
requires n >= 0
ensures r == exp(x,n)
{
    var expo:int := n;
    var c:int := x;
    var tempR:int := 1;

    while expo > 0
        invariant 0 <= expo
        decreases expo
    {
        if isEven(expo) {
            tempR := tempR * c;
        }
        c := c * c;
        expo := expo / 2;
    }
    r := tempR;
}

loops invariants loop-invariant dafny
person Asfourhundred    schedule 19.04.2021    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Предложение decreases используется для объяснения завершения. Чтобы доказать, что цикл завершается, вам нужно найти некоторое выражение, значение которого уменьшается (в обоснованном порядке) с каждой итерацией. В вашем случае expo является таким выражением, поэтому ваше предложение decreases - это все, что вам нужно, чтобы доказать завершение вашего цикла. (На самом деле, это больше, чем вам нужно. Если вы вообще опустите это предложение decreases, Дафни автоматически догадается об этом.)

Чтобы рассуждать о цикле, нужно найти некоторое условие, называемое инвариантом цикла, которое выполняется в самом начале каждой итерации (то есть условие, которое истинно каждый раз, когда защита от цикла срабатывает). оценивается). Вы написали один такой инвариант, а именно 0 <= expo. Однако не существует инварианта относительно переменных tempR и c или отношения между этими переменными и expo, x и n. Следовательно, верификатор ничего не знает о значениях этих переменных в начале итерации цикла или после цикла.

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

Позволь мне начать. Есть три вещи, которые должен сделать ваш инвариант. 0: Первоначально необходимо удерживать, когда петля впервые достигнута. То есть условие должно быть истинным для начальных значений переменных. 1: Инвариант и отрицание защиты от цикла (и только они, без каких-либо других фактов, которые, как вы можете подумать, также имеют место) должны быть достаточными для доказательства постусловия. Например, единственное, что вы можете сделать из вашего текущего инварианта цикла и отрицания защиты, это expo == 0 после цикла. 2: Инвариант должен поддерживаться телом цикла. То есть, учитывая инвариант и защиту в начале тела цикла, вы должны доказать, что инвариант снова сохраняется после тела цикла.

После того, как вы выясните, каким должен быть инвариант цикла, вам нужно будет доказать математический факт о возведении в степень. Ты увидишь, когда доберешься туда.

Удачи!

PS. Вот некоторые другие комментарии о ваших программах:

  • В настоящее время вы получаете нарушение предварительного условия при вызове exp в постусловии FastExp. Это означает, что ваше постусловие плохо определено и не всегда имеет смысл (что сделало бы задачу установления постусловия невозможной). Проблема в том, что FastExp позволяет n быть 0, а ваша функция exp - нет. Вам потребуется определить exp для показателя степени 0, чтобы доказать правильность FastExp. Итак, измените предварительное условие exp, чтобы n было 0. (Затем вам придется починить тело exp.)
  • У Дафни есть тип nat, обозначающий неотрицательные целые числа. Итак, если вы хотите, вместо объявления n: int и добавления предварительных условий 0 <= n вы можете просто объявить n: nat и отбросить эти предварительные условия.
  • Есть более короткий способ определить isEven, а именно a % 2 == 0.
  • Вам не нужно вводить локальную переменную tempR. Вы можете просто использовать r напрямую.
  • Немного странно объявлять FastExp как лемму. Дафни позволяет леммам иметь выходные параметры (что иногда очень полезно), и вы действительно можете написать доказательство леммы, используя цикл. Но причина написания FastExp не в том, чтобы показать, что есть какое-то значение, которое вы можете присвоить r, чтобы сделать r == exp(x, n) истинным — вы могли бы сделать это с помощью присвоения r := exp(x, n);. Вместо этого причина объявления FastExp заключается в том, что вам нужна программа, которая его вычисляет. Для этого объявите FastExp как method. (Единственное техническое различие между леммой и методом в Дафни заключается в том, что метод компилируется, а лемма стирается компилятором.)
person Rustan Leino    schedule 21.04.2021