Евгений Корныхин - Формальная спецификация программ (1185143), страница 9
Текст из файла (страница 9)
Контрактные спецификацииopen: Окно ̃︁→ Окно × Табне требуетсяВ Окне достигнут максимум одновременнооткрытых табовпоявляется один таб, в этом табе нет адреса,место этого таба пока не решено, все остальные табы и их порядок остаются без измененийОперация «Переход по ссылке»сигнатураgo: Окно × Адрес × Таб ̃︁→ Окнототальностьне требуетсяситуации, когда опера- Таб не входит в Окноция невозможнаэффект операции вразных ситуациях∙ В ситуации, когда достигнут максимумодновременно открытых табов, заменяется адрес в Табе на Адрес, остальныетабы и их порядок не меняются;сигнатуратотальностьситуации, когда операция невозможнаэффект операции вразных ситуациях∙ В остальных ситуациях открывается новый таб и ему прописывается АдресОперация «Закрытие существующего таба»сигнатураclose: Окно × Таб ̃︁→ Окнототальностьне требуетсяситуации, когда опера- Таб не входит в Окноция невозможнаэффект операции вразных ситуациях∙ В ситуации, когда это единственный открытый таб, табу не соответствует никакой адрес;∙ В остальных ситуациях Таб отсутствует,все остальные табы и их порядок сохраняютсяВыбрав подходящую модель состояния (на языке множеств, спискови отображений RSL), можно сформулировать инварианты состояния и2.3.
Программные контракты общего вида в RSL. Превыражения69программные контракты всех операций над системой.2.3123456Программные контракты общего вида вRSL. ПревыраженияПрограммные контракты общего вида — это пара «чистых» логических выражений RSL (поствыражение и превыражение), оформленныхв виде имплицитного описания функции («чистое» — значит завершающееся детерминированное без побочных эффектов).
Например:type Element , Stack = Element *value∼top : Stack → Elementtop ( s ) as epost e = s ( 1 )pre s ̸= ⟨ ⟩Превыражение — это «чистое» логическое выражение на тех входныхданных, на которых имеет смысл стоящее перед ним определение функции или утверждение (об утверждениях будет разговор чуть позже). Например, в последнем примере функция top при непустом стеке должнабыть такой, как сказано в поствыражении, а при пустом стеке можетбыть какой угодно. Превыражение ограничивает значения свободныхпеременных, на которых формулируется утверждение и определение, вкоторое они входят.
Для имплицитных описаний функций свободнымипеременными являются все входные данные (в последнем примере это s).Тем самым, написав превыражение, мы сказали, что данное имплицитное описание надо рассматривать не при всех s типа Stack (т.е. не длявсех списков из Element), а только для непустых списков. Про пустыесписки это описание ничего не говорит.Спецификация, в которой не сказано про поведение ряда операцийпри некоторых значениях входных данных, называется недоспецификацией.Однако пока неясно, можно ли при помощи превыражений и поствыражений выразить на RSL то, что удовлетворяет определениям постусловий и предусловий. С поствыражением вопросов никаких нет — оновполне может выполнять роль постусловия.
Вопрос только с превыражением: может ли средство ограничения области, в которой делается данное утверждение, быть условием на среду, при выполнении которого га-70Глава 2. Контрактные спецификациирантируется выполнение постусловия. На самом деле, поскольку можнонаписать только одно имплицитное/эксплицитное описание для операции, то и превыражение может быть сопоставлено только одно. Поэтомупревыражение у имплицитного/эксплицитного описания может выполнять роль предусловия (в общем случае превыражение не выполняетроль предусловия).Для рассматривавшейся ранее модели стека с операцией top:1234type Element , Stack = Element *∼value top : Stack → Elementtop ( s ) ≡ s ( 1 )pre s ̸= ⟨ ⟩при предусловии «стек непустой» операция гарантирует возврат значения s(1), значит при совершении операции взятия вершины стека при пустом стеке может произойти всё, что угодно (операция может завершиться с возвратом какого-нибудь значения, зациклиться, аварийно остановиться).
Но написав данное превыражение у определения, мы утверждаем, что при пустом стеке из текста эксплицитного описания нельзя сделать вывод о том, что произойдет при совершении операции взятия вершины стека. Этот пример ещё раз подчёркивает, что превыражение — неявляется средством выражения предусловия в том же его понимании.Напомним, что функция удовлетворяет требованию тотальности,если она детерминированно завершается на каждом значении входныхданных (на каждом значении из типов входных данных) и результат также соответствует типам выходных значений.
Здесь стоит отметить, чтоесли описание функции содержит превыражение и требование тотальности, то требование тотальности должно быть выполнено не только вобласти выполнимости превыражения, а даже в более широкой области(области значений типов входных данных). Например, в следующем описании:1234type Element , Stack = Element *value top : Stack → Elementtop ( s ) ≡ s ( 1 )pre s ̸= ⟨ ⟩сказано, что при непустом стеке функция должна возвращать головусписка, а при пустом стеке функция должна возвращать некое значениев типе Element, но, какое именно, в спецификации не сказано.2.4. Финитные программные контракты71В заключение хочется отметить, что контрактная спецификация операции (т.е.
сформулированный набор её свойств) зависит от того, какоевыбрано модельное состояние. Один вид модельного состояния позволяетсформулировать более конкретно и саму ситуацию, и эффект операции вней, а другой, например, позволяет задать только допустимые эффектыоперации.2.4Финитные программные контрактыПост- и превыражения общего вида не всегда удобны для проверки, поскольку не любое логическое выражение в RSL можно вычислить.Например, такое выражение:1∀ x : Int∙∃ y : Int∙x + y = 0предполагало бы просмотр всех целых чисел (в качестве х) и для каждогох ещё один просмотр всех целых чисел (в поиске нужного y). Как легкозаметить, оба эти просмотра не осуществимы за конечное время (ввидубесконечности типа Int). Хотя понятно, что при вычислении логическихвыражений без кванторов таких проблем нет. Нет их и в тех случаях,если кванторы ограничены.
Ограниченным квантором будем называтьследующие конструкции при конечном множестве ts:12∀ t : T∃ t : T∙∙t ∈ ts ⇒ . . .t ∈ ts ∧ . . .Такие кванторы могут быть легко превращены в заведома завершающийся обход множества. Аналогичная ситуация происходит при составлениимножества:1{ f(t) | t : T∙... }Назовем ограниченным конструктором множества следующее выражение при конечном множестве ts:1{ f(t) | t : T∙t ∈ ts ∧ . .
. . }В этом случае можно вычислить значение такого множества, фильтруяэлементы множества ts.По аналогичной причине надо ограничить использование рекурсии влогических выражениях, поскольку вызов рекурсивной функции можетпривести к зацикливанию. К зацикливанию может привести и использование операторов цикла в поствыражениях.72Глава 2. Контрактные спецификацииКроме того, использование функций, для которых нет эксплицитногоописания, также невозможно в поствыражениях, предназначенных длявычисления. Это достаточно очевидно просто потому, что для вычисления выражения необходимо уметь вычислять значение всех входящих вэто выражение функций, а если для такой функции нет эксплицитногоописания, то вычислить ее зачастую нельзя.Суммируя вышесказанное, назовем логическое выражение финитным, если для него выполнены все следующие свойства:1) все кванторы и конструкторы множеств, списков и отображенийограниченные;2) нет рекурсии и операторов циклов;3) нет вызовов функций без эксплицитного описания;4) нет бесконечных сущностей (целых чисел бесконечного значения,вещественных чисел бесконечной точности, бесконечных типов-множеств,типов-списков, типов-отображений.Назовем финитными программными контрактами такие программныеконтракты RSL, в которых поствыражение и превыражение являютсяфинитными.2.5Инварианты состоянияИнвариант состояния — это «чистое» логическое выражение.
Это выражение выделяет среди всех состояний, допустимых его сигнатурой,некоторое подмножество. Это подмножество должно означать согласованные, допустимые, состояния. Например:12345type S o r t e d L i s t = Nat *axiom ∀ s : S o r t e d L i s t ∙ s o r t e d ( s )values o r t e d : Nat * → Bools o r t e d ( s ) ≡ ( ∀ i : Nat ∙ { i , i +1} ⊆ inds s ⇒ s ( i ) ≤s ( i +1) )т.е. после ключевого слова axiom идет квантор всеобщности с переменной типа модельного состояния, подкванторным выражением является инвариантное свойство.2.5.
Инварианты состояния73ЗадачиОписать функциональность операцийВ задачах этого типа требуется составить описание подобное тому,какое было составлено для «Окон с Табами». Если данных в задаче недостаточно, требуется определить те ситуации, в которых поведение системы не описано, и доопределить поведение в таких ситуациях адекватнымобразом. В большинстве задач требуется выделить операции пользователя, которые выполняются посредством системы. У системы практическивсегда есть внутреннее состояние. Если у сеанса работы с системой естьграницы, то правильная система не должна позволять работать внеэтих границ (до того, как начат сеанс, и после того, как становится известно, что сеанс закончен), например, играть в игру можно только дотех пор, пока игра не будет закончена. Не забыть про операции инициализации системы (например, когда начинается игра).2.1.1 «Неазартное ’Двадцать одно’». Задача системы — визуализировать поле игры в «21» (это карточная игра) и модифицировать егов ответ на команды игрока (т.е.
в этой задаче не надо думать о всейпрограммной системе для игры в Двадцать одно, надо думать толькоо том, по каким правилам должно «работать» содержимое поля игры).В колоде 36 карт разных мастей, каждая карта имеет свою стоимость.Играют двое: банкир и его соперник. Сначала соперник берет из колодыкарт себе карты, затем банкир берет из колоды себе карты. Если сумманабранных баллов по картам у соперника равна 21, он выиграл; больше 21 - проиграл; иначе если у банкира 21, он выиграл; если больше 21- проиграл; в противном случае выигрывает тот, кто набрал большуюсумму баллов.2.1.2 «Шашки». Задача системы — визуализировать поле игры вшашки и модифицировать это поле в ответ на команды игрока (т.е.
вэтой задаче не надо думать о всей программной системе для игры вшашки, надо думать только о том, по каким правилам надо работатьс содержимым поля игры). Поле 8 на 8. У каждого игрока 12 шашек.Отличия от стандартных шашек: 1) бить назад нельзя, 2) бить несколькошашек нельзя, 3) дамок нет.74Глава 2. Контрактные спецификации2.1.3 «Домино». Задача системы — визуализировать поле игры в домино и модифицировать это поле в ответ на команды игрока (т.е. в этойзадаче не надо думать о всей программной системе для игры в домино,надо думать только о том, по каким правилам надо работать с содержимым поля игры). Играют двое. Вначале каждый игрок произвольнымобразом получает половину всех доминошек. Ход игрока заключается ввыборе доминошки из своей кучи и вставки его линию с подходящегоконца.
Если игроку нечем походить, он проигрывает.2.1.4 «Пятнашки». Задача системы — визуализировать поле игрыв пятнашки и модифицировать это поле в ответ на команды игрока (т.е.в этой задаче не надо думать о всей программной системе для игры вдомино, надо думать только о том, по каким правилам надо работать ссодержимым поля игры). Поле 4 на 4 клетки. Все клетки, кроме одной,содержат фишку. Ход игрока состоит в том, что нужно передвинуть однуиз фишек, соседствующих с пустой клеткой на пустое место. Цель игры— выстроить фишки в соответствии с их номерами.2.1.5Написать спецификацию функции библиотеки POSIX intfork().
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
