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


         

Доказательство очевидно, поскольку за семантикой


 

(T[1: N] – массив целых)   &  (T '[1: N] – массив целых)

 & ("i  если  i £ N  (T [ i] = T [ i] )).

Доказательство очевидно, поскольку за семантикой оператора присваивания, обеспечивающая поэлементную  пересылку чисел из Т в T’ , сами элементы при этом не изменяются и порядок их в Т і T'  одинаковый. Получили, что условие  (б) исходного утверждения выполнено. Первая строка доказанного утверждения совпадает с условием (а) исходного утверждения Аend  и остается справедливой до  конца работы алгоритма. В точке  алгоритма с одной звездочкой выполняется  оператор

(i < N) (T'( i)) > T' (i + 1) ® (T' ( i)  и   T' (i + 1)    для  изменения  местами элементов. 

В результате работы оператора будет справедливым такое утверждение:

$ i  если i < N  то  (T'(i) < T'(i +1),  которое  является   частью  условия   (в)  утверждения Аend

(для одной конкретной пары  смежных элементов массива T').

Очевидно, что семантика оператора обмена местами не нарушает условия (б) выходного утверждения Аend.

 

                                                                  

                                 Abeg                                           T = T’                                        0                         

                                                                                  M =true



                                                                                                 i = 0



                                                                                                  M=true                                 Aend                                        

                               

                                                                                         Ø M = true

                                                        ні    

                                                                                      i = i + 1


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