Математическая модель требований

Математическую модель требований к верифицируемой программе мы будем называть спецификацией программы. Семантика спецификации состоит в формальном описании требований к поведению программы.

Требований к поведению программ может быть огромное множество, но в данном разделе мы будем рассматривать только требования к функциональности программ. Под требованиями к функциональности понимаются ограничения на результат вычисления программы в зависимости от значений ее входных данных.

Входной и выходной предикаты

Спецификацией \(\Phi\) программы над переменными \(\mbox{V}\) мы будем называть два предиката:

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

Задачи и упражнения

В двух первых задачах предполагается, что доменом всех входных и выходных переменных является множество целых чисел, а все используемые в качестве предикатов функции должны быть формально определены. Можно считать априорным, что уже формально определены следующие арифметические операции над целыми числами: сложение, вычитание, умножение — а также операции сравнения (равно, неравно, больше, меньше и т.п.).

  1. Опишите словами требования, описанные каждой из следующих спецификаций:
    • \(\varphi(x) =(x > 0); \psi(x,z) = (x \cdot x = z) \)
    • \(\varphi(x) =(x > 0); \psi(x,z) = (0 \leq z < x) \)
    • \(\varphi(x_1, x_2) =(x_1 > x_2 + 1); \psi(x_1, x_2, z) = (x_1 > z > x_2) \)
    • \(\varphi(x) =(x > 0); \psi(x,z) = (x < z < 0) \)
  2. Дайте формальную спецификацию каждого из следующих требований:
    • программа должна вычислять модуль данного ей числа;
    • программа для двух данных целых чисел должна вычислять максимальное из них;
    • программа должна для двух данных ей положительных целых чисел вычислять их сумму, а для двух данных ей отрицательных целых чисел — произведение;
    • программа должна для любого неотрицательного целого числа вычислять ближайшее снизу приближение к квадратному корню из него;
    • программа должна для любого положительного целого числа большего единицы вычислять его максимальный простой делитель;
    • программа должна для двух заданных положительных целых чисел вычислять количество простых чисел между ними.
  3. Обоснованно ответьте на следующий вопрос. Является ли для любых спецификаций вида \( (\alpha, \beta) \) над переменными \( (A, Y^{*}, B) \) и \( (\beta, \gamma) \) над переменными \( (B, Y^{**}, C) \) пара утверждений \( (\alpha, \gamma) \) спецификацией над переменными \( (A, Y^{***}, C) \) при некоторых \( Y^{*}, Y^{**}, Y^{***} \)? Зависит ли ответ от выбора указанных множеств переменных?