Введение в формальную верификацию SPARK ── от контрактов Ada к математическому доказательству

1. Введение ── дальше, чем «запустить и проверить»

Самый распространённый способ обеспечить качество ПО — тестирование.

тест: подтверждает, что программа корректно работает на выбранных входах

Но у тестирования есть предел. Комбинаций входов бесконечно много, и одним тестированием «корректно на всех входах» не показать.

Здесь появляется формальная верификация (Formal Verification).

формальная верификация: математически доказывает, что свойство выполняется для всех входов

В предыдущей статье «Привлекательность языка Ada» был общий обзор Ada, SPARK там затронут кратко.

Эта статья сосредоточена на практике формальной верификации SPARK и собирает следующее.

что такое SPARK и как он связан с Ada
как писать контракты (Pre/Post)
как доказывать их GNATprove
как проектировать инварианты цикла
как управлять побочными эффектами контрактами потока данных (Global/Depends)
стратегию поэтапного применения уровней доказательства (Stone–Platinum)
как встраивать SPARK в реальный проект

Цель — прожить переход от теста к доказательству на примерах кода.

Для кого эта статья и какие нужны знания

Рассчитываем на таких читателей.

• Кто хотя бы раз видел базовый синтаксис Ada (пакеты, режимы параметров in / out / in out, типы и подтипы)
• Кто интересуется контрактным программированием и статическим анализом и ищет «следующий шаг после тестов»
• Кто в высоконадёжном, встраиваемом или управляющем ПО выбирает средства обеспечения качества

Читать можно и без опыта Ada, но два предварительных пункта стоит закрыть. В примерах этой статьи постоянно встречаются разделение спецификации и тела пакета через package ... is и package body ... is и режимы параметров вроде procedure P (X : in out Integer). Если эти две вещи незнакомы, сначала закройте базу Ada в «Привлекательность языка Ada» и вернитесь: тогда можно сосредоточиться на контрактах.

И наоборот: этих двух вещей достаточно, чтобы читать дальше. Обозначения SPARK (SPARK_Mode, Pre, Post, Loop_Invariant, Global, Depends) объясняются в этой статье. Теория доказателей и логика не нужны. Читать сообщения GNATprove и править код или контракт — на практике нужно именно это.

Фрагменты кода из статьи выложены на GitHub как справочный набор, разложенный по файлам согласно главам.

ada-spark-formal-verification - komurasoft-blog-samples (GitHub)

На схеме сплошная линия обозначает отношение, которое выполняется всегда, а пунктирная — условное отношение (условия указаны в пояснении к каждому отношению на странице сведений). Полный список отношений (всего 17, с доказательствами и степенью уверенности) и определения основных понятий собраны на странице сведений карты знаний (на японском). Данные: JSON-LD / Turtle

2. Что такое SPARK ── подмножество Ada и вход в мир доказательств

SPARK — подмножество (частичный язык) Ada.

То, что это подмножество, — осознанный замысел.

полный Ada → выразительность высока, но формально верифицировать всё нереалистично
SPARK       → оставляют только верифицируемые возможности, чтобы доказательство стало реалистичным

Основные ограничения SPARK такие.

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

Слово «ограничение» может звучать тесно. Но эти ограничения получены в обмен на доказуемость.

Ядро инструментария SPARK — GNATprove от AdaCore.

как работает GNATprove:
1. разбирает код Ada, написанный на SPARK
2. переводит контракты (Pre/Post) и утверждения в промежуточный язык Why3
3. пытается доказать их автоматическими доказателями Z3, cvc5, Alt-Ergo и другими
4. сообщает результат сообщениями на исходном коде

Схемой это выглядит так.

flowchart LR
    Src["Код Ada, написанный на SPARK<br/>Pre / Post / Assert"] --> GP[GNATprove]
    GP --> VC[Генерация условий верификации]
    VC --> Why3["Why3<br/>промежуточный язык и платформа доказательств"]
    Why3 --> P1[cvc5]
    Why3 --> P2[Z3]
    Why3 --> P3[Alt-Ergo]
    P1 --> Res[Сведение результатов]
    P2 --> Res
    P3 --> Res
    Res --> Msg["Сообщения с позицией в исходном коде<br/>info / medium / high"]

