Этап написания неявной спецификации (корректность операций системы по отдельности с известным состоянием)

Это сообщение является продолжением сообщения "Для чего нужна часть курса ФСВП о спецификации" и посвящена имплицитным (неявным) спецификациям.

Крайне рекомендуется к прочтению всем, кто выполняет этап написания неявной спецификации в рамках практического задания по RSL.


В вводной части было сказано, что сейчас для нас программа - словно "черный ящик", которому мы подаем входные воздействия и смотрим реакции, если они есть. В части, посвященной этапу написания алгебраической спецификации, мы занимались тем, что формально давали определение правильной системы с нужной функциональностью, если мы не знаем, какими структурами данных представлено состояние системы. В этом случае мы описывали корректные сеансы работы системы, при этом под корректностью понималось соответствие ожидаемых внешних эффектов полученным в реальности. Однако  "сеансовый метод" позволяет судить о выполнении далеко не всех функциональных свойств системы. Во-первых, ввиду ограниченного числа операций системы, обладающих внешним эффектом. Во-вторых, если мы всё же знаем, какими структурами данных представлено внутреннее состояние системы, то можем использовать систему более эффективным образом, но при этом мы должны точно знать, какие изменения во внутреннем состоянии делает система. Какие внутренние состояния запрещены, хоть и выразимы типами, задающими структуры данных. Какие внутренние состояния разрешены только для определенных операций. Какими получаются внутренние состояния после выполнения операции. Опять же поскольку внешний эффект операции зависит от внутреннего состояния, то мы можем более точно сформулировать внешний эффект (в результате чего верификация будет более тщательной, к чему мы как раз и стремимся). Тем самым мы приходим к возможности описания операций системы "с известным, или открытым, состоянием". Мы будем формулировать свойства операций системы (на каких внутренних состояниях и аргументах их выполнение разрешено, какими свойствами обладает внутреннее состояние после выполнения операции, какими свойствами обладает внешний эффект) в виде пред- и пост- условий. А на внутреннее состояние мы можем (и должны) сформулировать и инвариантные свойства.


