Хабрахабр

Ловим кота с 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 описана здесь.

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

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

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

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

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