Подготовка формальной модели¶

Подготовка формальной модели к динамической верификации в АНИС состоит из следующих шагов:

создать файлы с текстом модели
исправить синтаксические ошибки и ошибки типизации в тексте модели
настроить трансляцию модели в Python
исправить ошибки в модели, возникающие в процессе ее трансляции
доопределить значения констант и несущих множеств, чтобы все аксиомы и инварианты в начальном состоянии модели были выполнены

Написание исходных текстов модели¶

Формальная модель состоит из файлов-контекстов и файлов-машин. Файлы-контексты — это текстовые файлы с расширением .bc. Файлы-машины — это текстовые файлы с расширением .bm. В одном файле может располагаться только один контекст/машина. Название файла должно совпадать с именем его контекста/машины. Все файлы должны находиться непосредственно в директории src.

Создание исходных файлов модели¶

Создайте директорию src, если ее еще нет.
В директории src создайте файл, назовите его с расширением .bc, если это контекст, или .bm, если это машина.
При создании файла в VSCode сразу открывается редактор. Чтобы открыть файл для редактирования, нужно нажать на файл в дереве файлов (Explorer tab).

Синтаксис Event-B¶

Названия аксиом, охранных условий, действий должны предваряться символом @ и завершаться символом :.

Поддерживаются однострочные комментарии. Они начинаются с // и заканчиваются концом строки.

Подсказки при вводе¶

При вводе первых символов редактор показывает меню с предполагаемым продолжением. Поддерживаются следующие виды текстов для подсказок:

ключевые слова;
имена сниппетов (шаблонов текстов на Event-B);
компоненты модели (имена несущих множеств, именя констант, имена переменных и т.п.; пока не поддерживаются имена подкванторных переменных);
имена математических символов Event-B; ввод математических символов в «ascii» нотации не поддерживается.

Навигация по модели¶

Для перемещения по модели можно использовать следующие возможности:

текстовый поиск (так как модель находится в текстовом файле);
outline (строка вверху редактора);
Go to Definition (перемещается от использования компонента модели к месту его определения); вызывается из контекстного меню на идентификаторе.

Импорт/экспорт модели из Rodin¶

Чтобы импортировать модель из Rodin в АНИС, надо вызвать команду VSCode Event-B: Import the model from Rodin project.

Команда состоит из следующих шагов:

выбрать folder с формальной моделью, если работа идет в режиме multi-root workspace;
выбрать путь к директории с проектом Rodin (в этой директории должен находиться файл .project).

Все компоненты модели будут помещены в директорию src. Файлы с именами, совпадающими с именами компонентов модели, будут перезаписаны без предупреждения.

Чтобы экспортировать модель из АНИС в Rodin, надо вызвать команду VSCode Event-B: Translate all the model into Rodin XML. Шаги команды экспорта совпадают с шагами команды импорта.

Если имена аксиом, событий, охранных условий, действий в проекте Rodin не были идентификаторами (например, содержали пробелы), то при импорте они будут вставлены как есть, что приведет к синтаксическим ошибкам. Не следует использовать такие имена в проектах Rodin.

АНИС позволяет написать комментарий в любом месте. Это может приводить к синтаксическим ошибкам в экспортируемом проекте Rodin. Следует использовать комментарии только в конце формул.

Трансляция модели в Python¶

АНИС автоматически транслирует модель Event-B в исполнимый код на Python для проверки трассы. За каждой моделью закрепляется один из ее компонентов-машин, для которого генерируется исполнимый код. Такой компонент будет называться целевым.

АНИС добавляет следующую информацию в статусбар для каждой модели в workspace:

статус процесса трансляции (значок успешности и имя folder с моделью); это кнопка; по нажатию на ней открывается канал с дополнительной информацией о процессе трансляции;
целевой компонент; это кнопка; по нажатию на ней открывается диалог выбора целевого компонента.

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

Трансляция выполняется автоматически в следующих случаях (при условии, что целевой компонент выбран):

при активации расширения АНИС
при сохранении текста в редакторе Event-B
при смене целевого компонента

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

Список ошибок можно посмотреть в списке Problems, но он показывает только ошибки для активного редактора.

Нетранслируемые конструкции языка Event-B¶