Разработчик напрямую трогает только края: код слева и сообщения справа. Why3 и доказатели в середине работают сами, обычно о них не думают. Думать начинают, когда доказательство не проходит и нужно сменить доказатель или дать ему больше времени.

Имена, которые появились в этой главе

Здесь фиксируем имена, которые встречаются впервые. Дальше они идут без пояснений.

Важно, что SPARK построен поверх Ada.

код SPARK = код Ada + контрактные аннотации

То есть SPARK лежит на продолжении обычной разработки на Ada. Отдельный синтаксис учить заново не нужно.

3. Установка GNATprove и первое доказательство

Сначала соберём среду, в которой запускается GNATprove.

Поставить Alire

GNATprove входит в тулчейн GNAT. Самый простой способ получить этот тулчейн — Alire. Это менеджер пакетов на исходниках для Ada / SPARK, команда — alr. Дистрибутив берут со страницы релизов репозитория Alire на GitHub.

После установки выбирают компилятор по умолчанию.

alr toolchain --select

Запускается помощник выбора: из списка доступных GNAT выбирают компилятор по умолчанию. alr toolchain без аргументов показывает уже установленные компиляторы и текущий по умолчанию.

Записать версию

Когда среда готова, версию стоит сохранить. Результат доказательства зависит от версии доказателя. Если позже «тот же код перестал доказываться», это первое, что проверяют.

alr version
gnatprove --version

Создать проект

Через Alire проект со SPARK создают такой командой.

alr init --bin spark_demo
cd spark_demo

GNATprove входит в компилятор GNAT, поэтому если проект собирается через alr build, команда gnatprove уже доступна.

Как первую цель доказательства напишем функцию абсолютного значения.

package Simple_Proof with SPARK_Mode is

   function Abs_Value (X : Integer) return Integer
     with Post => Abs_Value'Result >= 0;

end Simple_Proof;

package body Simple_Proof with SPARK_Mode is

   function Abs_Value (X : Integer) return Integer is
   begin
      if X < 0 then
         return -X;
      else
         return X;
      end if;
   end Abs_Value;

end Simple_Proof;

На что смотреть.

with SPARK_Mode ставят и на спецификацию пакета, и на тело
условие Post объявляет свойство «результат не меньше 0»
атрибут 'Result ссылается на возвращаемое значение функции

Запустим GNATprove на этом коде.

gnatprove -P spark_demo.gpr

Результат выглядит так.

SUMMARY
-------
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
simple_proof.adb:5:15: info: range check proved
simple_proof.adb:6:16: info: range check proved
simple_proof.ads:3:19: info: postcondition proved

Сообщение postcondition proved. Это значит: для всех входов типа Integer доказано, что возвращаемое значение не меньше 0.

Этот опыт — вход в SPARK.

Вывод, когда доказать не удалось

Смотреть только на успешный вывод мало: на практике нужно уметь читать неудачу. GNATprove сообщает о недоказанных проверках с позицией в исходном коде. Базовая форма — одна строка.

file.adb:12:37: medium: divide by zero might fail

Это строка 12, столбец 37 файла file.adb, то есть позиция знака деления /: «не удалось доказать, что делитель не равен 0». Важно: это might fail (может завершиться неудачей), а не will fail (завершится неудачей). Реального бага может и не быть. Чаще всего информации не хватило, и доказатель не смог решить.

Если получен контрпример, отчёт подробнее.

high: assertion might fail
--> counterex.adb:11:25
 11 |    pragma Assert (R < 42);
    |                  ^~~~~~
  + e.g. when R = 42
  + provers gave up before completing the proof

e.g. when R = 42 — контрпример: конкретно говорит, что «не выполняется, когда R равен 42». Если GNATprove предполагает, что дело в нехватке контракта, иногда прилагает правку.

possible fix: subprogram at line xxx should mention Var in a precondition
possible fix: loop at line xxx should mention Var in a loop invariant
possible fix: call at line xxx should mention Var in a postcondition

К таким сообщениям быстрее всего привыкаешь, если вызывать их нарочно. Например, если в Abs_Value выше сменить Post на Abs_Value'Result > 0 (строго больше 0), случай X = 0 не докажется и появится postcondition might fail. Если у Increment из главы 5 снять Pre, появится overflow check might fail. Чередовать успешные и неуспешные примеры — самый короткий путь привыкнуть к GNATprove.

