Редактирование: ВПнМ/Теормин
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 92 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 951: | Строка 951: | ||
=== Верификация при помощи Spin. Задание свойств последовательностей состояний. Утверждения о невозможности. Трассовые ассерты. === | === Верификация при помощи Spin. Задание свойств последовательностей состояний. Утверждения о невозможности. Трассовые ассерты. === | ||
'''never claims (утверждения о невозможности):''' | '''never claims (утверждения о невозможности):''' | ||
- | * выполняются синхронно с моделью | + | * выполняются синхронно с моделью, |
- | * если достигнут конец, то – ошибка | + | * если достигнут конец, то – ошибка, |
- | * состоят из выражений и конструкция задания потока управления | + | * состоят из выражений и конструкция задания |
- | * фактически, описывают распознающий автомат. | + | потока управления |
+ | * фактически, описывают распознающий | ||
+ | автомат. | ||
'''Конструкция never''' | '''Конструкция never''' |