Теперь мы готовы к тому, чтобы дать формальную постановку задаче анализа потоков данных.
Пусть есть ограниченная полурешетка конечной высоты L, граф потока управления G и набор монотонных на L потоковых функций fv для каждой вершины v графа G.
Тогда решением задачи анализа потоков данных называется пара наименьших разметок before , after , являющихся решением системы уравнений (*), приведенной на слайде.
Неформально говоря, полурешетка L представляет собой множество потоковых фактов, разметка before описывает решение задачи анализа потоков данных до исполнения операторов в данной вершине графа, а разметка after - после. Решеточная операция описывает получение общей части нескольких решений. Систему уравнений можно интерпретировать следующим образом: для каждой вершины решением задачи до нее является общая часть решений всех предшественников данной вершины, а после нее - применение к этой общей части потоковой функции, ассоциированной с данной вершиной.