Оператор присваивания. Пусть P- спецификация , x - программная
переменная и e- выражение , не содержащее штрихованных переменных
(т.е. переменных x',y'). Тогда выражение x:=e;P является спецификацией
программной конструкции , которая сначала присваивает переменной x
значение выражения e , затем выполняется в соответствии со
спецификацией P . Пусть (ex -> P) обозначает выражение , получаемое
из P путем замены всех свободных вхождений переменной x на e и
De -область определения выражения e . Тогда :
x:=e;P =df ù ( De)Ú (ex -> P)
Примеры:
1) x:=x+y;IDENT = (x'=x+1&y'=y) ;
2) (y:=y/x; (x:=x+y;IDENT)) = (x=0) Ú ( x'=x+y/x & y'=y/x )
Условный оператор. Пусть P и Q -спецификации и b - логическое
выражение , не содержащее штрихованных переменных . Тогда
выражение if b then P else Q является спецификацией программной конструкции , которая выполняется как P , если b -истинно , и как Q - в противном случае . Пусть Db -область определения выражения b . Тогда :
if b then P else Q=df ù ( Db)Ú (b&P) Ú (ù b&Q)
Последовательная композиция. Пусть P - спецификация , содержащая переменную p , значением которой может быть любая допустимая спецификация . Тогда , если Q - некоторая спецификация , определим выражение (Qp ->>P) как соотношение , получаемое заменой всех
вхождений переменной p на Q в выражении P. Содержательно точки
вхождения переменной p в этом случае можно рассматривать как вызов
процедуры или функции со спецификацией Q . Важно отметить , что
данная операция подстановки (Qp ->>P) имеет более высокий приоритет,
нежели операция подстановки (ex -> P) , то есть в любом случае :
Qp ->>( ex -> P)= (ex ->( Qp ->> P)) .
Выделим специальную переменную SKIP для обозначения успешного завершения программной конструкции .
Пусть P и Q - некоторые специФикации, тогда последовательную композицию можно определить следующим образом :
P;Q =df QSKIP->>P .
Содержательно , выражение P;Q определяет программную конструкцию,
которая выполняется в соответствии со спецификацией P ,
и после успешного завершения конструкции P выполняется в
соответствии со спецификацией Q . Например , в конструкции y:=y/x ;
Q переход на выполнение Q может осуществиться только при x¹ 0 .
Примеры:
1) if b then P = if b then P else SKIP
2) SKIP;P=P;SKIP=P
.
Оператор цикла "while" . Спецификацию циклического оператора
определим рекурсивным образом :
while b do P=df if b then(P; while b do P) else SKIP ,
где b -логическое выражение , а P - спецификация тела цикла .
Использование аппарата спецификаций оказывается более
эффективным , если , кроме описания семантики программ , имеется возможностьисследования их свойств . Исследование свойств программ
может быть сделано на основе алгебраических соотношений ,
использование которых обеспечивает возможность эффективного и обоснованного перехода от спецификаций к соответствующим
программным конструкциям.
В исследовании свойств программ одним из важных аспектов является
семантическая эквивалентность программных конструкций.
Программные конструкции являются эквивалентными , тогда и только
тогда , когда их соответствующие спецификации - эквивалентны.
В данном случае мы рассматриваем логические спецификации , а для логических выражений понятие эквивалентности определено.
С содержательной точки зрения программы являются эквивалентными ,
если они предназначены для решения одной и той же задачи.
Примеры соотношений:
1) Db => (if b then P else P) = P ;
2) if b then P else Q = if ù b then Q else P ;
3) x:=e ; if b then P else Q = IF ( ex -> b) then ( x:=e ; P) else ( x:=e ; Q) ;
4) SKIP;P=P;SKIP=P ;
5) P; (Q ; R) = (P; Q) ; R
Доказательства перечисленных выше свойств могут быть проделаны на
основе свойств исчисления предикатов (правил вывода ) и
вышеприведенных определений спецификаций программных конструкций .
Ниже приводится перечень классических соотношений из
математической логики , являющихся полезными с точки зрения доказательства свойств :
1) P & P - P ;
2) ( P Ú Q ) - ù (ù P & ù Q) ;
3) ( P & Q ) - ù (ù P Ú ù Q) ;
4) (P & Q) - (Q & P) ;
5) (P Ú Q) - (Q Ú P) ;
6) ù (ù P ) - P ;
7) (P Ú ( Q &R ) ) - (P Ú Q ) & (P Ú R) ;
8) (P & ( Q Ú R ) ) - (P & Q ) Ú (P & R) ;
9) ( P - Q ) - ( P => Q ) & ( Q=>P ) ;
10) P Ú TRUE - TRUE ;
11) P & TRUE - P ;
12) P Ú FALSE - P ;
13) P & FALSE - FALSE ;
14) ù ( TRUE ) - FALSE ;
15) ù ( FALSE ) - TRUE ;
Пример доказательства .
Доказать :
if b then P else Q = if ù b then Q else P .
Доказательство :
if b then P else Q =
=ù ( Db)Ú (b&P) Ú (ù b&Q)= (по определению)
=ù ( Db )Ú (ù b&Q ) Ú (b&P))= ( коммутативность)
= if ù b then Q else P (по определению)
2.5. Системы параллельного программирования.Теория
взаимодействующих процессов и ее использование для спецификации
и анализа параллельных процессов .
Появление систем параллельных вычислений было вызвано
необходимостью существенного увеличения скорости компьютерного решения задач . Появление многопроцессорных вычислительных комплексов , компьютерных сетей и многозадачных операционных систем , основанных на концепции мультипрограммирования , обеспечили реальную базу для практической реализации параллельных вычислений .Содержательно , идея параллельного программирования сводится к декомпозиции проблемы на несколько подзадач, которые выполняются одновременно. Средства связи между параллельно решаемыми задачами , предусматривающие взаимодействие между соответствующими процессами , обеспечивают кооперативное решение проблемы. Существуют разные модели параллелизма , но наиболее распостраненными являются так называемая конвейерная модель и модели параллелизма данных, основанные на одновременном применение одних и тех же операций к различным частям структуры данных . В настоящее время средства параллельного программирования практически встроены в большинство объектно- ориентированных систем управления базами данных. Задача разработки программных средств , обеспечивающих параллельное выполнение процессов , представляется достаточно сложной и поэтому требует построения адекватных математических моделей , позволяющих всесторонне исследовать природу параллельных процессов с целью принятия правильных решений по разработке и реализации алгоримов параллельных вычислений . К настоящему времени сформировалось множество разных подходов к выбору математического аппарата для исследования параллельных процессов. Один из наиболее интересных подходов , сочетающий математическую строгость и адекватность практической реализации , представляет теория взаимодействующих процессов CSP ( Communicating Sequential Processes ) [5].
Теория базируется на следующих ниже понятиях .
Событие - спецификация существенного факта , имеющего положение
в пространстве и во времени. С точки зрения теории автоматов событие- - это возникновение стимула , который может активизировать переход из одного состояния в другое . Событие является атомарным
(неразложимым понятием) теории CSP. Примерами событий могут быть
возникновение какой либо ошибки в процессе выполнении программ , выполнение определенного запланированного условия , выбор элемента меню , активация командной кнопки , нажатие функциональной клавиши и т.п. . Каждое событие кодируется определенным символом. Множество символов , определяющее все события , в которых некоторый процесс может участвовать , определяет алфавит процесса .
След (трасса) - последовательность событий , определяющая один из возможных путей поведения некоторого процесса , начиная с начала
выполнения процесса до определенного фиксированного момента времени.
Процесс определяется множеством следов в некотором фиксированном алфавите .
Теория CSP позволяет создавать модели параллельно выполняемых взаимодействующих процессов с целью исследования свойств
процессов . Результаты этих исследований могут оказаться полезными для принятия обоснованных решений на последующих стадиях разработки и реализации соответствующего программного продукта.
В данном пособии рассматривается усеченный вариант теории CSP , включающий теоретико - множественную и процедурную модели.
2.5.1. Следы процессов.
Многие свойства процессов можно доказать , рассматривая соответ-ствующие свойства следов - последовательностей событий из
заданного алфавита A .
Пусть A * означает множество всевозможных следов в алфавите A . Пустой след обозначается как <> , а выражение ( c->s ) означает результат приписывания символа ( события ) c к следу s . Базисные свойства следов определяются следующими :
Ax1. <> Î A *
Ax2. ( c Î A ) & ( s Î A * ) - ( c->s ) Î A *
Ax3. ( c->s )= ( d-> t ) - c = d & s = t
Ax4. ( c->s ) ¹ <>
Ax5.( (<> Î S ) & (" cÎ A ." sÎ S . (c -> s) Î S)) => S Í A *
В дальнейшем будем буквами a, b, c, d обозначать события , буквами
s, t ,u, v - следы , буквами P ,Q, R, S ,T - процессы .
Например , s=< a,b,c,d > - обозначает след s , состоящий из событий
a,b,c,d ; ( c-> <>)= < c > ; ( a ->< b,c,d > ) = < a,b,c,d > .
Аксиома Ax5 обосновывает корректность применения метода
структурной индукции при доказательстве свойств следов . Ниже
приводится суть этого метода.
Пусть требуется доказать утверждение Y ( s, t ,u ,…) для любых s Î A * .
Доказательство строится из следующих шагов (индукция по длине
cледа s) .
B(базис индукции) . Доказываем Y ( <>, t , u ,…) для всех t , u ,… .
I ( индукционная гипотеза ) . Предполагаем , что Y ( s, t ,u ,…) истинно
для некоторого s Î A * и для всех t , u ,… .
S (шаг индукции) . Доказываем Y ( c->s, t , u ,…) для всех сÎ A .