Евгений Корныхин - Формальная спецификация программ (Евгений Корныхин - Формальная спецификация программ.pdf), страница 8

В структуре модельногосостояния могут совсем отсутствовать некоторые части реального состояния компонента, слабо связанные с его функциональностью, например,различного рода кэши и другие данные, используемые для увеличенияпроизводительности. Важно, что структура модельного состояния компонента должна содержать данные, достаточные для полного описанияфункциональности в пред- и постусловиях операций этого компонента.При этом предусловие зависит от аргументов вызова операции и данныхмодельного состояния при этом вызове, или пре-состояния. Постусловиезависит как от аргументов и пре-состояния, так и от результата и данныхмодельного состояния после вызова, или пост-состояния.Наличие сложной структуры модельного состояния приводит к необходимости учитывать в контрактах операций ограничения на его данные,которые должны выполняться в стабильных состояниях системы, когдани одна из операций не выполняется.

Такие ограничения оформляютсяв виде инвариантов модельного состояния. Инварианты являются общими частями пред- и постусловий всех операций, как-то затрагивающихсоответствующие компоненты — они должны выполняться как в пресостоянии любого вызова, так и в его пост-состоянии.2.2Ситуации и ветви функциональностиОбычно постусловие операции описывает несколько разных режимовее функционирования.

Предусловие запрещает все комбинации значе-64Глава 2. Контрактные спецификацииний параметров, при которых поведение операции не определено. Однако среди разрешаемых предусловием ситуаций могут остаться такие, вкоторых выполнить свою основную функцию операция не может. Вместоэтого она должна вернуть некоторый код ошибки, создать исключительную ситуацию или как-то иначе сигнализировать о том, что ее основная задача не может быть решена в такой ситуации.

