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;
}


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

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

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

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

Recent Posts from This Journal

  • "Трагедия курьера"

    Что забавно - попытки партии и ментов усиливать контроль за всем на практике дают противоположный результат - паспорта у меня в данный момент нет,…

  • Из комментов

    Впрочем у истории с чёрными кораблями были две забавные концовки — одна в Порт-Артуре, другая — в Жемчужной гавани

  • Во всяком культивировании

    всяких покрытых богоматерей, дней оун-упа и прочих мининых-невских-пожарских и тп меня раздражают не поводы (на них мне действительно насрать) а…

  • 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.
  • 73 comments

Recent Posts from This Journal

  • "Трагедия курьера"

    Что забавно - попытки партии и ментов усиливать контроль за всем на практике дают противоположный результат - паспорта у меня в данный момент нет,…

  • Из комментов

    Впрочем у истории с чёрными кораблями были две забавные концовки — одна в Порт-Артуре, другая — в Жемчужной гавани

  • Во всяком культивировании

    всяких покрытых богоматерей, дней оун-упа и прочих мининых-невских-пожарских и тп меня раздражают не поводы (на них мне действительно насрать) а…