История языка Real

Как найти монетку?

Н. В. Шилов, Е. К. Шилова

1. Трудная задача

Математику уж затем учить надо,
что она ум в порядок приводит.

М.В. Ломоносов

Однажды, во время подготовки задач областной олимпиады по математике для школьников 6–8 классов, один из членов жюри предложил для обсуждения следующую головоломку.

Дано 15 внешне одинаковых монет, среди которых одна — фальшивая, а остальные — настоящие. Все настоящие монеты имеют равный вес, а фальшивая монета имеет другой вес. Кроме того, есть одна гирька, равная по весу настоящей монете. Возможно ли найти фальшивую монету за (не более чем) 3 взвешивания на чашечных весах?

«Эта головоломка позволит сразу выделить лидера олимпиады», — аргументировал он своё предложение.

Возникла кратковременная пауза: все члены жюри задумались над решением предложенной задачи о фальшивой монетке. Молчание прервал другой член жюри: «Да-а, это интересная и трудная задача… Я пока не знаю, как её решить…” “По правде сказать, я тоже не знаю, как её решить”, — неожиданно “парировал” член жюри, предложивший задачу. “Ну, тогда и нечего обсуждать её”, — подвёл итог короткого обсуждения Председатель жюри.

Однако вердикт Председателя жюри ещё не означает окончания этой абсолютно правдивой истории. Дело в том, что среди членов этого жюри был один программист-теоретик. Он тоже не смог решить задачу сразу во время заседания, но решил разобраться с ней на досуге. Весь день после заседания он то и дело возвращался к анализу этой задачи. Увы, безрезультатно! Ночью монетки, взвешивания, весы стали его настоящим кошмаром…

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

Человеко-ориентированный подход к решению головоломки был задуман чрезвычайно просто. По совместительству теоретик работал преподавателем математического факультета в Новосибирском Государственном Университете. Поэтому на первом же занятии на следующий день со студентами он предложил эту головоломку студентам. Им был установлен и приз за первое решение: ксерокопия 100$ США.

Человеко-ориентированный подход быстро дал положительный результат, хотя теоретику не пришлось делать ксерокопию 100$, так как первой решила головоломку его жена, которая тут же отказалась от приза. А вот машинно-ориентированный подход к олимпиадной головоломке потребовал дополнительных размышлений.

Во-первых, эту головоломку естественно считать частным случаем следующей параметрической головоломки.

Дано N внешне одинаковых монет, среди которых одна — фальшивая, а остальные — настоящие. Все настоящие монеты имеют равный вес, а фальшивая монета имеет другой вес. Кроме того, есть одна гирька, равная по весу настоящей монете. Возможно ли найти фальшивую монету за (не более чем) K взвешиваний на чашечных весах?

Во-вторых, для поиска подхода к решению параметрической головоломки стоит разобрать какой-либо простой частный случай, когда ответить на вопрос о возможности найти фальшивую монетку значительно проще, чем в олимпиадной головоломке. Давайте, например, разберём случай M = 5 и
K = 2, когда надо найти одну фальшивую среди 5 монет за 2 взвешивания с помощью дополнительной гирьки, вес которой равен весу настоящей монеты.

В этом случае фальшивая монета может иметь любой номер из 1, 2, 3, 4 или 5, а вес её может быть как легче (л), так и тяжелее (т), чем у настоящей монеты. Значит, всего есть 5 ? 2 = 10 различных вариантов (номер, вес) фальшивой монеты. Ниже приведено 2 варианта фальшивой монеты и поиска этой монетки.

Наблюдение, которое можно сделать, рассматривая эту таблицу, следующее: процесс поиска фальшивой монетки очень напоминает игру двух партнёров — один пытается найти фальшивую монету (назовём его Догадой), а другой — осуществляет взвешивание монет на весах (назовём его Весовщиком). Ходы Догады состоят в выборе монет для взвешивания, а ходы Весовщика — это результаты взвешиваний монет. Давайте назовём описанную выше игру игрой в монетки (но не на деньги!).

