2018-02-23
1663
Контрактное программирование (designbycontract – DbC) — это метод проектирования ПО. Он предполагает, что проектировщик должен определить формальные, точные и верифицируемые спецификации интерфейсов для компонентов системы. При этом, кроме обычного определения абстрактных типов данных, также используются предусловия, постусловия и инварианты.
Основная идея контрактного программирования — это модель взаимодействия элементов программной системы, основывающаяся на идее взаимных обязательств и преимуществ. Контракт некоторого метода или функции может включать в себя (в списке ниже поставщик – это метод):
· конкретные обязательства, которые любой клиентский модуль должен выполнить перед вызовом метода — предуслови я, которые дают преимущество для поставщика — он может не проверять выполнение предусловий;
· конкретные свойства, которые должны присутствовать после выполнения метода — постусловия, которые входят в обязательства поставщика;
· обязательства по выполнению конкретных свойств — инвариантов, которые должны выполняться при получении поставщиком сообщения, а также при выходе из метода.
Контрактное программирование подразумевает эти требования критическими для корректности программ, поэтому они должны быть утверждены при проектировании. Таким образом, контрактное программирование предписывает начинать писать код с написания формальных утверждений корректности (assertions).В ООП контракт метода обычно включает следующую информацию:
· возможные типы входных данных и их значение;
· типы возвращаемых данных и их значение;
· условия возникновения исключений, их типы и значения;
· присутствие побочного эффекта метода;
· предусловия, которые могут быть ослаблены (но не усилены) в подклассах;
· постусловия, которые могут быть усилены (но не ослаблены) в подклассах;
· инварианты, которые могут быть усилены (но не ослаблены) в подклассах;
· (иногда) гарантии производительности, например, временная сложность или сложность по памяти.
Таким образом, для выражения ожидаемого поведения используются утверждения(assertions), а для того, чтобы понять, кто в программе не прав, вызывающий или вызываемый код, то добавлено несколько видов утверждений:
1. Предусловия – нарушения которых говорит о баге в вызывающем коде («клиент не прав»).
2. Постусловия – нарушения которых говорят о баге в вызываемом коде («сервис не прав»).
3. Инварианты класса – нарушения которых также говорят о баге в вызываемом коде. Это ОО-специфическая штука, которая позволяет четко сказать, чем же является валидное состояние объекта, чтобы не множить предусловия и постусловия. Тут нужно помнить, что инвариант валиден от момента создания объекта до момента его уничтожения – вызова деструктора/метода Dispose, но может быть не валидным *внутри* вызова метода. Инвариант должен быть валидным в *видимых точках*.
4. Утверждения о корректности реализации – нарушения которых также говорят о баге в вызываемом коде. Это макросы Asserts, вставленные в разные точки приложения и упрощающие отлов багов.
5. Инварианты цикла присутствуют в языке Eiffel, их можно игнорировать.
Тот факт, что нарушение утверждений – это баг, является очень важным, поскольку из этого следует, что в программе не должно быть возможности самовосстановления (это баг, его фиксация заключается в исправлении кода, в блоке catch с ним ничего сделать не удастся).
В чем же разница между контрактами и Asserts? Разница в том, что контрактное программирование подразумевает «интеграцию» утверждений в инструменты (среду разработки). Т.е. любаяполноценная реализация механизма «контрактов» должна предоставлять следующие возможности:
1. Возможность задавать уровень утверждений:
· убрать всё;
· оставить только предусловия;
· оставить предусловия и постусловия;
· оставить все утверждения.
2. Возможность генерации документации и удобный способ «обнаружения» контрактов в среде исполнения.
3. Возможность доказать корректность программы на этапе компиляции (статический верификатор).
Замечание о понятии корректности ПО. Д ан простейший пример. Что вы можете сказать о следующей функции:
int DoSomething(int y) {
int x = y / 2;
return x;
}
Сама по себе, эта функция не является ни корректной, ни не корректной. Понятие корректности приобретает смысл только в контексте ожидаемого результата. Эта функция является корректной к утверждению “Возвращаемое значение в два раза меньше аргумента”, но является некорректным к утверждению “Возвращаемое значение должно быть положительным”, поскольку нет никаких гарантий того, что в эту функцию не будет передано отрицательное значение. Таким образом, понятие корректности ПО можно рассматривать только по отношению к некоторой спецификации
Контракты C#. Класс Contractы (Пространство имен: System.Diagnostics.Contracts )
Для работы с контрактами кода можно использовать классы, доступные в пространстве имен System.Diagnostics.Contracts в.NET 4. И выше. Однако в VisualStudio15необходимый инструмент отсутствует. Понадобится загрузить расширение для VisualStudio из сайта MicrosoftDevLabs. Для проведения статического анализа с помощью этого инструмента требуется версия VisualStudioTeamSystem, а для анализа времени выполнения достаточно версии VisualStudioStandardEdition. На рис ниже показано окно свойств проекта с требуемым расширением.
Класс Contractсодержит статические методы для представления контрактов программы, таких как предусловие, постусловие и инвариантность объектов.
1. Предусловия -методы Requires () и Requires<TException> (). Метод Requires() принимает в качестве 1-го аргумента булевское значение, в качестве 2-го необязательного параметра – текстовую строку с сообщением, которое появляется при невыполнении контракта. Метод в случае невыполнения условия генерирует по умолчанию исключение типаContractsRuntime+ContractException. Метод Requires<TException>() генерирует исключение определенного типа.
2. Постусловия. Для задания постусловий используются Ensures() и EnsuresOnThrow<TException>(). Аргументы метода Ensures() определяются аналогично предыдущему случаю. EnsuresOnThrow<TException>() гарантирует, что разделенное состояние удовлетворит условию в случае генерации указанного исключения.
Метод Result<T>() используется для указания гарантированного возвращаемого значения.
OldValue<T>(T)Представляет значения, какими они были в начале метода или свойства. По умолчанию тип int.
3. Все требования контрактов, которые задаются в методе, независимо от того, являются они предусловиями или постусловиями, должны помещаться в начало метода.
Предусловия позволяют проверить условия на входе метода, постусловия – на выходе из метода. Реальный код, обслуживающий контракты, генерируется утилитой ccrewrite, находит все вызовы утверждений контрактов и вставляет в их место соответствующий код. В результате методContract.Ensures, который стоит в начале метода фактически происходит при выходе из метода.
4. Можно также назначить глобальный обработчик событияContractFailed, который будет вызываться при каждом нарушении контракта во время выполнения. При нарушении контракта возбуждается исключение ContractException. Но поставить обработчик на ContractException не получится, в пользовательском коде оно доступно как экземпляр Exception. Между концепцией исключения и нарушением контракта существует разница. Исключение возбуждается в случае возникновения ошибки, которая должна быть перехвачена и обработана где-то выше. Природа ошибки может быть различной: от получения ресурсов до ошибки кодирования. Нарушение контрактов всегда связано с ошибкой кодирования, поэтому другая обработка кроме прерывания приложения является излишней. Такой подход не приемлем для приложений, которые не должны прерываться даже в случае критической ошибки, именно для таких случаев есть возможность установить обработчик нарушения контракта
Contract.ContractFailed += (sender, args) =>
{ Console.WriteLine("{0}: {1}: {2}", args.FailureKind, args.Condition, args.Message);
args.SetHandled();
};
В данном примере при нарушении контракта будет выведено диагностическое сообщение. Вызов методе args.SetHandled() означает что исключение ContractException возбуждаться не будет.
5. Инварианты. Contract.Invariant() определяет условия, которые должны соблюдаться на протяжении времени жизни метода:
[ContractInvariantMethod] //обязательныйатрибут
private voidИмя_метода() //методбезаргументов, private – обязательно
{
Contract.Invariant (условие,необязательное_сообщение);
}
Тело метода – последовательность вызовов методов Contract.Invariant ().
using System;
...
usingSystem.Diagnostics.Contracts;
namespaceContr
{ public class Stack<T> // тестируемыйкласс
{ private List<T> list = new List<T>(); // списокэлементовтипаТ
public Stack() //конструктор
{ Contract.ContractFailed += (sender, args) => // добавлениеобработчика
{ Console.WriteLine("ContractFailed: {0} ", args.Message);
args.SetHandled();
};
}
publicintCount // свойство только для чтения
{get { return list.Count; }
}
publicvoidPush(Tt) // занесение новогоэлемента в объект Stack
{ Contract.Requires<Exception> (t!= null, "Вставляемый объект не должен быть null");
Contract.Ensures(Count == Contract.OldValue(Count) + 1, "Число элементов должно увеличиться на 1");
list.Add(t); // занесение новогоэлемента в list
}
publicTPop1() // удаление элемента изобъекта Stack
{ Contract.Requires<Exception>(Count > 0, "Списокнедолженбытьпуст");
// проверяемое требование
T obj = list.ElementAt(list.Count - 1);
list.RemoveAt(list.Count - 1);
Console.WriteLine("Элементсписка {0} ", obj);
returnobj;
}
publicTPop2() // удаление элемента изобъекта Stack
{ Contract.Ensures(Contract.Result<T>()!= null, "Извлекаемый объект не должен быть null");
// проверяемое требование
return (T)(object)(null);
}
publicTPop3() // удаление элемента изобъекта Stack
{ Contract.Ensures(Count == Contract.OldValue(Count) - 1,
"Число элементов списка при извлечении должно уменьшиться на 1");
// проверяемоетребование
return (T)(object)(null);
}
}//конецклассаStack
Class Program
{ Stack<string>st = null;
// Stack<string>st = new Stack<string>();
[ContractInvariantMethod]
