Хабрахабр

Ловим кота с TLA+

Формальные методы считаются эффективным, но неоправданно сложным способом обеспечения надежности программного обеспечения. Используемые при этом инструменты существенно отличаются от привычных программисту. Эта статья написана с целью снизить порог вхождения в этот инструментарий. Я применю систему model checking не для решения сложно формулируемых задач спецификации ПО, а для решения понятной даже школьникам головоломки.

В одной из них находится кот. Вы находитесь в прямом коридоре с семью комнатами по одну сторону. Как только дверь закроется, кот перейдет в одну из соседних комнат к той, в которой находился. За один шаг можно заглянуть в одну из комнат, если там есть кот, он пойман. Задача — поймать кота.

TLA+ и темпоральная логика

Есть много инструментов, способных решать подобные задачи. Часто в таких случаях применяют SMT-солверы. Как правило, такие системы используют обычную логику предикатов и выражение последовательности действий получается достаточно сложным (приходится использовать что-то типа массива, с которыми работать не очень удобно). В TLA+ используется темпоральная логика, позволяющая в одном утверждении использовать состояние системы и на текущем, и на следующем шаге.

CatDistr' = CatDistr \

Это условие утверждает что множество комнат, в которых может находиться кот после проверки комнаты n совпадает с множеством комнат, откуда убрали n (если кот был там — он пойман и делать больше нечего).

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

Немного о множествах

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

Структура программы в TLA+

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

---- MODULE cat ------------------------------------------------------------- EXTENDS Integers CONSTANTS Doors
VARIABLES CatDistr, LastDoor Init == /\ CatDistr = 0..Doors /\ LastDoor = -1 OpenDoor(n) == /\ CatDistr' = 0..Doors \intersect UNION { {x-1, x+1} : x \in CatDistr \ {n} } /\ LastDoor' = n Next == \E door \in 0..Doors : OpenDoor(door) CatWalk == CatDistr /= {} =============================================================================

Первая и последняя строки — особенности синтаксиса декларации модуля.

== означает «равно по определению», в то время как одиночное = — это именно равенство вычисленных значений выражений.

Doors — константа модели, ее надо будет задать в конфигурационном файле.
CatDistr — распределение кота по комнатам.

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

Doors — множество всех комнат). Предикат Init описывает начальное состояние (0.. OpenDoor(n) описывает, что происходит при открытии двери в комнату n (в худшем случае, что кота там нет — иначе мы его поймали).

Дело в том, что существование чего-то означает, что TLA+ не знает, в какую именно комнату мы заглянем, по этому проверит правильность инварианта во всех случаях. Предикат Next выглядит немного странно — существует комната, в которую можно заглянуть.

Более понятно было бы написать

Next == OpenDoor(0) \/ OpenDoor(1) \/ ... \/ OpenDoor(Doors)

но тогда наш код будет работать только с фиксированным количеством комнат, а лучше сделать его параметризованным.

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

Конфигурация модели

CONSTANTS Doors = 6 INIT Init
NEXT Next INVARIANT CatWalk

Здесь все просто — мы указали количество комнат, начальное условия, условия изменения состояния и проверяемый инвариант.

Запускается модель из командной строки tlc2 -config cat.cfg cat.tla.

К сожалению, он не понимает .cfg-файлов и параметры модели надо будет настраивать через меню. У TLA+ есть развитый GUI, запускаемый командой tla-toolbox.

Заключение

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

→ Задача была найдена здесь

Материалы для изучения TLA+. На всякий случай простая программа для интерактивной проверки решения. Другая система model checking, Alloy описана здесь.

Теги
Показать больше

Похожие статьи

Добавить комментарий

Ваш адрес email не будет опубликован. Обязательные поля помечены *

Кнопка «Наверх»
Закрыть