Скачайте файл 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 проверьте, что написанная вами спецификация достаточна для доказательства полной корректности тестовых функций. Обратите внимание, что наличие доказательства корректности тестовых функций является необходимым, но недостаточным условием правильности спецификации.