множественные действия (то есть запрещено слева от знака присваивания писать более одной переменной)
действия :∈
действия :∣, кроме имитирующих тернарную операцию (то есть разрешено только v :∣ c and v' = a or !c and v' = b, где v — это некоторая переменная, a, b, c — это выражения)
кванторы, в которых есть подкванторная переменная без явного указания множества значений (этот квантор не задает значение переменной v: ∀ v · v ≠ w ⇒ v ∈ z; следует добавить явное множество значений: ∀ v · v ∈ t ⇒ (v ≠ w ⇒ v ∈ z))
конструкции pred, succ, prj1, prj2, id
отношения сюръективные, тотальные сюръективные, инъективные, тотальные инъективные
функции сюръективные, тотальные сюръективные, биективные
композиции ∘ и ;
операции над интервалами ⊗ и ∥
кванторные конъюнкция ⋂ и дизъюнкция ⋃
функции union и inter (но бинарные операции объединения и пересечения множеств поддерживаются)
множество всех непустых подмножеств ℙ1
операция получения обратного отображения ∼ («тильда-оператор»)

Структура генерируемого кода на Python¶

Транслятор строит «плоскую» версию целевого компонента, т.е. добавляет в него все необходимое из уточняемого компонента и из видимых контекстов.

Затем он строит следующие модули Python:

machine.py — модуль для машины
events\<event>.py — модули для событий (для каждого события, кроме INITIALISATION, строится отдельный модуль)
test_axioms.py — модуль с тестами в формате pytest для всех аксиом
test_invariants.py — модуль с тестами в формате pytest для всех инвариантов в начальном состоянии целевого компонента

Модуль для машины состоит из класса Machine, представляющего целевой компонент. Атрибутами класса являются несущие множества и константы из «плоской» версии целевого компонента.

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

Несущее множество представляется двумя атрибутами класса Machine: объектом и типом данных (классом). Объект представляет множество значений (в Event-B каждому несущему множеству сопоставлено множество элементов, даже если это несущее множество неограничено, объект представляет именно это множество элементов). Тип данных нужен для создания элементов несущего множества и использования в типовых подсказках (type hints). Последние позволяют статически находить часть ошибок в коде на Python, который будет написан вручную.

Объект для неограниченного несущего множества создается функцией infinite_carrier_set. Объект для ограниченного несущего множества создается функцией finite_carrier_set. Объект для явного несущего множества создается функцией explicit_carrier_set. Связь между объектом и типом данных является связью «один-к-одному», то есть не может быть несколько множеств значений у одного и того же типа и наоборот. Эта связь устанавливается в момент создания объекта. То есть сначала описывается тип (класс, вложенный в класс Machine), а затем с ним создается объект для множества значений.

Константы из «плоской» версии целевого компонента представляются в виде атрибутов класса Machine. Константа, являющаяся элементом несущего множества, создается функцией constant. Остальные константы имеют тип целых чисел, логических значений, кортежей (представляются при помощи tuple) и множеств (представляется при помощи frozenset). Они создаются функциями-конструкторами.

Переменные из «плоской» версии целевого компонента представляются атрибутами инстанса класса Machine. Событие INITIALISATION становится конструктором класса Machine. В нем создаются переменные со значениями из события INITIALISATION.

Остальные события из «плоской» версии целевого компонента представляются модулями в пакете events. Модуль содержит функцию, имя которой совпадает с именем события. Эта функция некоторым образом «вычисляет» значение охранного условия события и подготавливает все необходимое для выполнения действий события, когда они потребуются.

Аксиомы представляются функциями-тестами. Каждая функция вычисляет соответствующую аксиому. У функции есть параметр m типа Machine, чтобы обращаться к константам и несущим множествам.

Инварианты представляются функциями-тестами. Каждая функция вычисляет соответствующий инвариант в начальном состоянии целевого компонента. У функции есть параметр m типа Machine, чтобы обращаться к константам, несущим множествам и значениям переменных в состоянии (объекте m).

Настройка средств тестирования. Проверка аксиом и инвариантов¶

Класс Machine может содержать значения констант и несущих множеств, для которых аксиомы или инварианты не выполняются. Чтобы это проверить, нужно предварительно настроить средства тестирования на основе фреймворка pytest.

Установите расширение Python в VSCode (автоматически установятся еще два расширения Python Debugger и Pylance)
Создайте виртуальную среду (запустите команду Python: Create Environment..., в качестве типа среды укажите Venv, в качестве workspace folder выберите модельную, в качестве интерпретатора Python выберите тот, который не старше версии 3.9)
Откройте терминал в VSCode (вначале строки с приглашением должно быть написано (.venv), это означает, что виртуальная среда создана и активирована)
Установите библиотеку anis (в терминале напишите команду pip install <path>, где <path> — это путь к файлу с библиотекой anis), при этом в виртуальную среду установится инструмент pytest
Настройте pytest: в модельном workspace folder создайте файл conftest.py со следующим содержимым
```
from pytest import fixture
from anis.model.machine import Machine

@fixture
def m():
    return Machine()
```
Настройте средства тестирования в VSCode (перейдите на вкладку Testing, нажмите кнопку Configure Python Tests, укажите модельный workspace folder, укажите фреймворк pytest, укажите . в качестве корневой директории с тестами)