Раунд — это пара последовательных ходов партнеров в игре. Тогда параметрическую и олимпиадную головоломку можно переформулировать следующим образом:
•  Существует ли в игре в N монеток выигрышная стратегия из K раундов?
•  Существует ли в игре в 15 монеток выигрышная стратегия из 3 раундов?

2. На помощь приходит компьютерная наука

Компьютерная наука занимается изучением вычислительных машин
не более чем астрономия занимается изучением телескопов

Э. Дейкстра

Игровая модель головоломок очень понравилась программисту-теоретику. Но ещё необходимо было разобраться, как формально выразить неформальное понятие выигрышной стратегии.

Вот тут-то и пришла на помощь современная компьютерная наука. Говоря о вкладе компьютерной науки в сокровищницу знаний человечества, во-первых, необходимо назвать языки программирования, т.е. языки явного описания в каком порядке производить преобразования данных. Но, во-вторых, необходимо сказать о языках спецификаций, которые позволяют описывать свойства данных и вычислений без явного упоминания порядка преобразований и конкретных значений данных. Примеры языков программирования известны многим людям, начиная со школы: популярные Бэйсик и Фортран, Си и Паскаль, Лисп и МЛ, Лого и Пролог. А вот примеры языков спецификаций известны только “широкому кругу узких специалистов”. Однако (будучи вхожим в этот круг) программист-теоретик использовал один из таких языков спецификаций для машинно-ориентированного решения параметрической головоломки, а именно: для формулировки понятия выигрышной стратегии была использована стратегия Пропозициональной Динамической Логики (ПДЛ).

Как и русский язык, язык ПДЛ состоит из слов, а из слов уже строятся предложения ПДЛ. Слово ПДЛ может быть действием или событием. Действия изменяют значения данных (например, позиции в игре), приводят к переходу от одних значений к другим (поэтому логика называется “динамической”). События не могут изменять значения данных, но для одних значений событие имеет место, а для других — нет. Предложения в языке ПДЛ часто называют спецификациями, высказываниями или пропозициями (поэтому и логика называется “пропозициональной”).

ПДЛ позволяет описывать формально, или (как это принято говорить в “широком кругу узких специалистов”) специфицировать, те позиции игры в монетки, где у Догады есть выигрышная стратегия в 1 раунд, в 2 раунда, в 3 раунда, и, вообще, для любого значения параметра K, где у Догады есть выигрышная стратегия в K раундов.

Проверка значений данных в модели, которые удовлетворяют спецификации, называется проверкой модели. Методы проверки моделей отличаются друг от друга тем, с какими моделями может работать тот или иной метод, какие языки спецификаций поддерживают, и, наконец, по своей эффективности. По-видимому, первыми, кто понял их прикладное значение, были американские исследователи Эдмунд Кларк и Алан Эмерсон и французский учёный Джозеф Сифакис. Произошло это около 20 лет назад в начале 1980-ых годов. Эти методы сразу стали применяться для анализа программного обеспечения и компьютерного оборудования. За прошедшие годы было разработано и реализовано на вычислительных машинах несколько десятков таких методов. Может быть, самая популярная реализация метода проверки моделей — это пакет SMV. Этот пакет был создан американским учёным Кеном Макмилланом. Сейчас свободно распространяются версии этого пакета для работы под Windows и Unix. Они доступны в Интернете.

Вот теперь уже всё готово для машинно-ориентированного решения олимпиадной головоломки: модель, спецификация и пакет проверки моделей SMV. Программисту-теоретику оставалось только скачать пакет SMV через Интернет, установить его на своём компьютере, запрограммировать в терминах, понятных SMV, игру в 15 монеток и ПДЛ-спецификацию позиций, где у Догады есть выигрышная стратегия в три раунда.

3. Распределённые системы

Здесь можно было бы закончить статью на мажорной ноте: олимпиадная головоломка решена! Да, решена, только программист-теоретик не использовал пакет SMV, а пошёл другим путём. Он использовал небольшую программу проверки моделей, написанную его коллегами для совместных исследований по проверке свойств протоколов на моделях распределённых систем. Вот об этих исследованиях и пойдёт речь в оставшейся части статьи…

