Здесь происходит несколько разных вещей. Я буду обсуждать каждое из трех постусловий по очереди.

Первое и второе постусловия

Поскольку IsEven является рекурсивно определяемым предикатом, в общем случае факты о нем потребуют доказательств по индукции. Ваше первое пост-условие достаточно простое, чтобы не требовать индукции, поэтому оно выполняется.

Ваше второе постусловие требует доказательства индукции. У Дафни есть эвристика для автоматического выполнения индукции, но эта эвристика вызывается только в определенных контекстах. В частности, Дафни будет пытаться индуцировать только «призрачные методы» (также называемые «леммами»).

Если вы добавите ключевое слово ghost перед method в Check1 (или замените method на lemma, что эквивалентно), вы увидите, что второе постусловие проходит. Это связано с тем, что вызывается эвристика индукции Дафни, и ей удается завершить доказательство.

Третье постусловие

Третье постусловие более сложное, поскольку включает нелинейную арифметику. (Другими словами, это включает в себя нетривиальные рассуждения о перемножении двух переменных.) Решатель, лежащий в основе Дафни, не может рассуждать о таких вещах, поэтому эвристическое доказательство по индукции не проходит.

Доказательство того, что a * a четно, если a четно

Один из способов доказать это — здесь. Я выделил IsEven(a) ==> IsEven(a * a) в отдельную лемму, названную EvenSquare. Я также изменил его, чтобы требовать IsEven(a) в качестве предварительного условия, а не помещать импликацию в постусловие. (Аналогичное доказательство также проводится с импликацией вместо этого, но использование предварительных условий для подобных лемм вместо импликации является идиоматическим Дафни.)

Доказательство EvenSquare проводится индукцией (вручную) по a. Базовый вариант обрабатывается автоматически. В индуктивном случае (тело оператора if) я вызываю гипотезу индукции (т. е. я делаю рекурсивный вызов метода EvenSquare, чтобы установить, что (a - 2) * (a - 2) четно). Затем я утверждаю, что a * a можно записать как сумму (a - 2) * (a - 2) и некоторого смещения. Утверждение отправляется автоматически. Доказательство будет сделано, если я смогу показать, что правая часть этого равенства четна.

Для этого я уже знаю, что (a - 2) * (a - 2) четно, поэтому сначала прибегаю к другой лемме, чтобы показать, что смещение четно, потому что оно в два раза больше другого. Наконец, я прибегаю к последней лемме, чтобы показать, что сумма двух четных чисел четна.

Это завершает доказательство в предположении двух лемм.

Доказательства двух лемм

Остается показать, что дважды все четно и что сумма двух четных чисел четна. Хотя это и не совсем тривиально, но и не так сложно, как EvenSquare.

Лемма EvenDouble доказывает, что дважды все четно. (На самом деле это более сильная версия вашего второго постусловия. Ваше второе постусловие говорит, что удвоение любого четного числа является четным. Фактически, удвоение любого (неотрицательного, согласно вашему определению четности) числа в все четно.) Доказательство EvenDouble проводится (вручную) индукцией по a. Базовый вариант обрабатывается автоматически. Индуктивный случай требует только явного вызова гипотезы индукции.

Лемма EvenPlus почти автоматически доказывается эвристикой индукции Дафни, за исключением того, что она натыкается на ошибку или какую-то другую проблему, вызывающую зацикливание в решателе. После небольшой отладки я определил, что аннотация {:induction x} (или {:induction y}, если на то пошло) делает доказательство не зацикленным. Эти аннотации сообщают эвристике Дафни, какую переменную (переменные) следует попытаться индуцировать. По умолчанию в этом случае Дафни пытается индуцировать оба x и y, что по какой-то причине приводит к зацикливанию решателя. Но индукция по любой переменной работает. Я исследую эту проблему дальше, но текущее решение работает.