June 19th, 2017

Dr.Strangelove

Поигрался с 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;
}


С точки зренияя верификатора вполне корректно.

Хотя в действительности если случится переполнение - результат вполне может оказаться отрицательным.

Причем это небезобидное свойство - потому что потом это реально вполне возможно отрицательное значение будет проходить как безусловно положительное во всех местах использования.

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