Драконограф писал(а): 1. Что подразумевается под синтаксической верификацией? Проверка структуры или всей модели (включая текст вершин)? 2. То же в отношении верификации маршрутной логики. 3. Имеете ли Вы в виду под структурой программы представление всего её текста - по такому принципу, как в этом примере?
Благодарю за ссылки, все очень любопытно. Пока, если честно, "глаза разбегаются" от количества информации на форуме 
1. Поскольку я до сих пор рассматривал Дракон как исключительно маршрутный язык, под синтаксисом подразумевается соблюдение правил компоновки икон.
2. см. далее про сети Петри.
3. Из п.1 следует что нет - речь пока только о модели программы (т.е. ее маршрутном графе, возможно с какими-то дополнениями).
Хочу поделиться возникшими мыслями (пусть знающие люди, если что, меня поправят).
1. Существует ли грамматика языка Дракон?
Под грамматикой подразумевается конечный набор правил (заданных, например, в виде формы Бэкуса-Наура), позволяющих однозначно определить принадлежность любой Дракон-схемы множеству корректных высказываний языка Дракон. Набор правил построения схем (описанных Владимиром Даниеловичом в книгах), насколько я понимаю, выведен эмпирически, т.е. в их основе не лежит какого-либо формализма. Следовательно, могут существовать схемы, корректные с точки зрения существующих правил, но некорректные с точки зрения, например, принципов структурного программирования (а это еще вопрос, какую базу взять за основу грамматики языка).
Поскольку обобщить обширный алфавит языка Дракон (и правила составления схем) в лаконичную грамматику с ходу не просто, я опишу последовательность своих мыслей с другой стороны: от частного к общему, взяв за основу мне (как программисту) привычную в области описания алгоритмов парадигму структурного подхода.
Вспомним теорему Дейкстры, согласно которой, любая программа может быть построена с использованием 3 конструкций: последовательность, условие, цикл. По всей видимости, теорема справедлива только для алгоритма с одним потоком управления, а для реализации параллельных вычислений к базовым 3-м добавляется еще FORK/MERGE.
Так мы получаем тезис: любой п-алгоритм (параллельный алгоритм) представим сочетанием 4-х базовых конструкций (возможны их взаимные вложенности).
В языке Дракон каждой базовой конструкции соответствует своя макроикона, точнее несколько макроикон. Наличие нескольких вариантов представления базовых конструкций делает схемы более выразительными, расширяет арсенал пользователя, и никак не нарушает выбранное ограничение алфавита макроикон 4-мя типами конструкций (на каждый тип несколько синонимов). Это минимальный маршрутный язык.
Здесь же стоит отметить, что ряд элементов языка являются "синтаксическим сахаром", т.е. при автоматической обработке они также сводятся к базовым конструкциям. Например, набор веток - силуэт. Если склеить все ветки (не на схеме, а при верификации) в одну последовательность, маршрут останется тем же. Все иконки связанные с комментариями - не учитываются, и т.п.
Очевидно, что все существующие иконы могут быть условно разделены:
1. Иконы, которые образуют макроиконы 4-х базовых типов (минимальный маршрутный набор).
2. Дополнительные иконы, являющимися расширениям минимального маршрутного языка.
Последовательность: заголовок, конец, действие, имя ветки, адрес ветки, петля силуэта.
Условие: выбор, вопрос, вариант.
Цикл: начало цикла для, конец цикла для, петля цикла.
Параллельность: параллельный процесс.
Не образуют маршрут: комментарий, правый, левый комментарий, формальные параметры.
И дополнительные элементы: ввод, вывод, пауза, период, пуск таймера, синхронизатор, полка, вставка.
Тогда грамматика языка - это несколько макроикон (4-х типов), и правил сочетания этих макроикон. Любая Дракон-схема, которая не может быть представлена иерархической совокупностью такого набора - считается синтаксический некорректной (разумеется, только в рамках выделенного таким образом подмножества языка Дракон, реализующего минимальный маршрутный язык согласно теореме Дейкстры о структурном представлении, расширенной до класса параллельных алгоритмов FORK/JOIN-исчисления).
2. Верификация маршрутной логики
Для обычного алгоритма маршрут - это граф, для параллельного придется вводить 2 типа вершин: в одних исходящие дуги будут трактоваться как выбор (один из..), в других - как разветвление (все сразу...). Вообще, верификация - это проверка системы на соответствие некому эталону. Для маршрутной модели эталон можно задать (например, с использованием темпоральной логики). Но если эталона нет, что можно верифицировать?
Возьмем за основу сети Петри. Если мы превратили маршрутную модель программы в сеть Петри и запустили ее симуляцию, могут произойти различного рода ошибки, отражающие ошибки маршрутной модели. Например, недостижимые позиции. Как я понимаю, само наличие недостижимого элемента в маршрутном графе является ошибкой его (графа) проектирования. Еще есть тупиковые маркировки, неограниченность позиций и др., но чтобы говорить о смысле этих ошибок, нужна доработка теории связки сетей с алгоритмами.
|