Ввести иерархическую детализацию отдельно взятой схемы "областным методом" на всё более формальном языке, как
в 5-м техтребовании от меня. При этом, возможно, следует ограничиться двумя уровнями - неформальный язык (в иконах - свободный текст) и формальный язык (в иконах - прогтекст на выбранном прогязыке). При этом для начала формальный язык выбрать единственный и для него сделать корректную трансляцию в прогтекст (с учётом отдельно визуализированной структуры программы).
Впоследствии трансляция должна учитывать и визуализацию межпрограммного конструктива (когда будет определён его язык), если вхождение данной программы в таковой определено.
P.S. Ознакомился с книгой Карпова по Model Checking (анонсированной
в этом сообщении) . Конечно, требует хорошей математической подготовки для полного понимания, но кое-какие изменения и дополнения в приложении техноязыка очевидны.
В частности, оправдано использовать в вышеуказанной иерархии как один из языков спецификации (уже формальный, но ещё не программирования) гибрид со входным языком системы симулирования-верификации (напр. ДРАКОН-Promela).
NB. Так мы, кстати, выходим на внешнюю симуляцию исполнения дракон-модели и не нужно её реализовать внутри РДП-среды. Ведь симуляция нам и нужна для тестирования алгоструктуры - а тут она уже интегрирована с верификацией, да ещё и в некоторых случаях всё это доступно бесплатно.Естественно, как результат трансляции должен идти текст на этом входном языке в формате ModelChecking-системы.
В стандарте Promela опять видим цикл Дейкстры в качестве единственной циклической алгоструктуры, что не проблема а наоборот - ведь это "универсальная программа", и мы можем, в частности, реализовать в ЦД по переменной
ИмяВетки и силуэт, как писал
при обсуждении ЦД в этом подпункте. Собственно, это качественный подход к теореме, что любой силуэт м.б. представлен как цикл Дейкстры по переменной
ИмяВетки.
![Smile :)](./images/smilies/icon_smile.gif)
Возможны два подхода к поддержанию соответствия "ЦД-силуэт" в РДП-редакторе:
* сочинять спецификацию-силуэт как ЦД от веточной переменной, а в редакторе заложить преобразование в силуэт при детализации;
* сочинять всегда как силуэт, а для конкретного языка спецификации в редакторе преобразовывать в ЦД-текст (от автоматически вводимой переменной-имени ветки).
Второй подход считаю более логичным и естественным для сочинителя, пользующегося техноязыком. Возможно, язык типа Promela подойдёт и как язык представления межпрограммных конструктивов.
К чему всё это говорится именно здесь? А к тому, что верифицированную спецификацию мы далее детализируем на гибридном прогязыке.
Очень важно, что техноязык может использоваться в формализации знаний с самого начала, когда деятельность представлена как организационные процессы. На с. 260 приведено справедливое замечание разработчиков одной из систем их визуализации, что "формулы логики... также являются слишком сложными для использования менеджерами". Не знаю, что за формы они сделали для упрощения спецификации этих формул (м.б. редактор LTL-формул с контекстными подсказками), но можно приложить ДРАКОН также и здесь. Нужно визуализировать в РДП-среде формулы используемой для верификации темпоральной логики (возможно - каждой из множества *TL). Имеется в виду представление формулы как never-процесса. Соответственно описание транслируется в текст процесса для ModelChecking-системы.
Конечно, для каждого формального языка должна поддерживаться нормальная авторетрансляция текста из файла трансляции (возможно, обработанного внешними приложениями - той же ModelChecking-системой) в визуал (дракон-модель).
Конечно, для каждого формального языка должна поддерживаться нормальная авторетрансляция текста в визуал (дракон-модель).