Сборка модели и воспроизведение доказательств¶

Для подтверждения того, что модель полностью доказана, ее необходимо собрать (build). В ходе сборки Rodin сначала сгенерирует утверждения для доказательства (proof obligations), а потом попробует применить к ним сохраненные в модели доказательства.

Для сборки модели необходимо в левой части интерфейса Rodin в окне Event-B Explorer щелкнуть правой кнопкой мыши по названию модели и выбрать в выпадающем меню Build Project:

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

Если это так, то модель является полностью доказанной.