На вкладке Testing должны появиться тесты для аксиом и инвариантов. Запустите их (нажатием на треугольник справа от названия теста или директории с тестами). Если не все тесты успешно завершаются, необходимо уточнить значения констант и/или несущие множества. Нажатием на тест открывается редактор текста теста с дополнительной информацией о статусе теста.

Уточнение констант и несущих множеств¶

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

Создайте текстовый файл для класса-потомка (например, в корневой директории файл pymodel.py)

Добавьте в файл следующий текст:

from anis.model.machine import Machine

class FixedMachine(Machine):

   def __init__(self):
       super().__init__()

Измените класс, который инстанцируется в функции m() на созданный только что, в примере получается так:
```
from pytest import fixture
from pymodel import FixedMachine

@fixture
def m():
    return FixedMachine()
```

Запустите еще раз тесты-аксиомы и тесты-инварианты и проверьте, что статусы тестов (пока) не поменялись.

Чтобы задать новое значение для несущего множества, надо определиться с его видом: неограниченное, ограниченное или явное. Автоматически генерируемые несущие множества являются неограниченными.

Чтобы сделать несущее множество явным, нужно:

определить новый тип элемента несущего множества наследником типа элемента в классе Machine как атрибут класса-наследника Machine с сохранением оригинального имени типа (требование к типу быть классом-наследником предъявляется статическим анализатором Pylance)
при помощи него определить новые значения констант (так как константы связаны с конкретным типом элемента)
определить новое несущее множество при помощи explicit_carrier_set

Пример: если в Event-B написана аксиома

partition(XATTR_FLAGS, {XATTR_CREATE}, {XATTR_REPLACE})

то в классе-наследнике надо написать следующее:

class FixedMachine(Machine):
    ...
    class XattrFlagsItem(Machine.XattrFlagsItem): pass
    XATTR_CREATE = constant('XATTR_CREATE', XattrFlagsItem)
    XATTR_REPLACE = constant('XATTR_REPLACE', XattrFlagsItem)
    XATTR_FLAGS = explicit_carrier_set(XattrFlagsItem,
                          frozenset((XATTR_CREATE, XATTR_REPLACE)))

Чтобы сделать несущее множество ограниченным, нужно:

определить новый тип элемента несущего множества наследником типа элемента в классе Machine и оформить как атрибут инстанса класса-наследника с сохранением оригинального имени типа (требование к типу быть классом-наследником предъявляется статическим анализатором Pylance)
при помощи него определить новые значения констант (так как константы связаны с конкретным типом элемента) как атрибуты инстанса класса-наследника
определить новое несущее множество при помощи finite_carrier_set

Пример: если в Event-B написаны аксиомы

finite(FILES)
card(FILES) = MAX_FILES

то в классе-наследнике надо написать следующее:

class FixedMachine(Machine):
    ...
    def __init__(self):
        ...
        class FilesItem(Machine.FilesItem): pass
        self.FilesItem = FilesItem
        self.FILES = finite_carrier_set('FILES', FilesItem, self.MAX_FILES)

Чтобы переопределить константу, тип которой использует ограниченное несущее множество, нужно определить его как поле инстанса класса-наследника. Иными словами, такие константы должны определяться в конструкторе класса-наследника. Пример:

class FixedMachine(Machine):
    ...
    def __init__(self):
       ...
       self.ROOT = constant('ROOT', FilesItem)

Остальные константы (использующие только встроенные типы, неограниченные и явные несущие множества) нужно определять как атрибуты класса-наследника. Пример:

class FixedMachine(Machine):
    ...
    O_RDONLY = 1

Если не работают такие возможности редактора Python как подсказки при наборе, автоимпортирование, языковой сервер Pylance может работать в неполном режиме (для экономии потребляемых ресурсов). Чтобы перевести его в полноценный режим работы, необходимо установить настройку "python.analysis.languageServerMode" в значение full. После перехода в полноценный режим может потребоваться некоторое время для индексации всего массива программных модулей.

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