Схема с разметкой

Схема с разметкой (Data flow analysis frameworks) — модель (схемы) программы, ориентированная на извлечение свойств потока данных в программе (в схеме программы), — решение задачи анализа свойств состояний.

Схема с разметкой — это пятерка $\,(G,L,F,M,a_0)$ , где $\,G$ — уграф; $\,L$ — полурешетка свойств — множество пометок с отношением порядка $\sqsubseteq$ , не содержащее бесконечных цепей и являющееся полурешеткой с $\,0$ и $\,1$ относительно пересечения $\sqcap$ ; $\,F$ — множество так называемых преобразователей пометок (свойств), которое состоит из монотонных функций $f: L \rightarrow L$ и является замкнутым относительно композиции функций и содержит тождественную функцию и для любого $a\in L$ такую функцию $f \in F$ , что $\,a=f(0)$ ; $\,a_0\in L$ — начальная пометка; $\,M$ — функция, ставящая в соответствие каждой дуге $\,u$ анализируемого уграфа $\,G$ функцию эффекта дуги $M(u)\in F$ . Схема с разметкой хорошо определена, если существуют алгоритмы, позволяющие для любых $a,b\in L$ и $f\in F$ вычислять элементы $a\sqcap b$ и $\,f(a)$ .