Итак, в рамках этапа написания неявной спецификации мы знаем, какими структурами данных представлено внутреннее состояние системы. Рассматриваем каждую операцию системы в отдельности от других операций (т.е. думаем о правильности системы не в рамках ее сеансов работы, а в рамках ее отдельных операций). Но мы не знаем реализацию операций, т.е. алгоритмов формирования внутреннего состояния и внешнего эффекта. Более того, может быть несколько реализаций с совершенно разными алгоритмами, но поддерживающими выполнение одних и тех же пред- и пост- условий и инвариантных свойств (например, одна реализация есть . Из этого надо сделать вывод, что пред- и пост- условия должны позволять иметь несколько реализаций, но не должны допускать те из них, которые частично или полностью не выполняют основные функциональные особенности операций. Например, пусть у нас есть БД с операцией добавления данных. Структура данных, представляющая БД, пусть лишь для примера будет достаточно простой: список данных. Но этого мало, надо еще знать, как должна эта структура данных поддерживаться. Пускай в нашем примере это будет такой свойство: список не содержит пропусков, т.е. каждый элемент списка, от головного до завершающего, есть реальные данные, находящиеся в БД. Тогда следующее постусловие:
    type DB = Data-list
    variable db : DB
    value insert : Data -~-> write db Unit
    insert(d) post  db = db` ^ <.d.>
значит не только помещение данных d в базу данных, но и указание конкретного места, куда надо их поместить, что не имеет отношения к инвариантным свойствам типа DB (что должно давать сомнение в правильности постусловия), а, кроме того запрещает реализацию, в которой данные бы помещались, например, в начало (а такая реализация по выбранным инвариантным свойствам допустима!). Правильное постусловие должно формулировать лишь свойства содержимого, но не их порядок:

    type DB = Data-list
    variable db : DB
    value insert : Data -~-> write db Unit
    insert(d) post
           len db > len db`
           /\
           (all i : Nat :- i isin inds db` => db`(i) isin db)
           /\
           (all i : Nat :- i isin inds db =>
                db(i) = d \/  db(i) isin db` ) 

Постусловие должно описывать критерии правильности операции, не имеющие отношения к алгоритмам выполнения операций. Посмотрите на пример с insert: мы просто проверяем, что нужные данные есть в db. Представьте, что некто написал реализацию, вы не знаете деталей этой реализации, но вы знаете, какую функциональность она должна поддерживать. Ваша задача - проверить, правильная ли реализация. Реализация выполняет операции, вычисляет вам новое внутреннее состояние (db) и эффект (в примере с insert он отсутствует). Вы для операции составляете список проверок вычисленного и "проверяете" его этими "проверками". Чем-то это напоминает проверку преподавателем работ его учеников. На нашей второй контрольной работе есть задача, где надо выписать все неверные условия верификации/корректности/завершаемости. Эта задача - как операция, у нее есть внешний эффект (те самые условия в ответе ученика). Преподаватель, взяв решение, использует такие критерии правильности:

• не указано, какая формула означает какое условие (завершаемости, корректности или верификации)
• указан вид формулы, но с ошибкой
• выписано только одно условие
• не выписано ни одного из условий из правильного решения
• выписано истинное условие, которое верно составлено, но не входящее в правильное решение
• выписанное условие составлено неверно, но вид его правильный

Здесь преподавателю совершенно всё равно, каким алгоритмом пользовался ученик для решения задачи. Есть ответ - есть оценка за него. Подобную же деятельность будете вести и вы, когда будете писать пред- и пост- условия.

Подводя итог, сформулируем план работы по выполнению этапа написания неявной спецификации.

1. Договориться об интерфейсе системы (в частности, берем из алгебраической спецификации тот же интерфейс); еще раз обратите внимание, что типы аргументов  и внешних эффектов операций могут быть лишь "простыми": числами, булевскими значениями, enumeration, строками;
2. Договориться о представлении внутреннего состояния системы (структуры данных, представляющие внешний эффект были выбраны на этапе написания алгебраической спецификации); т.е. речь идет о структурах данных и об инвариантных свойствах; Вам разрешается выбрать это всё самостоятельно, но надо получить согласие семинариста, написав ему эти структуры данных и описав словами инвариантные свойства, снабдив этот выбор обоснованием на основе эффективности; на этой структуре данных с этими инвариантными свойствами должна быть возможность написать эффективную реализацию вот прямо с такими же структурами данных; при необоснованном выборе или выборе без учета эффективности, семинарист вам откажет и попросит прислать другое предложение о структурах данных и инвариантных свойствах;
3. Записать структуры данных и инвариантные свойства на RSL
4. Для каждой операции системы сформулировать предусловие и постусловие, записать его на RSL. Следить за тем, чтобы постусловие не запрещало иметь разные реализации. 

Инвариант типа можно задать двумя способами: либо при помощи аксиом (как было в первой контрольной работе), либо при помощи подтипов. В любом случае сначала надо написать тип, задающий структуру данных, например,
     type Persons0 = Person-list
А затем написать другой тип, которым вы будете везде пользоваться в качестве внутреннего состояния, и этот тип имеет аксиомы или ограничение подтипа. Для аксиом надо писать следующее:
    type Persons = Persons0
    axiom all p : Persons :-   условие корректности для p
Для ограничений подтипа надо написать следующее:
   type Persons = {| p : Persons0 :-  условие корректности для p  |}
Если Вы определите только тип Persons0 и будете им пользоваться в операциях, то везде придется добавлять предусловием "условие корректности для p" и постусловием "условие корректности для p в измененном состоянии". Это сделает вашу спецификацию более громоздкой, оно вам надо? :)

Хороший программный контракт не «намекает» ни на одну из реализаций. Пример контракта, который намекает на реализацию, в котором плохо видны критерии правильности результата операции (требования вида «что-то тогда и только тогда то-то» и, аналогичные им, равенства структур данных предполагают их построение, что перегружает спецификацию) :

schedule_for_passanger : Schedule -> Item-list

schedule_for_passanger(sch) as sch_pass

post

( all item : Item :- (modify(item) isin sch_pass) =

( item isin all_items(sch) /\ have_stop(item) ) ),

Более удачный вариант:

schedule_for_passanger : Schedule >< Station -> Item-list

schedule_for_passanger(sch, station) as sch_pass

post

( all item : Item :- item isin all_items(sch) =>

(have_stop(item) => modify(item) isin sch_pass)

/\ ( all item : Item :- item isin sch_pass =>

have_stop(item) )

/\ ( all item : Item :- item isin sch_pass =>

isin_respect_to_modifications(s, item) ),

isin_respect_to_modifications : Schedule >< Item -> Bool

isin_respect_to_modifications(sch, item) is (

exists i : Item :- i isin s /\

track(i) = track(item) /\ … /\
(if … then day_arrive(i) = day_arrive(item) else … end) )

Каждый квантор всеобщности, после которого подкванторная переменная ограничивается неким множеством, может быть автоматически странслирован в цикл по множеству. Поэтому это крайне удачная форма описания проверок в постусловии. Аналогично с квантором существования.

Удачные программные контракты написаны так, что они не создают новых сущностей и потом проверяют их равенство, а разбивают существующие сущности на составляющие и проверяют их.

Как в Dafny в requires и ensures запрещено вызывать методы, так и у нас — в программных контрактах старайтесь не вызывать операции системы (но можно вызывать дополнительные функции, введенные только лишь для задания программного контракта и не требуемые к реализации). Вызов операций системы не запрещен синтаксисом и семантикой RSL, но является крайне дурным тоном.

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