Контрактное программирование
Контрактное программирование
(программирование по
контракту, Design by Contracts,
DbC) – подход к созданию
программ высокого качества
Автор подхода – проф. Бертран
Мейер
Впервые введено в языке
программирования Eiffel
1985 год
Ицыксон В.М. Технологии разработки ПО © 2011-12
Основная идея – объединить
программный код и спецификации
Спецификации (контракты) встраиваются
в программу
В основе лежит логика Хоара
Тройка Хоара: {P}С{Q}
◦ P и Q – утверждения
◦ С – часть программы
Ицыксон В.М. Технологии разработки ПО © 2011-12
В терминах контрактного
программирования метод (или функция)
обязуется выполнить контракт:
◦ Если на вход поступили данные
удовлетворяющие входному
∙ условию
контракта, то метод гарантирует соблюдение
выходного условия
◦ Если входные данные НЕ удовлетворяют
первому условию, то ничего не гарантируется
◦ При этом соблюдаются некоторые обобщенные
условия
Ицыксон В.М. Технологии разработки ПО © 2011-12
Входное условие называется предусловием
(precondition)
Выходное условие – постусловием
(postcondition)
Дополнительно обеспечивается поддержка
инвариантов.
Инвариант (invariant) – условие, которое не
должно нарушаться из-за выполнения метода,
т.е. должно гарантироваться выполнение
инварианта до и после выполнения метода
◦ Во время выполнения инвариант может быть временно
нарушен!
Ицыксон В.М. Технологии разработки ПО © 2011-12
Пример 1. Метод, вычисляющий корни
квадратного уравнения a∙x²+b∙x+c=0
Предусловие:
◦ a≠0
Постусловие:
◦ Вариант 1:
a∙x1²+b∙x1 +c=0;
a∙x2²+b∙x2 +c=0
◦ Вариант 2:
x1 + x2 = -b/a;
x1 ∙x2 = c/a.
Ицыксон В.М. Технологии разработки ПО © 2011-12
Пример 2. Снятие денег в банкомате
◦ Balance – сумма на счете клиента
◦ Cash – сумма, которую клиент хочет снять
◦ Amount – денежный запас банкомата
Предусловия:
◦ Cash > 0;
◦ Cash ≤ 10000;
Постусловия:
◦ Balance = old(Balance) – Cash;
◦ Amount = old(Amount) – Cash;
Инвариант:
◦ Amount ≥ 0;
◦ Balance ≥ - 1000;
Ицыксон В.М. Технологии разработки ПО © 2011-12
В ООП языках программирования
контракты могут являться часть
объектной модели.
При наследовании:
◦ Предусловия у наследников могут быть
ослаблены
◦ Постусловия у наследников могут быть усилены
◦ Инварианты у наследников могут быть усилены
Ицыксон В.М. Технологии разработки ПО © 2011-12
Проверка всех условий во время
исполнения
◦ В случае нарушения – останов
◦ Возможность отключения проверок в релизах
Статические проверки
◦ Вывод с помощью дедуктивных методов
◦ Проверка контрактов с помощью методов
статического анализа
Ицыксон В.М. Технологии разработки ПО © 2011-12
Документирование
◦ Предусловия + постусловия + интерфейс
класса – документирование методов
◦ Инварианты + интерфейс класса –
документирование классов
Тестирование
◦ Контракты могут служить основой для
автоматизированного тестирования:
Предусловия и инварианты – ограничения на
генерируемые тесты
Постусловия и инварианты – основа для
построения тестовых оракулов.
Ицыксон В.М. Технологии разработки ПО © 2011-12
Контракты задаются с помощью
выражений логики первого порядка с
использованием:
◦ целочисленной арифметики
◦ вещественной арифметики
◦ И.т.п
Контракты – сугубо декларативное
описание требовний
Ицыксон В.М. Технологии разработки ПО © 2011-12
Языки со встроенной поддержкой
◦ Eiffel
◦ SPEC#
◦ Fortress
◦ D
◦ …
Языки с добавленной поддержкой
◦ C# (Code Contracts)
◦ Java (JML, Modern Jass, CoFoJa и т.п.)
◦ ADA
◦ C/C++ (DbC средствами препроцессора)
◦ …
Ицыксон В.М. Технологии разработки ПО © 2011-12