Серьёзность сообщений (info / medium / high) и список видов проверок собраны в главе 12.

4. Основы контрактного проектирования ── как писать Pre и Post

Доказательства SPARK начинаются с контрактов.

Контракты — возможность языка Ada 2012, но в SPARK они становятся входом доказательства.

procedure Transfer (From, To : in out Account; Amount : Positive)
  with Pre  => From.Balance >= Amount,
       Post => From.Balance = From.Balance'Old - Amount
                and then
                To.Balance = To.Balance'Old + Amount;

Ориентиры для Pre и Post такие.

Pre (предусловие):
  ответственность вызывающей стороны
  «если вызвать, выполнив это условие, Post гарантирован»
  достаточно слабое (в пределах того, что вызывающая сторона может выполнить) и при этом настолько сильное, насколько нужно

Post (постусловие):
  ответственность реализации
  «после вызова мир находится в таком состоянии»
  атрибут 'Old ссылается на значение до вызова
  слишком сильное стесняет реализацию, слишком слабое не даёт доказать полезные свойства

Типичные ошибки и что с ними делать.

ошибка 1: Pre слишком сильный
  Pre => X > 0 and X < 100 and X /= 50 and ...
  → проверить, может ли вызывающая сторона всегда выполнить это условие
  → не сужать Pre только потому, что тесты проходят

ошибка 2: Post слишком слабый
  Post => True
  → ничего не гарантирует. Доказательство теряет смысл

ошибка 3: побочный эффект забыли записать в Post
  Post => Result = X * 2  (пропущено обновление глобальной переменной)
  → побочные эффекты делают явными контрактами Global/Depends (глава 8)

5. Доказательство отсутствия переполнения ── гарантия численной безопасности

Одно из самых полезных на практике доказательств SPARK — предотвращение переполнения.

Посмотрим на этот код.

procedure Increment (X : in out Integer)
  with SPARK_Mode,
       Pre  => X < Integer'Last,
       Post => X = X'Old + 1;

Ключ — Pre => X < Integer'Last. С этим контрактом GNATprove может доказать, что сложение не переполнится.

Без контракта GNATprove предупреждает о возможном переполнении.

medium: overflow check might fail

То же верно и для более сложных вычислений.