Помимо режимовсигнализации о невозможности выполнить основную функцию, само еевыполнение может идти разными путями. Например, операция конкатенации двух строк может проверять, не является ли один из ее аргументовпустой строкой, и в этом случае просто возвращать копию другого аргумента, не выполняя никаких действий над ней. Если же оба аргументане пусты, копия одного из них должна быть подвергнута модификации,чтобы получить результат операции.При написании постусловий удобно выделять такие разные режимы,иначе постусловие превращается в большую и сложную формулу, трудную для анализа и понимания, что противоречит основной цели созданияформальных спецификаций. Различные режимы работы операции описываются в виде импликаций с несовместными посылками (постусловиепри этом выглядит как формула123(X1 ⇒ Y1) ∧(X2 ⇒ Y2) ∧ .

. .(Xn ⇒ Yn)или в виде разных выражений для возвращаемого результата приразных исходных условиях, т.е. результат постусловия вычисляется вразных ветвях некоторого условного оператора или оператора выборапо-разному. Поэтому эти разные режимы называют ветвями функциональности операции.Например, при выполнении операции перехода по ссылке в одном изтабов веб-браузера открывается новый таб или открывается новое окно с одним табом, или не открывается ни одного окна, ни одного таба(операция перехода по ссылке выполнилась — и мы видим эффект этойоперации: открытие таба или открытие окна, или неоткрытие таба инеоткрытие новых окон, эффект операции в формуле выше обозначенкак ).

В этой модели нас будут интересовать только работа с табамипри выполнении различных операций.Под «ситуацией» будем понимать совокупность значений входных параметров, некие условия, при которых эффект операции обладает заданной спецификой (ситуация обозначена в формуле выше как ). Напри-2.2. Ситуации и ветви функциональности65мер, в ситуации, когда достигнут максимальный предел одновременнопоказываемых табов, при переходе по ссылке всегда открывается одноновое окно с одним табом. В этом функциональном требовании операцией является «переход по ссылке», ситуацией — «достигнут предел максимально показываемых табов и потребовано открытие нового таба», эффектом операции является «открыто новое окно с одним новым табом»(по-хорошему, этот эффект требует дополнения).Еще несколько примеров.

«При выполнении операции закрытия табавсе остальные табы остаются без изменений» — ситуация «таб открыт»,операция «закрытие таба», эффект «все табы, кроме закрываемого, неизменились» (не изменилось их содержимое, заголовок и т.п., в зависимости от того, какие из характеристик таба входят в формальную модель).Заметьте, этот почти очевидный факт неполный. Он позволяет при закрытии таба изменить порядок табов. Тем самым, формальная модельсистемы с требованием «при выполнении операции закрытия таба всеостальные табы остаются без изменений» содержит логику выполненияоперации по закрытию таба с сохранением порядка и без сохранения порядка. Этот важный вывод о поведении системы получен чисто путеманализа формальной модели.

Например, из этого следует, что нельзяутверждать, что если один таб создан позже другого, то всегда будетсохранен их относительный порядок один после другого. Это замечание может оказаться важным при проектировании других операций стабами, которые будут предполагать сохранение относительного расположения табов.Возникает вопрос, какие факты нужно выделять, сколько фактовнужно выделять (когда фактов достаточно).

Поскольку ситуации выражены на формальном языке, можно точно определить, покрывают лиэти ситуации все возможные ситуации, в которых будет выполнятьсяоперация. Например, если выделена только ситуация закрытия таба длясвоего окна, то «для полноты картины» нужна ситуация закрытия таба для окна без этого таба (если такие окна обладают дополнительнойспецификой, влияющей на эффект закрытия таба, то требуется выделение для них дополнительных ситуаций). Полное выделение ситуаций— первый залог того, что поведение системы в спецификации описанополно.Следующий важный момент — это слежение за замкнутостью модели. Речь идет вот, о чем.

В правильной спецификации не может бытьтакого, что в результате выполнения операции в некоторой ситуации си-66Глава 2. Контрактные спецификациистема приходит в такое состояние, про которое неизвестно, как себя будутвести операции, выполняющиеся из полученного состояния. Грубо говоря, есть строго определенное множество допустимых состояний системы,или инвариант состояния системы, за которые операции не имеют права выводить систему. Например, инвариантами могут быть следующиефакты: «количество табов в окне не должно превысить максимально допустимое», «в каждом окне должен быть как минимум один таб». Однакопри проектировании операций придерживаются более гибкого подхода идопускается пересматривание инварианта, но в этом случае приходитсяперепроверять уже спроектированные операции для выявления того, вовсех ли ситуациях описано их поведение и не требуется ли дополнительно определить поведение системы при выполнении операции из новыхсостояний, вошедших теперь в инвариант.В некоторых ситуациях операция не может быть выполнена (например, нельзя закрыть единственный таб в окне — это приведет к нарушению инварианта (в окне не останется ни одного таба).

Знание о том,когда операция невозможна, так же важно, как и знание эффекта операции там, где операция возможна.Подводя итог, можно предложить следующий подход к формализации поведения системы.1) сформулировать уровень абстракции (например, ограничиваемсярассмотрением логики работы с табами в рамках одного окна браузера);2) выделить множество операций и составить их сигнатуры (например, открытие нового таба, переход по ссылке, закрытие таба);3) сформулировать наиболее общий инвариант на состояние системы(под «системой» в данном случае понимается окно браузера с табами; например, в каждом окне должен быть как минимум 1 таб);4) далее действовать итеративно до получения полного замкнутогоописания поведения системы при выполнении всех операций во всехситуациях:∙ выделить набор ситуаций на очередную операцию и описатьэффект операции в этих ситуациях (как минимум, выделитьситуации, в которых операция невозможна);2.2.

Ситуации и ветви функциональности67∙ проверить, что эффект всех операций согласуется с инвариантом;∙ при необходимости уточнить (усилить) инвариант или расширить (ослабить) инвариант — при этом снова проверить соответствие эффекта операций во всех ситуациях.В результате применения этого подхода к примеру с табами можетполучиться, например, следующая заготовка для функциональных требований:Понятия: Окно, Таб, АдресИнварианты:1) Окно есть совокупность табов;2) Табы в окне упорядочены;3) Все табы считаются различными;4) Табы содержатся в окнах, в табах окон нет;5) Каждому табу соответствует не более одного окна;6) В окне не может быть открыто табов больше некоторого максимума;7) Каждому табу соответствует некоторый один адрес или не соответствует никакого адреса.NB: Представьте, что браузер реализовали так, что какое-нибудь изэтих свойств корректности не выполнено.

Можно ли считать такой браузер правильным ?При описании операций будет упомянуто требование тотальности.Операция тотальная, если ни при каких своих входных данных (т.е. нипри каких значениях, входящих в типы входных данных) она не можетзациклиться или привести к аварийному останову системы. Иначе, операция называется частичная. Требование тотальности на RSL можноуказать. Для этого в сигнатуре соответствующей функции надо указатьстрелку без тильды (→).Операция «Открытие нового таба»68Глава 2.