ПРОЕКТИРОВАНИЕ И ДЕКОМПОЗИЦИЯ ДВУНАПРАВЛЕННЫХ ПОТОКОВ ДАННЫХ ИНТЕРАКТИВНЫХ СИСТЕМ

А.Г. ПИСКУНОВ 10 июня 2006 г.

В работе рассматривается применение языка спецификаций RAISE (RSL) для анализа и декомпозиции двунаправленных потоков данных интерактивных систем.

Будем считать, что любой алгоритм, и, как следствие, любой компьютер, любая информационная система, любое приложение, любая программа, любой скрипт и т.д., написанные на любом множестве любых языков программирования есть

•частично-рекурсивная функция (согласно тезису Черча - Клини [3,

1.6, 2.5])

•или конечным автоматом (согласно тезису Поста [12, приложение 1] [5, стр. 74]);

Также будем считать, что любой тип данных DATA можно представлять как конечное прямое произведение множества натуральных чисел Zn[3, .24].

Далее, как показано в схеме FM, условимся что

•слово данные обозначает некоторое значение типа DATA;

•функция выхода OUTF : функция которая отображает данные и оператор в данные;

•функция перехода GOF : функция, которая отображает данные и оператор в номер оператора;

•оператор STATE : пара (функция выхода, функция перехода);

•программа: последовательность операторов STATE-list;

•шаг вычисления: пара (данные, порядковый номер оператора в программе);

•вычислительный процессом COMP: список шагов вычисления;

• приложение: рекурсивная функция fvm (finite virtual mashine), которая кортеж (программа, данные, номер оператора в программе, момент времени) отображает в вычислительный процесс;

-- Start of Scheme

scheme FVM = class

DATA,--data

TIME = Nat,

Z = { n : Nat • n > 0 } ,--state number

COMP = (DATA x Z)w ,--computation

OUTF = DATA x STATE DATA,--output function

GOF = DATA x STATE Z,--goto function

STATE = OUTF x GOF,--state

PRG = STATE*--programm

- - finite virtual machine fvm : PRG x DATA COMP fvm(p, d) = fvm(p, d, 1, 0),

fvm : PRG x DATA x Z x TIME COMP fvm(prg, data, sNo, t) = let stt = prg(sNo), (outf, go) = stt in ( (data, sNo)} Л

fvm(prg, outf(data, stt), go(data, stt), t + 1) end

-- End Of Scheme Далее, под

•потоком данных будем понимать последовательность изменения данных DATA-list и функцию df, которая его строит из вычислительного процесса;

•потоком управления будем понимать последовательность операторов (или номеров операторов в программе) и функцию sf, которая его строит из вычислительного процесса;

•подпотоком управления - последовательность на выходе функции sbrf.

-- Start of Scheme

- - . n

rsl/FVM

scheme FLOW = extend FVM with class value

df : COMP - DATA"--data flow

df(c) EE ( d (d, i) in c) ,

sf : COMP - Z"--state flow

sf(c) E ( i (d, i) in c) ,

sf : COMP x PRG - STATE"

sf(c, prg) E ( prg(i) (d, i) in c) ,

sbrf : STATE" x Z x Z - STATE" sbrf(sl, st) E

s in sub • let i : Z • 1 < i in

STATE" Z Z

sbrf(sl, st, le) E

s in sub •

let i : Z 1 < i Л i < le in

sub(i) = sl(st + i - 1)

sub(i) = sl(st + i

End Of Scheme

Программа p: PRG называется определенной в точке d: DATE, если длина вычислительно процесса не конечна: len fvm(p, d) is chaos. Множество всех точек Delta: PRG -> DATE-set, на которых программа p определена,