function Average (A, B : Integer) return Integer
  with SPARK_Mode,
       Pre  => (if A >= 0 and B >= 0 then A <= Integer'Last - B
                elsif A < 0 and B < 0 then A >= Integer'First - B),
       Post => (if A <= B then A <= Average'Result and Average'Result <= B
                else B <= Average'Result and Average'Result <= A);

Pre выглядит сложно, но это условие «сумма A и B не переполняется», разложенное по знакам.

суть:
  суть доказательства отсутствия переполнения — объявить в Pre до сложения/умножения,
  что «результат укладывается в диапазон типа»
  выглядит хлопотно, но написав один раз, с ошибками переполнения больше не живут

6. Инварианты цикла ── доказываем свойства циклов

Одна из самых трудных частей формальной верификации — доказательство циклов.

Цикл выполняется произвольное число раз, поэтому тестом все варианты не покрыть. В SPARK для этого используют инвариант цикла (Loop Invariant).

function Sum_Of_Naturals (N : Natural) return Natural
  with SPARK_Mode,
       Post => Sum_Of_Naturals'Result = (N * (N + 1)) / 2;

function Sum_Of_Naturals (N : Natural) return Natural is
   Result : Natural := 0;
begin
   for I in 1 .. N loop
      Result := Result + I;
      pragma Loop_Invariant (Result = (I * (I + 1)) / 2);
   end loop;
   return Result;
end Sum_Of_Naturals;

Чтобы спроектировать инвариант цикла, нужен такой ход мысли.

1. записать свойство, которое выполняется в начале каждой итерации
2. выбрать такое, из которого после последней итерации выводится нужный Post
3. инвариант выражает формулой результат вычисления к этому моменту

Ещё один пример — поиск в массиве.

function Find (Arr : Array_Of_Integer; Target : Integer) return Natural
  with SPARK_Mode,
       Post => (if Find'Result = 0 then
                  (for all K in Arr'Range => Arr (K) /= Target)
                else
                  Arr (Find'Result) = Target);

function Find (Arr : Array_Of_Integer; Target : Integer) return Natural is
begin
   for I in Arr'Range loop
      if Arr (I) = Target then
         return I;
      end if;
      pragma Loop_Invariant
        (for all K in Arr'First .. I => Arr (K) /= Target);
   end loop;
   return 0;
end Find;

Инвариант здесь: «в уже просмотренном диапазоне Target нет».

принципы проектирования инвариантов цикла:
  формулой выразить «что можно утверждать после n итераций»
  в циклах по массиву частая форма — «для уже обработанного диапазона выполняется …»
  слишком сильный инвариант не доказывается, слишком слабый не выводит Post
  этот баланс — как раз то место, где видно умение доказывать циклы

7. Прагмы утверждений ── частичные свойства внутри кода

Помимо контрактов (Pre/Post), в SPARK в середине кода можно писать утверждения (Assert).

procedure Divide (A, B : Integer; Q, R : out Integer)
  with SPARK_Mode,
       Pre  => B /= 0,
       Post => A = Q * B + R and R >= 0 and R < abs (B);

procedure Divide (A, B : Integer; Q, R : out Integer) is
begin
   Q := A / B;
   R := A rem B;

   pragma Assert (A = Q * B + R);
   pragma Assert (R >= 0);
   pragma Assert (R < abs (B));
end Divide;

Как развести прагмы.

Pre/Post:       обещания на входе и выходе подпрограммы
Assert:         свойство, которое должно выполняться в конкретной точке кода
Loop_Invariant: свойство, которое сохраняется на каждой итерации цикла
Loop_Variant:   убывающая величина, которой показывают, что цикл обязательно завершится

Где Assert полезен.

проверка промежуточного результата сложного вычисления
проверка состояния после ветвления if/else
проверка свойств возвращаемого значения после вызова процедуры
подача леммы для последующего доказательства

8. Контракты потока данных ── Global и Depends

Одна из сильных сторон SPARK — контракты потока данных.

Они явно объявляют, какие глобальные переменные подпрограмма читает и пишет.

package Counter_Unit with SPARK_Mode is

   Count : Natural := 0;

   procedure Increment
     with Global => (In_Out => Count);

   procedure Reset
     with Global => (Output => Count);

   function Get_Value return Natural
     with Global => (Input => Count);

end Counter_Unit;

Режимы контракта Global — три.

Input:  только чтение (для функций)
Output: только запись (для инициализации)
In_Out: чтение и запись (для обновления)

Зависимости между переменными можно выразить через Depends.

procedure Transfer
  (From, To : in out Account)
  with Global => (Input => Exchange_Rate),
       Depends => (From =>+ (From, Exchange_Rate),
                   To   =>+ (To, Exchange_Rate));

=>+ значит «зависит от прежнего значения плюс эти входы».

зачем контракты потока данных:
  1. «к чему прикасается эта функция» видно сразу
  2. непреднамеренные побочные эффекты ловят при компиляции
  3. они входят во вход анализа информационного потока переменных
  4. помогают увидеть поток данных в крупной системе

9. Уровни доказательства ── поэтапное применение от Stone до Platinum

В SPARK есть понятие уровня доказательства (Proof Level).

Пытаться сразу полностью доказать весь код часто кончается срывом. Поэтому SPARK даёт стратегию постепенно поднимать строгость.

Stone:
  подтверждение, что код допустим как подмножество SPARK
  используют как промежуточный этап внедрения

Bronze:
  Stone + нет чтения неинициализированных переменных,
  поток данных такой, как задумано
  применяют как можно шире

Silver:
  Bronze + доказательство, что ошибок времени выполнения
  (выход за диапазон, переполнение, деление на ноль) не будет
  (AoRTE: Absence of Run-time Errors)
  стандартная цель для критичного ПО

Gold:
  Silver + важные свойства integrity
  (свойства, ключевые для безопасности функционирования и информационной безопасности)
  применяют только к той части кода, где такие свойства есть

Platinum:
  доказательство полной функциональной корректности относительно требований
  только к частям с самым высоким уровнем требований
  стоимость высока, примеров применения немного

Что называют «уровнем» ── --mode и --level — разные вещи

Здесь легко перепутать. Stone–Platinum — это уровни гарантии ПО, а опция --level у gnatprove — другое понятие. Первым соответствует --mode.

Silver, Gold и Platinum запускаются одним и тем же переключателем. Разница не в том, как крутят инструмент, а в том, что и до какого предела считают объектом проверки — в постановке цели.

А --level=0 … --level=4 — пресеты, которые задают, сколько усилий тратить на доказательство. Чем выше значение, тем больше времени, но выше сила доказательства. Внутри это комбинация отдельных ключей.

То есть --mode — «что проверять», --level — «насколько настойчиво». Сначала держат в голове --mode; --level — регулятор, который поднимают, когда доказательство не проходит.

Ещё одна практическая оговорка. --level ограничен временем, поэтому результат зависит от машины и нагрузки и не воспроизводится. В CI и когда результат делят несколько человек, официально рекомендуют --steps (предел в шагах вывода, а не во времени) или --replay (повтор уже полученного доказательства).

Источник: SPARK User’s Guide (8.1 Levels of Software Assurance и Appendix A Command Line Invocation)

Практическая стратегия внедрения такая.

этап 1: провести весь проект через уровень Stone
  → найти ошибки в написании контрактов

этап 2: важные модули довести до уровня Silver
  → убрать переполнения и выходы за границы
  → большую часть практических ошибок ловят уже здесь

этап 3: ядро логики довести до уровня Gold
  → математически гарантировать свойства, ключевые для безопасности функционирования и информационной безопасности
  → не весь код, а ту часть, где эти свойства есть

этап 4: только части с самым высоким требованием — на Platinum
  → доказать полную функциональную корректность относительно требований
  → стоимость высока, поэтому охват минимальный

10. Практический ход доказательства ── рабочий процесс с меньшим числом возвратов

Рабочий процесс повседневного использования GNATprove.

1. Спроектировать типы и спецификацию
   задать ограничения диапазона и инварианты типа

2. Написать контракты (Pre/Post)
   выразить спецификацию контрактом до реализации

3. Добиться компиляции
   снять ошибки компиляции через GNAT

4. Запустить GNATprove на уровне Stone
   gnatprove -P proj.gpr --mode=stone

5. Посмотреть предупреждения и при необходимости поправить контракты
   особенно следить за пропущенной инициализацией
   если нужны только инициализация и поток данных — Bronze
   gnatprove -P proj.gpr --mode=bronze

6. Целиться в уровень Silver
   gnatprove -P proj.gpr --mode=silver
   убрать ошибки времени выполнения

7. Если есть циклы — добавить инварианты
   если не доказывается, проверить, не не хватает ли инварианта

8. На уровне Gold доказать важные свойства
   gnatprove -P proj.gpr --mode=gold
   переключатель запуска тот же, что у Silver; меняется цель проверки
   --level поднимают, только когда доказательство не укладывается во время
   пример: gnatprove -P proj.gpr --mode=gold --level=3

Частые случаи «доказать не удаётся» и что делать.

случай 1: «medium: postcondition might fail»
  → Post слишком сильный или Pre слишком слабый
  → либо не хватает инварианта цикла

случай 2: «medium: overflow check might fail»
  → ограничить диапазон значений в Pre
  → или сузить диапазон самого типа

случай 3: «medium: array index check might fail»
  → инвариантом показать, что диапазон цикла лежит внутри диапазона массива
  → использовать for I in Arr'Range (SPARK лучше распознаёт диапазон)

случай 4: «prover timeout»
  → у доказателя кончилось время. Дробить доказательство инвариантами поэтапно
  → резать функцию на более мелкие

11. SPARK вместе с тестами ── понять, что они дополняют друг друга

Формальная верификация и тестирование — не противники, они дополняют друг друга.

доказательство SPARK:
  свойство выполняется для всех входов
  объект — только свойства, записанные в контракте
  то, что доказать нельзя, отдают ручной проверке или тестам

тест:
  проверяет фактическое поведение на выбранных входах
  может найти неявные допущения, которых нет в контракте
  может проверить взаимодействие со средой выполнения

Схема совместного использования.

1. SPARK гарантирует уровень Silver (нет ошибок времени выполнения)
2. модульные тесты подтверждают конкретную правильность ввода-вывода
3. уровень Gold доказывает ядро логики
4. тесты сосредотачивают на частях, которые доказать не удалось

В Ada есть фреймворк модульного тестирования AUnit. Практичное сочетание: SPARK закрепляет типы и контракты, AUnit тестирует поведение.

12. Как читать результаты GNATprove ── смысл сообщений

У вывода GNATprove три уровня.

info:    доказательство успешно
medium:  доказать не удалось (предупреждение). Нужна ручная проверка
high:    доказательство не удалось (ошибка). Высока вероятность нарушения контракта

Частые сообщения и их смысл.

«postcondition proved»          условие Post доказано
«range check proved»            проверка диапазона доказана
«overflow check proved»         доказано отсутствие переполнения
«index check proved»            доказан диапазон индекса массива
«divide by zero check proved»   доказано отсутствие деления на ноль

«might fail»                    доказать не удалось
«cannot prove»                  доказатель не смог завершить доказательство
«prover timeout»                доказательство не завершилось за отведённое время

Порядок действий при might fail.

1. прочитать код и решить, может ли он действительно завершиться неудачей
2. если может — править код
3. если не должен — усилить контракт (Pre / инвариант)
4. если всё равно не доказывается — объявить допущением через pragma Assume
   (Assume — недоказанное допущение, пользоваться осторожно)

13. Как встраивать в реальный проект

Реалистичный подход к внедрению SPARK в существующий проект.

1. Начинать с нового кода
   не пытаться разом перевести на SPARK весь существующий код
   включать SPARK_Mode в модулях, которые пишут заново

2. Целиться в Silver
   Gold (доказательство важных свойств целостности) и Platinum (полное функциональное доказательство)
   — идеал, но начинают с Silver (нет ошибок времени выполнения)
   даже одно предотвращение переполнений даёт очень большую практическую пользу

3. Писать контракты от интерфейса
   контракты — в спецификации пакета (.ads) раньше реализации
   если спецификация зафиксирована, любой реализующий сможет написать код, который её выполняет

4. Встроить в CI/CD
   добавить gnatprove в конвейер CI
   при неудаче доказательства останавливать сборку (или хотя бы предупреждать)

5. Копить отчёты о доказательствах
   генерировать отчёт gnatprove --report=all
   следить за динамикой недоказанных пунктов

В проектах, где смешан существующий код C/C++, работает поэтапный подход.

1. новые модули писать на Ada/SPARK
2. с C/C++ стыковаться через Interfaces.C
3. важные структуры данных и логику проверки переносить в SPARK
4. постепенно расширять охват SPARK

14. Пределы SPARK и оговорки

SPARK тоже не всесилен. Честно понимать пределы — условие правильного применения.

что можно доказать:
  SPARK доказывает только «свойства, записанные в контракте»
  пропуски контракта (свойства, о которых забыли написать) не доказываются
  пример: Post доказывает, что результат отсортирован, но если забыть
  «неразрушаемость», сохранение исходных элементов не гарантируется

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

ограничения языка:
  код с интенсивным использованием указателей на SPARK не перевести
  доказательство динамического выделения памяти ограничено
  доказательство рекурсивных структур данных трудно

навык разработчика:
  написание контрактов требует тренировки
  проектирование инвариантов цикла осваивается особенно долго
  без плана повышения квалификации всей команды не обойтись

15. Итог ── доказательство в повседневной разработке

Мы разобрали практику формальной верификации SPARK.

SPARK — подмножество Ada, суженное до доказуемых возможностей
контракты (Pre/Post) — вход доказательства; контракты Ada 2012 используют как есть
GNATprove выполняет автоматическое доказательство и сообщает результат на уровне исходного кода
инварианты цикла доказывают свойства циклов
Global/Depends делают поток данных явным и управляют побочными эффектами
уровни доказательства (Stone–Platinum) позволяют постепенно поднимать строгость
практичная первая цель — уровень Silver (нет ошибок времени выполнения)
тест и доказательство не противники, они дополняют друг друга

Может быть предубеждение: «формальная верификация сложна и годится только для особых проектов».

Но сегодняшняя связка SPARK и GNATprove уже на таком уровне.

1. написать контракт — по сути та же проектная работа, что писать типы или тесты
2. запустить gnatprove — ощущение как у компиляции
3. посмотреть результат и поправить код или контракт

Этот цикл ничем не отличается от повседневной разработки, когда код правят по сообщениям компилятора.

Разница в том, что компилятор гарантирует «синтаксис корректен», а GNATprove — «корректно на всех входах».

Формула Ada из предыдущей статьи — «ошибки не ищут, типы и контракты делают так, чтобы их нельзя было написать», — со SPARK выходит на следующий шаг.

Отсутствие ошибок гарантируют доказательством.

Начните с небольшой функции: поставьте SPARK_Mode и Post, запустите gnatprove.

Когда увидите зелёное сообщение postcondition proved, взгляд на обеспечение качества ПО, скорее всего, сдвинется.

Справочные материалы

• Справочный набор фрагментов кода этой статьи, разложенный по главам - komurasoft-blog-samples (GitHub)
• SPARK - AdaCore
• Introduction to SPARK - learn.adacore.com
• SPARK 2014 Reference Manual
• GNATprove User’s Guide
• Ada Reference Manual (Ada 2022)
• Alire - Ada Library Repository
• Why3 - Platform for Deductive Program Verification
• Привлекательность языка Ada ── типы выражают проект, язык, который держит ПО, работающее десятилетиями - этот сайт

Похожие статьи

Недавние статьи с теми же тегами помогут подробнее изучить близкие темы.

Связанные темы

Эти страницы показывают тему статьи в более широком контексте услуг и решений.

Частые вопросы

Вопросы, которые часто возникают при консультациях по теме статьи.

Что такое SPARK и как он связан с Ada?

SPARK — подмножество (частичный язык) Ada, спроектированное так, чтобы свойства программы можно было доказывать математически. В обмен на ограничения — динамическое управление памятью через указатели, свободное использование исключений и другое — он даёт доказуемость. Код SPARK — это код Ada с контрактными аннотациями, поэтому он лежит на продолжении обычной разработки на Ada: отдельный синтаксис учить заново не нужно. Центральный инструмент — GNATprove от AdaCore: он переводит контракты в промежуточный язык Why3 и пытается доказать их автоматическими доказателями вроде Z3.

Чем формальная верификация отличается от тестирования?

Тест подтверждает, что программа корректно работает на выбранных входах. Формальная верификация математически доказывает, что свойство выполняется для всех входов. Комбинаций входов бесконечно много, поэтому одним тестированием корректность на всех входах не показать. Это не противники, а дополнение: на практике SPARK гарантирует уровень Silver (нет ошибок времени выполнения), модульные тесты проверяют конкретный ввод-вывод, а тестирование сосредотачивают на тех частях, которые доказать не удалось.

Что такое уровни доказательства SPARK (от Stone до Platinum)?

Это рамка, чтобы постепенно поднимать строгость доказательства. Stone — код является допустимым SPARK. Bronze — нет чтения неинициализированных переменных, поток данных такой, как задумано. Silver — нет ошибок времени выполнения (выход за диапазон, переполнение, деление на ноль). Gold добавляет к этому доказательство ключевых свойств целостности (integrity): сохраняются важные инварианты данных, переходы состояний соответствуют спецификации. Platinum — полная функциональная корректность: контракты покрывают функциональные требования, реализация доказанно соответствует спецификации; стоимость высока, примеров достижения немного. На практике самая полезная первая цель — уровень Silver.

Что делать, если GNATprove не может доказать?

Смотрят по сообщению. «postcondition might fail» — Post слишком сильный, Pre слишком слабый, или не хватает инварианта цикла. «overflow check might fail» — ограничивают диапазон значений в Pre или сужают диапазон самого типа. «array index check might fail» — инвариантом показывают, что диапазон цикла лежит внутри диапазона массива. «prover timeout» — дробят доказательство инвариантами поэтапно или режут функцию на более мелкие. Первый шаг всегда один: прочитать код и решить, может ли он действительно завершиться неудачей.

Об авторе

Страница с профилем автора статьи.

Го Комура

Представитель KomuraSoft LLC

Специализируется на разработке программного обеспечения для Windows, техническом консалтинге и расследовании сбоев, особенно в проектах с унаследованными системами и трудно воспроизводимыми ошибками.