Треугольник

Скачайте файл triangle.

Напишите спецификацию функции triangle со следующим заголовком:

int triangle(int a, int b, int c);

Параметры a, b, c могут принимать только положительные значения. Функция должна возвращать следующее значение:

  • 3, если можно составить равносторонний треугольник со сторонами, равными соответственно a, b, c;
  • 2, если можно составить неравносторонний равнобедренный непрямоугольный треугольник со сторонами, равными соответственно a, b, c;
  • 6, если можно составить неравносторонний равнобедренный прямоугольный треугольник со сторонами, равными соответственно a, b, c;
  • 4, если можно составить неравносторонний неравнобедренный прямоугольный треугольник со сторонами, равными соответственно a, b, c;
  • 0, если можно составить неравносторонний неравнобедренный непрямоугольный треугольник со сторонами, равными соответственно a, b, c;
  • -1, если нельзя составить треугольник со сторонами, равными соответственно a, b, c.

При помощи инструментов Frama-C + Jessie проверьте, что написанная вами спецификация достаточна для доказательства полной корректности тестовых функций. Обратите внимание, что наличие доказательства корректности тестовых функций является необходимым, но недостаточным условием правильности спецификации.