12.3. Проектирование программ.

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

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

12.3.1. Корректность частей программы.

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

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

12.3.2. Условные присваивания как спецификации.

Условное присваивание обладает достаточной мощностью для выражения эффекта любой части CF Pascal программы. Условные присваивания одновременно служат двум назначениям в проектировании программ CF Pascal:

1. как компоненты высокоуровневого проекта

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

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

Условные присваивания могут быть описаны в любой удобной смеси CF Pascal, математики и обычного языка.

Например, процедура

PROCEDURE Sort2(VAR Ch1, Ch2: CHAR);

VAR

Temp: CHAR;

BEGIN

IF Ch1 > Ch2

THEN

BEGIN

Temp := Ch1;

Ch1 := Ch2;

Ch2 := Temp

END

END;

может быть выражена как проект:

PROCEDURE Sort2(VAR Ch1, Ch2: CHAR);

VAR

Temp: CHAR;

BEGIN

{(Ch1 > Ch2 -> Ch1, Ch2, Temp := Ch2, Ch1, Ch1) |

(Ch1 <= Ch2 -> )}

END;

или

PROCEDURE Sort2(VAR Ch1, Ch2: CHAR);

VAR

Temp: CHAR;

BEGIN

IF Ch1 > Ch2

THEN

{Ch1, Ch2, Temp := Ch2, Ch1, Ch1)}

END;

или даже

PROCEDURE Sort2(VAR Ch1, Ch2: CHAR);

VAR

Temp: CHAR;

BEGIN

IF {Ch1 <> min(Ch1, Ch2)}

THEN

{Ch1, Ch2 = Ch2, Ch1)}

END;