Спасибо за ссылку, Драконограф!
Воспроизвожу по полученной ссылке форму цикла Дейкстры в языке Promela из указанного
источника:
Код:
proctype Euclid(int x, y){
do
:: (x > y) -> x = x - y
:: (x < y) -> y = y - x
:: (x == y) -> goto done
od;
done: skip
}
Здесь
skip - пустой оператор, перед которым стоит метка
done.
А вот как будет выглядеть тот же пример в PureBuilder:Код:
┌while
│▼ x > y
│ dec (x, y)
│▼ x < y
└ dec (y, x)
Алгоритм функции записывается не внутри длинного программного кода, а в отдельной вкладке интерфейса. Поэтому заголовок функции отсутствует.
Объявление параметров и возвращаемого значения функции Euclid осуществляется в отдельной табличке.
Псевдографика не очень правильно передает скобку слева. На самом деле она непрерывная, с закругленными углами и полностью охватывает строки с while и dec (y, x).
Ключевые слова должны изображаться жирным шрифтом. Значки ▼ используются при необходимости сворачивания соответствующих ветвей цикла. При этом они принимают вид ►.
Вход
FAQ
Поиск
