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

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

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

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

CatDistr' = CatDistr \ {n}

Это условие утверждает что множество комнат, в которых может находиться кот после проверки комнаты 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, последняя проверенная комната, введена для удобства чтения вывода программы. Для больших моделей такие переменные могут существенно замедлить работу программы увеличив количество анализируемых состояний (так как состояние теперь содержит историю, как оно возникло и одинаковые состояния созданные разными путями будут теперь разными).

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

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

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

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

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

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

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

CONSTANTS
  Doors = 6

INIT Init
NEXT Next

INVARIANT CatWalk

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

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

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

Заключение

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

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

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