Главная Промышленная автоматика.

Код процедуры siftup с утверждениями

procedure siftup (i,n); value i,n; integer i,n; begin real copy; integer j; comment

1.1: l:io=inpa3Mep массива 1.2: A(io+l) 1.3: M=p(Mo); copy:=M.p]; loop: j:=2Xi; comment 3.1: in 3.2: 2i=j

3.3: i = io или i2io 3.4: M=p(Mo) при Miil=copy 3.5: A(io) или (i=io и A(io+l)) 3.6: MIi-4-2]>copy или i=io 3.7: Mfi4-2]M[i] или i=io; if jn tlien begin if j<n tlien begin if MO+ll>M[j] then j:=i+l end; comment 6.1: i=j-T-2 6.2: 2ijn 6.3: i=io или i>2io 6.4: M=p(Mo) при M[i]:=copy 6.5: A(io) или (i=io и A(io+l)) 6.6: MlIi-4-2]>copy или i==io 6.7: M[i4-2]>Mi] или i = io 6.8: (2i<n и M[i]=max(M[2i], M[2i + 1])) или

(2i=n и M[j]=Ml[n]) 6.9: MpJMIi] или i=.io; if MU]>copy then begin Мр]:=М[]]; comment

8.1: i = io или i2io 8.2: 2i=jn

8.3: M0-4-2]=M[i]=MIj]>copy 8.4: Mfi4-2]Mlj] или i=io 8.5: M=p(Mo) при MIj]=copy 8.6: A(io)3 i:=r, comment

8.7: i>2io

8.8: i=i=n

8.9: M[i-b2]>copy

8.10: Mti-i-2]M[i]

8.11: M=p{Mo) при Mil]:=copy

8.12: A(io); go to loop end



comment

9.1: Mlj]:copy, если пришли от строки 7, или 2i=j>n, если пришли от 4;

10 МИ:=сору;

comment

ШЛ: М=р(Мо) 10.2: A(io);

11 end siftup;

Обоснование утверждений процедуры siftup

Справедливость вышеуказанных утверждений основывается на следующих соображениях.

1.1-1.2: Утверждения, необходимые для вьшолнения процедуры siftup. 1.3:"здесь р - это тождественная перестановка. 3.1-3.7: Если пришли от строки 2, то

3.1: 1.1.

3.2: 3.

3.3, 3.5-3.7: i=io по 1.1. 3.5 требует и 1.2. 3.4: 1.3 и 2.

Если же пришли от строки 8, то соответственно 8.8, 3, 8.7, 8.11, 8.12, 8.9 и 8.10. 6.1: В 3.2 j=2i, а по 6Ь j может быть равно 2i-f-l. В обоих случаях i=j-b2.

6.2: После 4 jn. На участке от 3.1 до 6.2 j меняется только в 6Ь.

Перед 6Ь ]<п согласно 5. Следовательно в 6.2 jn. 2ij по 6.1. 6.3-6.7: 3.3-3.7 соответственно.

6.8: Если 4 есть true, а 5 - false, то j=2i=n (согласно 3.2), так что второй пункт утверждения 6.8 выполняется.

Если 4 - true и 5 - true, то в 6а 2i=j"<n (согласно 3.2), так что равенство

Mj-f l]=Mf2i-f 1] установлено. Теперь в 6.8 j=2i или j=2i-f 1. В любом случае

по 6а и 6Ь первый пункт утверждения 6.8 выполняется. 6.9: По 6.5 i¥=iD дает A(io). 2io:2i:jn по 6.3 и 6.2.

Следовательно, A(io) и 6.1 дают Mtil=Milj-r-2]M[j]. 8.1: 6.3. 8.2: 6.2.

8.3: i=j-b2 по 6.1, M[i]=MiIj] по 8а и МП>сору по 7. 8.4: 6.7 и 6.9.

8.5: 6.4 требует, чтобы значение M{i] было заменено значением сору. Поскольку (согласно 8а) M[i]=Mi[j], то М {]] может с таким же успехом быть заменено на сору.

8.1 и 8.2 дают ioin, так что изменение массива М в 8а производится внутри сегмента от Мро] до Мп].

8.6: Согласно 8а и если выполняется 6.8 (первый пункт), то M[i]MI2i] и Mfi] M[2i-f 1]. Согласно 8а и если выполняется 6.8 (второй пункт), то iM!H]=M[j]= =М[п]=ЛЦ21], и для данного вызова процедуры siftup M2i-f-l] не существует. В 6.5 A(io-bl) выполняется, поскольку A(io) включает в себя и A(io-bl). Если i=io, то выполнение A(io-bl) и вышеуказанные соотношения для М{1] дают выполнение A(io). Если i¥=,io. то 8а, 8.4, выполнение A(io) в 6.5 и вышеуказанные соотношения для Мр] дают выполнение A(io) в 8.6.

8.7: 8Ь, 8.1 и 8.2.

S.8: 8Ь и 8.2.



8.9: 8b и 8.3.

8.10: В 8.6 2io]"n по 8.1 и 8.2. Следовательно, по 8.6

MIj-i-2]MIj]. Для соотношения Mlj-b2]M[j] используется 8Ь. 8.11: 8Ь и 8.5. 8.12: 8.6.

Э.1: В 9.1 приходим только, если 7 есть false или если 4 есть false. 2i=j по 3.2.

Л0.1-10.2: Если пришли от 7, то

10.1: 6.4 и 10. (6.2 и 6.3 дают ioiin, обеспечивая то, что изменение массива М в 10 будет происходить внутри сегмента от Щ1о] до Min].) 10.2: Согласно 10, 9.1, 6.2 и 6.8 MIi]=copyM[j]MI2i]

и если MI2i+l] существует, то MIj]>M[2i+l]. Если i=io, то выполнение 10.2 следует так же, как и в утверждении 8.6. Если же iic, то 6.6 и 10 дают М[1ч-2]>сору==М{1]. Теперь выполнение A(io) в 6.5 дает выполнение A(io) и в 10.2.

Если пришли ог 4, то 10.1: 3.4 и 10. (3.1 и 3.3 дают ioin)

ilO.2: 2i>n означает, что в A(io) нет соотношений, имеющих форму М{1]... Если i=io, то 3.5 дает 10.2. Если же 1фо, то 3.6 и 10 дают MIi-2]>copy=MIi]. Теперь A(io) в 3.5 дает 10.2.

Код тела процедуры TREESORT 3 с утверждениями

О integer i; comment

0.1: A(n-f-2+l); 1 for i: = n-H2 step -1 until 2 do .2 begin

comment 2.1: A(i+1)

2.2: Условия для процедуры siftup. выполняются;

3 siftup (i,n); comment

3.1: A(i);

4 end; comment

4.1: M[p]M[p+l] для n+lpn-1 4.2: A(2), T. e. MfkH-2]M[k] для 4=k=n;

5 for i: = n step -1 until 2 do S begin

comment

6.1: M[p]MIp+l] для i+Kp=n-1 6.2.: М[кн-21М1к] для 4=ki 6.3: M{i-f l]M[r] для 1 ri 6.4: Условия для процедуры siftup выполняются; 7 siftup(l,i);

comment

7.1: M[p]M[p-l-l] для i+lpn-1 7.2: Mfk-2]M[k] для 2=ki 7.3: MIl]M[r] для 2:r=i 7.4: Mli+1]M[1]; 8 exchange (MflLMffl);

comment





0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 [40] 41 42 43

0.0017