Введение в формальную верификацию с SPARK ── От контрактов Ada к математическому доказательству
· Го Комура · Ada, SPARK, Формальная верификация, GNATprove, Контрактное программирование, Высокая целостность, Язык программирования, Высокая надёжность
1. Введение ── За пределами «запустить и проверить»
Самый распространённый способ обеспечить качество программного обеспечения — это тестирование.
Тест: проверяет, что программа корректно работает для выбранных входных данных
Но у тестирования есть неустранимые ограничения. Число возможных входных данных бесконечно, и одно лишь тестирование не может доказать корректность для всех них.
Здесь на помощь приходит формальная верификация (Formal Verification).
Формальная верификация: математически доказывает, что свойство выполняется для всех возможных входных данных
В предыдущей статье «Привлекательность языка Ada» был дан общий обзор Ada и вскользь упомянут SPARK.
Эта статья сосредоточена именно на практической формальной верификации с помощью SPARK и рассматривает следующее:
Что такое SPARK и как он связан с Ada
Как писать контракты (Pre/Post)
Как доказывать их с помощью GNATprove
Как проектировать инварианты циклов
Как управлять побочными эффектами с помощью контрактов потока данных (Global/Depends)
Стратегию поэтапного внедрения через уровни доказательства (от Stone до Platinum)
Как интегрировать SPARK в реальные проекты
Цель — дать вам возможность прочувствовать переход от тестирования к доказательству на реальных примерах кода.
Фрагменты кода из этой статьи собраны по главам и доступны как справочная коллекция на GitHub.
ada-spark-formal-verification - komurasoft-blog-samples (GitHub)
2. Что такое SPARK ── Подмножество Ada как вход в мир доказательств
SPARK — это подмножество языка Ada.
То, что это подмножество, — осознанное решение при проектировании.
Полный Ada → высокая выразительность, но полная верификация нереалистична
SPARK → ограничен верифицируемыми возможностями, что делает доказательство реалистичным
Основные ограничения, которые накладывает SPARK:
Динамическое управление памятью через указатели (access-типы) → контролируется моделью владения
Свободное использование обработчиков исключений → допускается в ограниченной форме
Рекурсивные структуры данных → ограничены из-за сложности доказательства
Свободное использование задач (tasking) → ограничено профилем Ravenscar
Слово «ограничения» может звучать стеснённо, но эти ограничения — плата за доказуемость.
Ядро инструментария SPARK — это GNATprove от AdaCore.
Как работает GNATprove:
1. Анализирует код Ada с аннотациями SPARK
2. Переводит контракты (Pre/Post) и утверждения в промежуточный язык Why3
3. Пытается выполнить доказательство с помощью автоматических доказателей, таких как Z3, CVC4 и Alt-Ergo
4. Сообщает результаты в виде сообщений прямо в исходном коде
Важно понимать: SPARK построен поверх Ada.
Код SPARK = код Ada + контрактные аннотации
Иными словами, SPARK — это естественное продолжение повседневной разработки на Ada. Не нужно заново изучать совершенно новый синтаксис.
3. Установка GNATprove и первое доказательство
Сначала настроим окружение для запуска GNATprove.
С помощью Alire можно создать проект, готовый к работе с SPARK, следующей командой:
alr init --bin spark_demo
cd spark_demo
Поскольку GNATprove поставляется вместе с компилятором GNAT, команда gnatprove доступна сразу же, как только проект собирается с помощью alr build.
В качестве первой цели доказательства напишем функцию, возвращающую абсолютное значение.
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 декларирует свойство «результат неотрицателен»
Атрибут '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 математически доказано, что возвращаемое значение неотрицательно.
Это и есть первый опыт знакомства с SPARK.
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 (раздел 9)
5. Доказательство отсутствия переполнения ── Гарантия численной безопасности
Одна из самых ценных на практике вещей, которые доказывает SPARK, — это отсутствие переполнения (overflow).
Рассмотрим этот код:
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 Invariants).
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 итераций?»
В циклах по массивам типичен паттерн «для уже обработанного диапазона выполняется P»
Слишком сильный инвариант невозможно доказать; слишком слабый не влечёт 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_Type)
with Global => (Input => Exchange_Rate),
Depends => (From =>+ (From, Exchange_Rate),
To =>+ (To, Exchange_Rate));
=>+ означает «зависит от предыдущего значения плюс эти дополнительные входные данные».
Преимущества контрактов потока данных:
1. «К чему прикасается эта функция?» видно с первого взгляда
2. Непреднамеренные побочные эффекты обнаруживаются на этапе компиляции
3. Они служат входными данными для анализа потока информации переменных
4. Они помогают визуализировать поток данных в крупных системах
9. Уровни доказательства ── Поэтапное внедрение от Stone до Platinum
SPARK определяет концепцию уровней доказательства (Proof Levels).
Попытка сразу полностью доказать весь код часто приводит к разочарованию. Поэтому SPARK предлагает стратегию постепенного повышения строгости доказательства.
Stone (уровень 0):
Только проверка синтаксиса контрактов и согласованности типов
Первый уровень, которого нужно достичь
Bronze (уровень 1):
Stone + доказательство отсутствия чтения неинициализированных переменных
Гарантия базовой корректности
Silver (уровень 2):
Bronze + доказательство отсутствия ошибок времени выполнения (выход
за границы, переполнение, деление на ноль)
Самая практичная цель
Gold (уровень 3):
Silver + доказательство условий Pre/Post
Гарантия полной функциональной корректности
Platinum (уровень 4):
Gold + доказательство независимости данных и потока информации
Для систем, критичных с точки зрения безопасности
Практическая стратегия внедрения:
Этап 1: довести весь проект до уровня Stone
→ выявить ошибки при написании контрактов
Этап 2: довести критически важные модули до уровня Silver
→ устранить переполнения и выходы за границы
→ большинство реальных ошибок устраняется уже здесь
Этап 3: доказать ключевую логику на уровне Gold
→ математически гарантировать функциональную корректность
→ доказать корректность алгоритмов
Этап 4: перейти к Platinum при наличии требований безопасности
→ выявить пути утечки информации
10. Практический рабочий процесс доказательства ── Сокращение переделок
Вот рабочий процесс для повседневного использования GNATprove:
1. Спроектировать типы и спецификации
Определить ограничения диапазонов и инварианты типов
2. Написать контракты (Pre/Post)
Выразить спецификацию в виде контрактов до начала реализации
3. Добиться успешной компиляции
Устранить ошибки компиляции с помощью GNAT
4. Запустить GNATprove на уровне Stone
gnatprove -P proj.gpr --level=0
5. Просмотреть предупреждения и при необходимости уточнить контракты
Особое внимание уделить проблемам инициализации
6. Стремиться к уровню Silver
gnatprove -P proj.gpr --level=2
Устранить все ошибки времени выполнения
7. При необходимости добавить инварианты циклов
Если доказательство не удаётся, проверить, не отсутствуют ли инварианты
8. Доказать функциональную корректность на уровне Gold
gnatprove -P proj.gpr --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. Гарантировать отсутствие ошибок времени выполнения (уровень Silver)
с помощью SPARK
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 (полное функциональное доказательство) — идеал, но начинать
стоит с Silver (отсутствие ошибок времени выполнения)
Даже одно только предотвращение переполнений даёт огромную
практическую пользу
3. Писать контракты, отталкиваясь от интерфейсов
Писать контракты в спецификации пакета (.ads) до реализации
При устойчивой спецификации любой разработчик сможет написать код,
удовлетворяющий контрактам
4. Интегрировать в CI/CD
Добавить gnatprove в конвейер CI
Останавливать сборку (или хотя бы предупреждать) при неудаче доказательства
5. Накапливать отчёты о доказательствах
Генерировать отчёты с помощью gnatprove --report=all
Отслеживать динамику недоказанных элементов со временем
Для проектов со смешанным кодом на C/C++ и Ada эффективен поэтапный подход:
1. Писать новые модули на Ada/SPARK
2. Взаимодействовать с C/C++ через Interfaces.C
3. Постепенно переносить в SPARK критически важные структуры данных
и логику верификации
4. Постепенно расширять охват SPARK
14. Ограничения и предостережения SPARK
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 ── Выражать проектирование через типы, поддерживать десятилетиями работающее программное обеспечение - Этот сайт
Похожие статьи
Недавние статьи с теми же тегами помогут подробнее изучить близкие темы.
Практическое руководство по Process Monitor (ProcMon) — как за 10 минут выяснить, почему «настройки не читаются» или возникает ACCESS DENIED
«Исправил конфигурационный файл, но изменения не применяются», «вчера всё работало, а сегодня приложение не запускается» — прежде чем лез...
Когда не стоит переводить Windows-приложение в веб: таблица решений и «разделение» как реальный выход
Запросов на перевод корпоративных Windows-приложений в веб становится всё больше, но для приложений с интеграцией оборудования, локальной...
Интернационализация приложений WinForms/WPF — resx, сателлитные сборки и переключение культуры на практике
Разбираем интернационализацию десктопных приложений Windows на практике: различие между CurrentCulture и CurrentUICulture, устройство рес...
CSV — не «просто текст»: практика работы с CSV в бизнес-приложениях на C# (кодировки, совместимость с Excel, защита от инъекций)
Разбираем типичные ошибки при вводе-выводе CSV в бизнес-приложениях — самописный парсинг через Split(','), искажение текста в Excel из-за...
Не оборачивайте HttpClient в using ── практика HTTP-взаимодействия в бизнес-приложениях на C# (паттерны создания, тайм-ауты, повторные попытки)
HttpClient в C#, создаваемый через using при каждом запросе, приводит к исчерпанию сокетов, а статический HttpClient перестаёт учитывать ...
Связанные темы
Эти страницы показывают тему статьи в более широком контексте услуг и решений.
Технические темы Windows
Раздел о разработке Windows, расследовании сбоев и использовании существующих активов.
Частые вопросы
Вопросы, которые часто возникают при консультациях по теме статьи.
- Что такое SPARK и как он связан с Ada?
- SPARK — это намеренно ограниченное подмножество Ada, спроектированное так, чтобы свойства программы можно было доказать математически. Он ограничивает трудно верифицируемые возможности — свободное использование указателей, неограниченную обработку исключений, рекурсивные структуры данных и неограниченное использование задач (tasking) — в обмен на доказуемость. Код SPARK — это код Ada с добавлением контрактных аннотаций, поэтому он является естественным продолжением повседневной разработки на Ada, а не отдельным языком. Инструмент GNATprove переводит контракты в промежуточный язык Why3 и пытается выполнить доказательство с помощью автоматических доказателей, таких как Z3, CVC4 и Alt-Ergo.
- Чем формальная верификация с SPARK отличается от тестирования?
- Тестирование проверяет, что программа корректно работает для выбранных входных данных; формальная верификация математически доказывает, что свойство выполняется для всех возможных входных данных. Эти подходы не противоречат друг другу, а дополняют: SPARK доказывает только те свойства, которые записаны в контрактах, тогда как тестирование способно выявить неявные предположения, никогда не зафиксированные явно, и проверить взаимодействие со средой выполнения. На практике удобно сочетание: гарантировать отсутствие ошибок времени выполнения с помощью SPARK, проверять конкретное поведение ввода-вывода модульными тестами и сосредоточить тестирование на тех частях, которые не удаётся доказать.
- Что такое уровни доказательства SPARK (от Stone до Platinum) и к какому стоит стремиться в первую очередь?
- SPARK определяет пять уровней возрастающей строгости: Stone (синтаксис контрактов и согласованность типов), Bronze (добавляется доказательство отсутствия чтения неинициализированных переменных), Silver (добавляется доказательство отсутствия ошибок времени выполнения — переполнения, выхода за границы, деления на ноль), Gold (добавляется доказательство функциональной корректности через Pre/Post) и Platinum (добавляется независимость данных и доказательство потока информации). Silver — самая практичная первая цель: большинство реальных ошибок устраняется уже за счёт исключения ошибок времени выполнения, — а к уровню Gold стоит стремиться для ключевой логики, корректность которой должна быть гарантирована.
- Что такое инвариант цикла и почему он нужен доказательствам SPARK?
- Инвариант цикла — это свойство, которое выполняется в начале каждой итерации и записывается с помощью pragma Loop_Invariant. Циклы выполняются произвольное число раз, поэтому доказателю нужен инвариант, чтобы рассуждать сразу обо всех итерациях: он выражает в виде формулы уже выполненную часть вычисления, а после последней итерации должен подразумевать нужную постусловие. Проектирование инвариантов — самый тонкий навык в доказательствах циклов: слишком сильный инвариант невозможно доказать, а слишком слабый не влечёт постусловие.
Об авторе
Страница с профилем автора статьи.
Го Комура
Представитель KomuraSoft LLC
Специализируется на разработке программного обеспечения для Windows, техническом консалтинге и расследовании сбоев, особенно в проектах с унаследованными системами и трудно воспроизводимыми ошибками.
Публичные ссылки