Методы и средства инженерии программного обеспечения



         

 Модель формального доказательства конкретности программы - часть 2


Выходное  утверждение А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]).  Результат выполнения алгоритма  в точке с нулем может быть выражен утверждением:




Содержание  Назад  Вперед