Многие программисты испытывают затруднения при использовании формальных методов для решения проблем в своих программах, поскольку эти методы могут быть неоправданно сложными. Чтобы понять, почему это происходит, давайте воспользуемся методом проверки модели и решим относительно простую задачу:

Условия

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

TLA + и временная логика

Некоторые инструменты могут решить подобные проблемы. Например, решатели SMT, которые часто используются в этих случаях, используют логику предикатов для решения проблемы, но для этого требуется использование массива, что неудобно для программистов и часто приводит к излишне сложной последовательности действий. TLA +, с другой стороны, использует временную логику, которая позволяет программе использовать состояние системы как на текущем, так и на следующем шаге в одном операторе.

CatDistr' = CatDistr \ {n}

Это условие гласит, что после проверки за дверью 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 /= {}  
====================================================================

В этом примере:

  • Первая и последняя строки объявляют, что это исходный модуль.
  • == означает «равно по определению».
  • = означает, что вычисленные значения выражения равны
  • Двери - это постоянная установка в файле конфигурации.
  • CatDistr определяет комнату, в которой находится кошка.
  • Переменная LastDoor, которая представляет последнюю проверенную комнату, удобно считывает вывод программы. Для больших моделей такие переменные могут замедлить рабочий процесс программы и увеличить количество состояний, которые необходимо проанализировать. Однако в этой модели состояние теперь содержит историю того, какие двери были открыты. Таким образом, равные государства, созданные разными способами, теперь разные.
  • Предиктор Init описывает начальное состояние программы - в этом случае двери еще не открыты.
  • 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 + имеет расширенный графический интерфейс и запускается командой tla-toolbox. К сожалению, он не понимает файлы .cfg, поэтому параметры модели необходимо настраивать через меню.

Заключение

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

  • Простую программу для интерактивной проверки решения можно найти здесь.
  • Узнайте больше о TLA + здесь.

Читайте Новостной канал Waves
Следите за Waves Twitter
Смотрите на Waves Youtube
Подпишитесь на Waves Subreddit