Выполнение практического задания по RSL

Выполнение практического задания по RSLЗадание состоит из трех этапов:1. анализ требований, алгебраическая спецификация;2. формальное описание программного интерфейса (реализации) системы, неявнаямоделеориентированная спецификация;3. реализация системы, явная моделеориентированная спецификация.Пример описания системы заказчиком:Требуется реализовать программу Geolocator. Программа предназначена для мобильногоустройства.

Она отображает карту некоторой местности и то, что на ней находится.Программа должна уметь:• сохранять указанные пользователем описания мест на карте ("Здесь живу я", "Тутмой любимый Университет" и т. п.);• показывать места в части карты, указанной пользователем;• при показе должны учитываться как указанные пользователем, так иподгружаемые с публичных серверов описания мест;• хочется иметь опцию, публиковать ли свое описание на публичном сервере.Первый этап.

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

п. Т.е. первый этап — эточеткая формулировка той информации, в которой работает система, которую она получаетизвне и которую она производит. Разработка системы после первого этапа не должнанаткнуться на неотвеченные вопросы вида: «Что оно делает?», «Как оно должно себявести в такой-то ситуации?»1. «то, что непосредственно сказано заказчиком»: сущности, операции какинформационные потоки.◦ «информационный поток» — это отображение всей информации, котораянужная для выполнения операции, на всю информацию, которую производитоперация.◦ «информационный поток» описывается просто в виде сигнатуры функции.◦ взглянув на «информационные потоки», должна возникать интуитивнаяидея, для чего какие сущности нужны, какую информацию они в себесодержат, какую информацию из сущностей можно извлечь.◦ если у функции описаны типы возвращаемых значений, то функция не можетне генерировать какое-либо из них, получив всё, что нужно, на свой вход.◦ нужно добиваться замкнутости операций: если в какой-либо функциииспользуется некий тип как вход, то нужна функция, генерирующая этот тип(из других типов, констант и т.

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

«увидеть особые значения типов»: посмотрев на каждый тип в спецификации,надо подумать, на какие важные множества значений разбивается всёмножество значений этого типа («какие бывают особенные случаи в сущноститакой-то»); увидев их, сформулировать в виде констант или доп. функцийобсерверов с аксиомами вида all t : T :- p1(t) \/ p2(t).4. объявить предусловия всех функций новыми дополнительными функциями(тотальными, возвращающими Bool).5. поделить все функции на обсерверы, генераторы и трансформеры и написатьалгебраические аксиомы вида «обсервер(генератор)» и«обсервер(трансформер)».◦ для сокращения можно использовать вариантные определения:type Pair == pair( left : Item ↔ change_left, right : Item ↔ change_right)обсерверы – left, right,генераторы — pair,трансформеры — change_left, change_rightпри таком описании будут автоматически объявлены все нужные аксиомынад этими функциями.Чего делать нельзя в этом этапе:1.

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

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

Взаголовочных файлах нет тел функций, но есть определения всех типов, которыеиспользуются в сигнатурах функций. Эта же идея работает в RSL: на этом этапе мыдолжны предложить структуры данных для типов и описать программные контракты дляфункций в предположении, что это функции из настоящей реализации! Аналогия с Dafny:на втором этапе не надо описывать тела методов, но надо сформулировать их requires иensures, при этом можно определять свои function (явным образом!) и их использовать вrequires и ensures.Получается, что над явной и неявной спецификациями нужно думать совместно, но внеявной спецификации указывать информацию для тех, кто будет пользоватьсяреализацией, а в явной — для тех, кто будет писать реализацию. По этой причине внеявной спецификации не должно быть того, что относится к реализации алгоритмов, нодолжно быть то, что относится к особенностям использования реализации в другом коде:когда функции реализации можно вызывать, какую предварительную подготовкунеобходимо сделать, какие входные данные можно подавать функции и каких результатовждать от функции.Можно перефразировать этот тезис так: неявная спецификация должна допускать какможно большее число различных эффективных реализаций в рамках той «задачи»,которую должна «решать» реализация (т.

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

Заметьте: при наличииповторов данных появляется проблема согласованного состояния. Например,если изначально структура данных была Key -m-> Data1 >< Data2, а мы хотимхранить предвычисленное множество первых данных, т. е. новая структураданных будет State = (Key -m-> Data1 >< Data2) >< Data1-set, то возможнытакие значения в типе State, например, как ([], {1}), в которых свойство«множество есть все первые данные» не выполнено, т.

е. значение ([], {1})является несогласованным. Значение ([0 +> (1, 2)], {1}) уже являетсясогласованным. Надо сформулировать то свойство данных, котороегарантирует согласованность, в виде инвариантов.3. Формулируем структуры данных и их инварианты.•инвариант можно формулировать в виде аксиомы или в видеподтипа с использованием предиката от состояния (is_wf : State0->Bool , State = {| s : State0 :- is_wf(s) |}).4. Формулируем пред- и пост- условия операций системы.Хороший программный контракт не «намекает» ни на одну из реализаций.

Примерконтракта, который намекает на реализацию, в котором не видны простейшие требования(требования вида «что-то тогда и только тогда то-то» и, аналогичные им, равенстваструктур данных предполагают их построение, что перегружает спецификацию и :schedule_for_passanger : Schedule -> Item-listschedule_for_passanger(sch) as sch_passpost( all item : Item :- (modify(item) isin sch_pass) =( item isin all_items(sch) /\ have_stop(item) ) ),Более удачный вариант:schedule_for_passanger : Schedule >< Station -> Item-listschedule_for_passanger(sch, station) as sch_passpost( 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 -> Boolisin_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).Третий этап. Реализация системы. Явная моделеориентированнаяспецификация.Тут всё довольно просто: выбираете эффективные реализации для функций изаписываете их в явном виде..