Распределенная система — это несколько устройств, время от времени обменивающихся информационными сообщениями друг с другом. Так, например, распределённую систему образуют два компьютера, один из которых (клиент) посылает напарнику запросы на выполнения определённых действий, а второй (сервер) — информирует своего напарника о результатах этих действий; распределённую систему такого типа часто так и называют “системой клиент—сервер”. Глобальная распределенная система — это Интернет, объединяющий миллионы компьютеров-серверов и миллиарды компьютеров-клиентов.

Но не следует думать, что устройства распределённой системы обязательно должны быть вычислительными машинами. Распределённая система может включать как вычислительные машины, так и живых людей. Именно поэтому лучше говорить не об устройствах, а о взаимодействующих агентах. Например, в игре в монетки Догада и Весовщик — два агента, которые образуют распределённую систему типа клиент—сервер: Догада — это клиент, а Весовщик — это сервер; клиент запрашивает сервер произвести взвешивание, а сервер его производит и информирует клиента о результатах.

Распределённые системы всё чаще встречаются в современном мире, а их надёжность и свойства протокола становятся критическим моментом социальной, экономической и военной стабильности. Например, если протокол обмена сообщениями через Интернет между клиентами-покупателями и сервером e-магазина не обеспечивает секретности индивидуальных банковских pin-кодов, то такое положение дел чревато как экономическим ущербом для покупателей, так и банкротством e-магазина.

Осознавая значение надёжности распределённых систем, Международный Телекоммуникационный Союз ITU (International Telecommunication Union) в период 1976–2000 гг. разработал специальный стандарт Z100 для проектирования распределённых систем. Этот стандарт получил название SDL (Specification and Design Language). По-русски его называют по-разному, например, языком формальных описаний. Нам кажется, что гораздо лучше перевести его по-другому: “specification” — “техническое задание”, “design” — “эскизное проектирование”; получается “язык технического задания и эскизного проектирования” или, кратко, “язык Тех-Про”.

Язык SDL имеет мощные средства описания структуры распределённых систем, индивидуальных агентов, возможных сообщений и потоков сообщений, посылаемых от агента к агенту. Этот язык имеет математически точные правила, которые позволяют (в принципе) реализовать все его конструкции на современных языках программирования. Эти правила называются операционной семантикой языка SDL. Но плата за выразительную силу языка — сложность операционной семантики для понимания и реализации. Достаточно сказать, что только описание правил семантики занимает более 500 страниц.

Ещё один недостаток языка SDL — это отсутствие средств описания свойств. Другими словами, нет стандартного языка спецификаций для систем и данных, описанных на языке SDL. В результате получается, что у нас есть возможность спроектировать на этом языке систему покупки товаров через Интернет, но нет возможности специфицировать свойство такое, что протокол обмена сообщениями между покупателями и e-магазином обеспечивает тайну индивидуальных банковских pin-кодов. А раз нет возможности специфицировать свойства, то у нас нет возможности при помощи вычислительных машин их проверять.

4. Особенности национальной науки

Вернёмся к исследованиям по проверке свойств протоколов на моделях распределённых систем, в которых участвовал программист-теоретик вместе со своими коллегами по лаборатории Теоретического программирования в Институте систем информатики Сибирского Отделения Российской Академии Наук (ИСИ СО РАН) ещё с конца 1980-х годов. Ещё существовал Советский Союз, ещё выдвигались амбициозные национальные проекты. Один из этих проектов — создание национальной телекоммуникационной сети нового поколения.

Одним из основополагающих принципов этого проекта было использование языка SDL на всех этапах: от разработки требований до программной реализации. Такое массовое использование языка SDL предполагало разработку новых эффективных машинно-ориентированных методов исследования свойств распределённых систем. Группа научных сотрудников лаборатории Теоретического программирования ИСИ СО РАН, участвовавшая в этом национальном проекте, пришла к выводу, что самое реальное — проверять на моделях свойства протоколов для разрабатываемой национальной телекоммуникационной сети.

Жёсткая привязка всего телекоммуникационного проекта к языку SDL диктовала жёсткое условие: язык описания моделей распределённых систем должен быть настолько близок к языку SDL, чтобы быть понятным инженерам-разработчикам самой системы. Кроме этого языка описания моделей, должен быть “естественный” язык спецификации свойств этих моделей, который не требует дополнительно упрощать модели распределённых систем. И, наконец, и язык описания моделей, и язык спецификации свойств этих моделей должны быть поддержаны эффективными методиками проверки этих свойств в этих моделях.

