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