kouzdra (kouzdra) wrote,
kouzdra
kouzdra

This journal has been placed in memorial status. New entries cannot be posted to it.

Categories:

По поводу 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

  • "И все его оставили"

    Чего0то мне кажется, что на Украине жизнь скоро может начать иллюстрировать искусство: Когда случился тот неслыханный скандал, тот крик, и брань, и…

  • Технологии

    "... держать молоток либо какие-то новые технологии...", – считает Володин.

  • Попались обсуждения какого-то

    гопнического сериала про "слова пацанов", там в воспоминательных рассуждаловах всякие личные воспоминание про "с раёнов" - поражает театраьность и…

  • Post a new comment

    Error

    Comments allowed for friends only

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 28 comments

  • "И все его оставили"

    Чего0то мне кажется, что на Украине жизнь скоро может начать иллюстрировать искусство: Когда случился тот неслыханный скандал, тот крик, и брань, и…

  • Технологии

    "... держать молоток либо какие-то новые технологии...", – считает Володин.

  • Попались обсуждения какого-то

    гопнического сериала про "слова пацанов", там в воспоминательных рассуждаловах всякие личные воспоминание про "с раёнов" - поражает театраьность и…