После нескольких лет поисков, в 1992 г. научной общественности был представлен проект языка REAL. Этот язык состоит из двух равноправных частей: исполняемых спецификаций и логических спецификаций. Исполняемые спецификации языка REAL очень близки к языку SDL и служат для создания моделей распределённых систем. А логические спецификации языка REAL — это вариант Пропозициональной Динамической Логики (ПДЛ), обогащенный некоторыми дополнительными средствами, и служат они для спецификации свойств моделей. В 1992 г. язык ещё не имел формальной операционной семантики, пригодной для реализации на компьютере, но был снабжён неформальным описанием.

Отличительная особенность языка REAL — это широкие возможности работы со временем, каких нет в SDL . Модель времени, принятая в языке, позволяет так реалистично описывать течение времени у разных агентов в распределённых системах, что авторы языка единодушно выбрали название «Реал». Это русское название превратилось в английское « REAL », так как впервые язык был представлен на Международной конференции “Перспективы системной информатики”, рабочий язык которой был английский.

Первый успех позволял двигаться дальше: на очереди стояла задача формальной операционной семантики языка REAL. Но пути возникли трудности совсем ненаучного характера: в 1992 г. уже не было Советского Союза, и прекратились скоординированные работы по проекту создания национальной телекоммуникационной сети нового поколения. Одни научные и инженерные коллективы, ранее занятые в этом проекте, вообще прекратили своё существование, другие — сменили тему исследований, а некоторые — попытались продолжить начатые исследования по проекту с надеждой на свои силы и с верой в перспективность своего подхода. Именно так поступила группа авторов языка REAL.

В 1992-94 гг. участникам этой группы приходилось работать на энтузиазме: государственного заказа на исследования по проверке свойств моделей распределённых систем уже не было, негосударственных научных фондов для поддержки фундаментальных исследований ещё не было. Рассказывают, что в конце 1920-х годов участники Группы Изучения Реактивного Движения (ГИРД), создавшие первые советские ракеты, в шутку расшифровывали аббревиатуру ГИРД так: Группа Инженеров, Работающих Даром. Так вот, в 1992–94 гг. небольшой коллектив, занятый разработкой операционной семантики языка REAL92, можно было назвать ГУРД: Группа Учёных, Работающая Даром.

Несмотря на все трудности (научные и ненаучные), возникшие перед группой учёных, работавших даром, в 1994 г. первая версия операционной семантики языка REAL была представлена специалистам на международном рабочем совещании по моделям параллельных вычислений в Берлине. Отличительная особенность этой семантики — краткость. Достаточно сказать, что формальное и неформальное описание всей семантики занимает всего 25 страниц. (Сравните с сотнями страниц семантики SDL.) В то же время, эта семантика доступна для новичков и реализуема на компьютере.

Научные успехи 1994 г. совпали с началом финансирования исследований по языку REAL Международным Научным Фондом Дж. Сороса (ISF — International Scientific Foundation), Международной Ассоциацией развития сотрудничества с учёными новых независимых государств бывшего СССР (INTAS — INTernational ASsociation for promotion of cooperation with new independent states) и Российским Фондом Фундаментальных Исследований (РФФИ). В конце 1994 г. были получены небольшие и краткосрочные гранты от ISF и INTAS. Но кардинальные изменения произошли в конце
1995 г., когда исследования получили поддержку от INTAS и РФФИ в виде совместного гранта ИНТАС—РФФИ 95-0378 «Методы и средства верификации и анализа распределенных систем» (рук. В. А. Непомнящий) на период 1996–1999 гг.

5. П.Д.Л. = Полный. Детский. Льготный

Если на клетке слона написано “Буйвол”,
не верь глазам своим.

Козьма Прутков “Мысли и афоризмы”

Итак, к середине 1990-х годов была разработана операционная семантика языка REAL для описания моделей и свойств распределённых систем. Теперь можно было ставить задачу проверки свойств распределённых систем в этих моделях.

