Методы и средства инженерии программного обеспечения
утверждение Аend запишем как конъюнкции
Выходное утверждение Аend запишем как конъюнкции таких условий:
(а) (Т– массив целых ) & (Т' – массив целых )
(б) ( " i если i £ N то $ j (T'( i ) £ T' ( j )))
(в) ( " i если i < N
то (T' ( i ) £ T' ( i+1) ),
то есть Аend – это (Т – массив целых ) & (Т'
– массив целых ) & " i если i £ N то $ j (T'( i ) £ T' ( j )) & " i если i < N то (T' ( i ) £ T' ( i+1) ).
Для расположения элементов массива Т в порядке возрастания их величин в массиве Т’ в используется алгоритм пузырьковой сортировки, суть которого заключается в предварительном копировании массив Т в массив Т', а затем проводится сортировка элементов согласно условия их возрастания. Алгоритм сортировки представлен на блок–схеме (рис.7.1).
Операторы алгоритма размещены в прямоугольниках. Условия, с помощью которых происходит выбор альтернативных путей в алгоритме, представлен в параллелограммах. Кружками отмечены точки с начальным Abeg конечным условиями Aend и состояниями алгоритма: кружок с нулем обозначает начальное состояние, кружок с одной звездочкой – состояние после обмена местами двух соседних элементов в массиве Т', кружок с двумя звездочками обозначает состояние после обмена местами всех пар за один проход массива Т'.
Кроме уже известных переменных Т, T' и N, в алгоритме использованы еще два переменные: i – типа целая и М – булева, значением которой являются логические константы true и false.
2. Для доказательства того, что алгоритм действительно обеспечивает выполнение исходных условий, рассмотрим динамику выполнения этих условий последовательно в определенных точках алгоритма. Заметим, что указанные точки делят алгоритм на соответствующие части, правильность любой из которых обосновывается в отдельности.
Так оператор присваивания означает, что для всех i (i £ N & i>0 ) выполняется (T' [i] : = T [i]). Результат выполнения алгоритма в точке с нулем может быть выражен утверждением:
