Методы алгоритмизации предметных областей (23.05.2011)

Автор: Новиков Федор Александрович

Наложим ограничение (f(F (Arg(f) ( ( & Res(f) ( ( & Arg(f) ( Res(f) = (). В таком случае пара <A, F> определяет модель предметной области. Поскольку здесь не используется вложенные отношения, а все атрибуты находятся на одном уровне, то такую модель уместно называть плоской.

Формулы теории называются предложениями вычислимости и имеют вид:

C(X, Y, [G]),

где X, Y ? A — множества имен атрибутов, а G = g1, …, gn — последовательность имен функций (gi(F, i(1..n). Неформально предложение вычислимости C(X, Y, [G]) означает, что Y может быть вычислено по X применением последовательности функций G.

В исчислении присутствует одна схема аксиом: C(X, Y, [ ]), где Y ( X, а [ ] — пустая последовательность (пустая абстрактная программа). Такие предложения вычислимости называются тривиальными. В данном фрагменте исчисления достаточно рассматривать схему C(X, X, [ ]) тривиальных предложений вычислимости.

Аксиомы исчисления (предметные — зависящие от предметной области) — это все формулы вида C(Arg(f), Res(f), [ f ]), где f(F. Предметные аксиомы иногда называют элементарными предложениями вычислимости. Введем следующее правило композиции:

C(X, Y, [G1]) & C(W, Z, [G2]) & W(Y ? C(X, Y(Z, [G1; G2]),

где G1; G2 — конкатенация двух последовательностей функций. Данное правило имеет простую интерпретацию: имея абстрактную программу, вычисляющую Y, и другую абстрактную программу, входы которой содержатся в Y, последовательным применением этих программ можно расширить множество вычисленных атрибутов. Правило композиции часто используют в форме правила элементарной композиции:

C(X, Y, [G]) & C(Arg(f), Res(f), [ f ]) & Arg(f)(Y ? C(X, Y(Res(f), [G; f]).

Задачей Q на модели предметной области <A, F> называется четверка

Q = <A, F, X, Y>,

где <A, F> — модель предметной области, X, Y ( A — множества имен входных и выходных атрибутов соответственно. Решением задачи Q = <A, F, X, Y> называется последовательность G=g1, …, gn, для которой

( U ( W (U(X & Y(W & C(U, W, [G]).

Неформально это означает следующее: при решении задачи могут быть использованы не все входные данные и могут быть вычислены ненужные результаты.

Теорема (О полноте правила элементарной композиции). Пусть G=g1, …, gn — решение задачи Q = <A, F, X, Y>. Тогда оно может быть получено применением правила элементарной композиции из предложения вычислимости C(X, X, [ ]).

Поиск вывода в данном исчислении несложен. Пусть дана задача <A, F, X, Y>. Выберем в качестве исходного предложения вычислимости C(X, X, [ ]) и будем наращивать программу при помощи правила элементарной композиции. Если на определённом шаге имеем C(X, Z, [G]) & Z(Y, то решение найдено. Если (f(F (Arg(f) ( Z & & Res(f) ( Z), то применяем правило элементарной композиции для функции f, получая новое предложение вычислимости. Если достигается состояние, в котором (f(F (Arg(f) ( Z ( Res(f) ( Z) & Z(Y, то решения поставленной задачи не существует.

Применение этой формальной теории на практике состоит в следующем. Алгоритм синтеза программы можно интерпретировать как алгоритм поиска вывода в построенном формальном исчислении. Действительно, задача синтеза трактуется как задача доказательства теоремы существования решения. Заметим, что аксиомы корректны в вычислительном смысле, а единственное правило вывода сохраняет корректность. Таким образом, если удается построить формальный вывод, то можно быть уверенным, что синтезированная абстрактная программа является корректной. Здесь необходимо еще раз вернуться к важному понятию «доверия» к программному фонду. Алгоритм синтеза не проверяет корректность заданного программного фонда. Таким образом, синтезированная программа корректна с точностью до корректности доверительного программного фонда.

В разделе 4.3 рассматривается вопрос об эффективных (не переборных) алгоритмах синтеза. Предлагается следующая структура данных — результат предобработки для представления модели <A, F> (рис. 13).

Рис. 13. Результат предобработки модели предметной области

В результате предобработки модели строится списочная структура из совершенно одинаковых ячеек, имеющих разный смысл. Каждая ячейка хранит четыре указателя (left, right, up, down), что позволяет ей быть элементом двух двусвязных списков одновременно. Модель имеет два входа: А — указатель на список атрибутов (белый цвет) и F — указатель на список связей (серый цвет). Каждая ячейка списка связей F содержит два указателя, поддерживающих двусвязный (но не кольцевой!) список связей, а также указатель на двусвязный список вхождений атрибутов в качестве аргументов связи (горизонтальная штриховка) и указатель на двусвязный список вхождений атрибутов в качестве результатов связи (вертикальная штриховка). Совершенно аналогично устроен список атрибутов A.

Эта списочная структура дает возможность проводить синтез очень эффективно — число шагов алгоритма не превосходит числа вхождений атрибутов в МПО.

Алгоритм 1. Линейный алгоритм синтеза программ на плоской модели

Вход: Модель предметной области, заданная парой указателей А и F, как на рис. 13, и условие задачи в виде множеств X, Y входных и выходных атрибутов, соответственно.

Выход: Список G функций, применение которых решает поставленную задачу.

proc Solve (A, F, X, Y): G

H := ( // применимые связи

G := [ ] // синтезируемая программа

Z := Y \ X // целевые атрибуты

for a(X do Process (a) end for

while U ? ( do

if H=( then return fail

end if

select g ( H

G = G + g

U = U \ g.right

for a ( g.right do

Process (a)

end for

end while

end proc


загрузка...