Спецификация требований
Предлагаемый подход к представлению требований основан на использовании контрактных спецификаций в форме пред- и постусловий. В отличие от классического Design-by-Contract, когда контракты определяются на уровне операций, мы предлагаем определять контракты для отдельных микроопераций, а контракт для операции в целом получать путем временнóй композиции контрактов отдельных микроопераций (Рис. 2.).
Рис. 2.Построение спецификации отдельной операции.
Здесь под микрооперациями мы понимаем некоторым образом выделенные аспекты функциональности операций, реализуемые за один такт работы модуля, а под временнóй композицией контрактов - спецификацию, в которой для каждой микрооперации указан номер такта, в конце которого должен выполняться соответствующий контракт.
В общих чертах процесс спецификации требований к отдельной операции состоит в следующем. Определяется предусловие, ограничивающее ситуации, в которых операцию можно подавать на выполнение. На основе анализа документации производится функциональная декомпозиция операции на набор микроопераций. Для каждой микрооперации определяется постусловие, описывающее требования к ней. После этого производится временнáя композиция спецификаций - постусловие каждой микрооперации помечается номером такта, в конце которого оно должно быть выполнено. Таким образом, контракт операции f, для которой выделено n микроопераций, формализуется структурой C=(pre, {(posti, τi)i=1,n}) .
Для контракта С=(pre, {(posti, τi)i=1,n}) введем следующие обозначения. Через preC будем обозначать предусловие операции (pre), через postC,i - постусловие i-ой микрооперации (posti), через τC,i - номер такта, в конце которого должно выполняться постусловие i-ой микрооперации (τi), через PostC(τ) - конъюнкцию постусловий микроопераций, помеченных тактом τ, то есть
{ postC,i | τC,i=τ }.
