# include <stdio.h> /*@ requires n >= 0; @ ensures \result >= 1; */ int fact (int n) { if (n == 0) return 1; return n * fact (n-1); } int main (int argv, char * argc []) { printf ("Hello: %d\n", fact (50)); return 0; }
Кажется подавляющее большинство народу вообще не понимает в чем на самом деле состоит тут неправильность:
Она вовсе не в том, что тут "может быть переполнение и переполнения надо запретить" - она в том что в контракте функции заявлено что выдаваемый ей результат всегда больше нуля и верификатор это полагает выполненым.
И дальше при вызовах функции он будет полагаться на это.
По уму оно должно быть так:
module Fact use import int.Int let rec fact (n : int) : int = if n = 0 then 1 else n * fact (n-1) let test () = fact 5 end
При попытке это дело выполнить WhyML выдает следующее:
msk@debian:~/TEST$ why3 execute fact.mlw Fact.test File "fact.mlw", line 7, characters 29-39: warning: this expression may diverge, which is not stated in the specification File "fact.mlw", line 9, characters 14-20: warning: this expression may diverge, which is not stated in the specification Execution of Fact.test (): type: int result: 120 globals:
Предупреждения посвящены тому, что функция с его точки зрения может не завершиться.
Чтобы он это мог понять нужна подсказка:
let rec fact (n : int) : int variant { n } = if n = 0 then 1 else n * fact (n-1)
Конструкция variant задает значение "от параметров", которое должно гарантировано уменьшаться при каждом вызове функции. Если верификатор сумеет это доказать - он ругаться перестанет. Отступление о рекурсии на этом заканчивается.
Теперь собственно к исходному вопросу:
let rec fact (n : int) : int variant { n } requires { n >= 0 } ensures { result >= 1 } = if n = 0 then 1 else n * fact (n-1)
Компилируется - но в отличие от C в WhyML int действительно безразмерный:
Результат выполнения fact 50:
Execution of Fact.test (): type: int result: 30414093201713378043612608166064768844377641568960512000000000000 globals:
Так что верификатор тут вполне прав.
Это так сказать первая часть известного балета. Вторая будет в следущем посте.