kouzdra (kouzdra) wrote,
kouzdra
kouzdra

По поводу frama-c

# 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: 


Так что верификатор тут вполне прав.

Это так сказать первая часть известного балета. Вторая будет в следущем посте.
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 28 comments