Схема с разметкой: различия между версиями
Glk (обсуждение | вклад) (Создана новая страница размером '''Схема с разметкой''' (''Data flow analysis frameworks'') - модель (схемы) программы, ориенти...) |
(нет различий)
|
Версия от 12:55, 2 февраля 2010
Схема с разметкой (Data flow analysis frameworks) - модель (схемы) программы, ориентированная на извлечение свойств потока данных в программе (в схеме программы), --- решение задачи анализа свойств состояний.
С.ср. --- это пятерка [math]\displaystyle{ (G,L,F,M,a_0) }[/math], где [math]\displaystyle{ G }[/math] --- уграф; [math]\displaystyle{ L }[/math] --- полурешетка свойств --- множество пометок с отношением порядка [math]\displaystyle{ \sqsubseteq }[/math], не содержащее бесконечных цепей и являющееся полурешеткой с [math]\displaystyle{ 0 }[/math] и [math]\displaystyle{ 1 }[/math] относительно пересечения [math]\displaystyle{ \sqcap }[/math]; [math]\displaystyle{ F }[/math] --- множество так называемых преобразователей пометок (свойств), которое состоит из монотонных функций [math]\displaystyle{ f: L \rightarrow L }[/math] и является замкнутым относительно композиции функций и содержит тождественную функцию и для любого [math]\displaystyle{ a\in L }[/math] такую функцию [math]\displaystyle{ f \in F }[/math], что [math]\displaystyle{ a=f(0) }[/math]; [math]\displaystyle{ a_0\in L }[/math] --- начальная пометка; [math]\displaystyle{ M }[/math] --- функция, ставящая в соответствие каждой дуге [math]\displaystyle{ u }[/math] анализируемого уграфа [math]\displaystyle{ G }[/math] функцию эффекта дуги [math]\displaystyle{ M(u)\in F }[/math]. С.ср. хорошо определена, если существуют алгоритмы, позволяющие для любых [math]\displaystyle{ a,b\in L }[/math] и [math]\displaystyle{ f\in F }[/math] вычислять элементы [math]\displaystyle{ a\sqcap b }[/math] и [math]\displaystyle{ f(a) }[/math].
Другое название --- Схема свойств состояний.
См. также Задача анализа свойств состояний.
Литература
[Касьянов/88]