Пример 0

Здесь, по сути, одна мысль о результате была выражена на двух равно-мощных языках в том смысле, что конструкции одного могут быть автоматически сгенерированы исходя из конструкции другого.
Поэтому различие их типов - "программирования" или "спецификаций", - здесь считается условны.

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

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

Аналогично трём рассмотренным этапам усложнения можно представить и его три соответствующих стадии:

1	x=3;	(z=3,x=3)	H
2	switch (z) {   case 1:     x=1;     break;   case 2:     x=2;     break;   default:     x=3;     break; }	(z=1,x=1) (z=2,x=2) (z=3,x=3)	I
3	switch (z) {   case 1:     x=1;     x1=2;     break;   case 2:     x=2;     x1=2;     break;   case 2:     x=3;     x1=2;     break;   case 4:     x1=1;     break;   case 5:     x1=3;     break;   case 6:     x1=3;     break; }	(z=1,x=1,x1=2) (z=2,x=2,x1=2) (z=3,x=3,x1=2) (z=4,x1=1) (z=5,x1=3) (z=6,x1=3)	J

Для обозначения последовательного выполнения указанных фрагментов очевидно требуется некая связка "СЛЕДУЕТ".

Однако, для демонстрации сути данного подхода вполне достаточно употреблённой выше связки "И".

В этом случае:

J	G	K = J И G
(z=1,x=1,x1=2) (z=2,x=2,x1=2) (z=3,x=3,x1=2) (z=4,x1=1) (z=5,x1=3) (z=6,x1=3)	(x=1,x1=2,y=11,y1=31) (x=2,x1=2,y=12,y1=32) (x=3,x1=2,y=13,y1=33) (x=1,x1=1,y=21,y1=31) (x=2,x1=1,y=22,y1=32) (x=1,x1=3,y=21,y1=31) (x=2,x1=3,y=22,y1=32)	(z=1,x=1,x1=2,y=11,y1=31) (z=2,x=2,x1=2,y=12,y1=32) (z=3,x=3,x1=2,y=13,y1=33) (z=4,x=1,x1=1,y=21,y1=31) (z=4,x=2,x1=1,y=22,y1=32) (z=5,x=1,x1=3,y=21,y1=31) (z=5,x=2,x1=3,y=22,y1=32) (z=6,x=1,x1=3,y=21,y1=31) (z=6,x=2,x1=3,y=22,y1=32)

Пусть в приведённом ниже фрагменте произошла "описка" в отмеченном операторе - вместо "1" написано "11".

1	x=3;	(z=3,x=3)
2	switch (z) {   case 1:     x=1;     break;   case 2:     x=2;     break;   default:     x=3;     break; }	(z=1,x=1) (z=2,x=2) (z=3,x=3)
3	switch (z) {   case 1:     x=1;     x1=2;     break;   case 2:     x=2;     x1=2;     break;   case 3:     x=3;     x1=2;     break;   case 4:     x1=11;     break;   case 5:     x1=3;     break;   case 6:     x1=3;     break; }	(z=1,x=1,x1=2) (z=2,x=2,x1=2) (z=3,x=2,x1=2) (z=4,x1=11) (z=5,x1=3) (z=6,x1=3)	J*

Тогда:

J*	G	K* = J* И G
(z=1,x=1,x1=2) (z=2,x=2,x1=2) (z=3,x=3,x1=2) (z=4,x1=11) (z=5,x1=3) (z=6,x1=3)	(x=1,x1=2,y=11,y1=31) (x=2,x1=2,y=12,y1=32) (x=3,x1=2,y=13,y1=33) (x=1,x1=11,x1=1,y=21,y1=31) (x=2,x1=11,x1=1,y=22,y1=32) (x=1,x1=3,y=21,y1=31) (x=2,x1=3,y=22,y1=32)	(z=1,x=1,x1=2,y=11,y1=31) (z=2,x=2,x1=2,y=12,y1=32) (z=3,x=3,x1=2,y=13,y1=33) (z=4,x=1,x1=11,x1=1,y=21,y1=31) (z=4,x=2,x1=11,x1=1,y=22,y1=32) (z=5,x=1,x1=3,y=21,y1=31) (z=5,x=2,x1=3,y=22,y1=32) (z=6,x=1,x1=3,y=21,y1=31) (z=6,x=2,x1=3,y=22,y1=32)

То есть, становится недостижим сооветствующий оператор фрагмента G:

J*	G	K*
switch (z) {   case 1:     x=1;     x1=2;     break;   case 2:     x=2;     x1=2;     break;   case 3:     x=3;     x1=2;     break;   case 4:     x1=11;     break;   case 5:     x1=3;     break;   case 6:     x1=3;     break; }	if (x1 == 2) {   switch(x)   {     case 1:       y=11;       y1=31;       break;     case 2:       y=12;       y11=32;       break;     default:       y=13;       y1=33;       break;   } } else {   switch(x)   {     case 1:       y=21;       y1=31;       break;     case 2:       y=22;       y11=32;       break;   } }	(z=1,x=1,x1=2,y=11,y1=31) (z=2,x=2,x1=2,y=12,y1=32) (z=3,x=3,x1=2,y=13,y1=33) (z=4,x=1,x1=11,x1=1,y=21,y1=31) (z=4,x=2,x1=11,x1=1,y=22,y1=32) (z=5,x=1,x1=3,y=21,y1=31) (z=5,x=2,x1=3,y=22,y1=32) (z=6,x=1,x1=3,y=21,y1=31) (z=6,x=2,x1=3,y=22,y1=32)

Обычно трансляторы подобные ошибки не фиксируют.

Здесь самое место разобраться, почему это "ошибка".

В предлагаемом подходе это так потому, что не должно "пропадать" или "портиться" знание, зафиксированное как в "конструкции", так и в "поведении".

В приведённом выше примере ведь сам оператор "case 1:" никуда не делся, но он оказался недостижим в потоке управления, то есть его наличие в конструкции неявно предполагает и соответствующее поведение в полном процессе, чего нет на самом деле.

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

За основу рассуждений здесь взята "алгебра" с двумя частичными, то есть не всюду определёнными, операциями - И и ЛИБО.

Листьям дерева соответствуют простейшие процессы, узлам - указанные операции объединения, само дерево - это конструкция, а приписываемые узлам результаты применения операций - это и есть поведение.

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

В приведённом примере именно это условие не выполняется - не существует состояния, которое одновременно служит прообразом как для (z=4,x1=11), так и для (x=1,x1=1,y=21,y1=31) или (x=1,x1=1,y=22,y1=32) - всё дело в наличии двух противоречащих друг другу требований - x1=11 и x1=1.

То есть, здесь переменная может принимать в некоторый момент лишь одно значение.

А это и есть одно из условий, делающих операции объединения частичными - синтезированный процесс должен содержать прообразы всех состояний объединяемых процессов.

Некорректность при развитии программы в процессе "синтеза" её фрагментов может возникать не только из-за "пропажи" состояний, но и из-за появления новых.

Для такого примера рассмотрим операцию деления, которая не определена, если делитель равен нулю.

Нормальное действие операции:

z = x / y	(x=2,y=1,z=2) (x=2,y=2,z=1) (x=6,y=2,z=3) (x=6,y=3,z=2)

Неважно, как были перед этим получены значения переменной y, но если в результате очередной доработки в подобном множестве появится 0, то программа очевидно станет "неправильной".

Назад Вперёд