Здесь можно было пойти на использование метода “грубой силы”: запрограммировать какой-либо универсальный метод проверки моделей, а потом его применять ко всем моделям и всем свойствам автоматически, без вмешательства человека. Но такой подход — чересчур затратный для проверки простых свойств, которые чаще всего возникают на практике. Поэтому возникла идея разобраться с проверкой наиболее часто встречающихся свойств, а дополнительно реализовать какой-либо универсальный метод проверки моделей для остальных свойств.

Что касается универсального метода проверки моделей, то выбор пал на так называемый ускоренный метод проверки моделей, который был теоретически разработан группой зарубежных ученых в 1992 г. Программная реализация этого метода оказалась довольно-таки практичной и в настоящее время широко используется для проведения различных экспериментов в ИСИ СО РАН. В частности, именно эта программа проверки моделей была использована программистом-теоретиком для машинно-ориентированного решения олимпиадной головоломки.

Теперь время рассказать про проверку свойств распределённых систем, которые часто встречаются на практике. Здесь на помощь пришла идея классифицировать эти свойства. Еще в 1980-х годах американские учёные Мани Чанди и Джадев Мишра и израильские ученые Захар Манна и Амир Пнуели разработали основы такой классификации и исследовали приёмы математического доказательства свойств, попадающих в предложенную ими классификацию. Ими было замечено, что очень многие свойства распределённых систем, вызывающие реальный интерес, могут быть отнесены к четырем классам.

Вот пример одного из этих классов:

после наступлений события P,
при любом сценарии работы распределённой системы
в некоторый момент времени наступит событие F.

Свойства, которые попали в этот класс, получили условное название свойств прогресса. (Позже мы приведём пример такого свойства, который прояснит это название.)

Для этих классов были разработаны простые шаблоны (схемы) для конструирования доказательств свойств распределённой системы. Шаблоны не зависят от распределённой системы, а только от свойства. Эти схемы позволяют конструировать эскизы доказательств, которые сводят доказательство сложных свойств из этих классов к доказательству большого числа простых свойств, легко выразимых в самых простых терминах Пропозициональной Динамической Логики (ПДЛ). Эскизы доказательств отличаются краткостью и простотой. Они легко могут быть сконструированы вручную одновременно с эскизным проектом распределённой системы, так как свойства всех четырёх классов имеют очень простую структуру. А вот доказательство простых свойств может оказаться непростым делом, так как нет никаких ограничений на события P и F, а они могут использовать очень ёмкие и сложные понятия.

Описанный подход к доказательству свойств распределённых систем был адаптирован для проверки свойств моделей распределённых систем, описанных на языке REAL. Главная идея состояла в том, что простые свойства, которые возникают после применения шаблонов доказательств, не надо доказывать, а надо проверять при помощи простого метода проверки моделей для самых простых формул ПДЛ. Так как этот подход использует классификацию на классы проблем и метод проверки моделей, то за ним закрепилось название “проблемно-ориентированный методики проверки моделей”. Эту методику можно считать основным результатом исследований 1996-1999 гг. по проверке свойств моделей распределённых систем, описанных на языке REAL. (Другие важные результаты, полученные в этот период, — это аниматор исполняемых спецификаций и конвертор SDL в исполняемые спецификации.)

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

после наступлений события P =
"пассажир и касса готовы к работе",
при любом правильном сценарии работы
распределённой системы "касса-пассажир"
в некоторый момент времени наступит событие F =
"касса выдаст билет пассажиру до нужной станции".

Было рассмотрено несколько моделей этой системы и вариантов спецификации свойства на языке REAL. Причём, новые модели и варианты появлялись в результате исправлений в модели и уточнений спецификаций после применения к ним проблемно-ориентированной методики проверки. Типичные ошибки, которые возникали при последовательном уточнении и исправлении распределённой системы «касса-пассажир» и при формальной спецификации ее свойств, были двух сортов:
•  отсутствовала «чистка мусора»;
•  не соблюдались временные ограничения.

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

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

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

Следующая статья сборника

Из сборника "Новосибирская школа программирования. Перекличка времен". Новосибирск, 2004 г.
Перепечатываются с разрешения редакции.