Побудова семантичного терму програми

За допомогою методу математичної індукції за кількістю кроків циклу знайдемо F₃(F₂(d₁)) , враховуючи, що n≥ 0,а потім n<0. Розглянемо спочатку випадок n≥ 0.

Гіпотеза: при виконанні n кроків тіла циклу F₃(F₂(d₂)) = [M→m,N→n,R→m*n,A→m,B→0]

База: 0 крок: b=0 =>умова циклу не виконується ,маємо таке результуюче дане: [M→m, N→n, R→0, A→m, B→0] => R= m*n =0.Гіпотеза справджується.

Припущення: припустимо, що виконано t-1 кроків тіла циклу, тоді дані мають вигляд d*= [M→m, N→n, R→m*(t-1), A→m, B→n-t+1]. Покажемо, як зміняться дані після виконання ще одного кроку циклу :

F₃ (d*)= F₃ ([M→m, N→n, R→m*(t-1), A→m, B→n-t+1]) = [M→m, N→n, R→m*t, A→m, B→n-t]. Оскільки тіло циклу виконується, то S² (gr,B=>,0) = true, тобто b>0, n-t>0 => n>t, n>n-t+1 і виконується тіло циклу AS^R (S² (add,R=>,A=>)) • AS^B (S² (sub,B=>, )) ([M→m, N→n, R→m*(t-1), A→m, B→n-t+1]) = [M→m, N→n, R→m*(t-1), A→m, B→n-t+1] Ñ[R→ m*(t-1)+m; B→ n-t] = [M→m, N→n, R→m*t, A→m, B→n-t].При кількості кроків циклу t=n отримаємо результат [M→m N→,n, R→m*n, A→m, B→0].

Умова циклу S² (gr,B=>, ) = false.

Отже, гіпотезу доведено.

Тепер аналогічно розглянемо випадок, коли n<0.

Гіпотеза: при виконанні n кроків тіла циклу F₃(F₂(d₃)) =[ M→m, N→n, R→ (-m)*(-n), A→ -m, B→0]

База: 0 крок: b=0 => умова циклу не виконується ,маємо таке результуюче дане: [M→m, N→n, R→0, A→ -m, B→0] => R= (-m)*(-n) = 0. Гіпотеза справджується.

Припущення: припустимо, що виконано t-1 кроків тіла циклу, тоді дані мають вид d**= [M→m, N→n, R→-m*(t-1), A→ -m, B→ -n-t+1]. Покажемо, як зміняться дані після виконання ще одного кроку циклу :

F₃ (d**)= F₃ ([M→m, N→n, R→ (-m)*(t-1), A→ -m, B→ -n-t+1]) = [M→m, N→n, R→ (-m)*t, A→ -m, B→ -n-t]. Оскільки тіло циклу виконується, то S² (gr,B=>, ) = true, тобто b>0, n-t>0 => n>t, n>n-t+1 і виконується тіло циклу AS^R (S² (add,R=>,A=>)) • AS^B (S² (sub,B=>, )) ([M→m, N→n, R→ (-m)*(t-1), A→ -m, B→ -n-t+1]) = [M→m, N→n, R→ (-m)*(t-1), A→ -m, B→ -n-t+1] Ñ[R→ (-m)*(t-1)-m; B→ -n-t] = [M→m, N→n, R→ (-m)*t, A→ -m, B→ -n-t]. При кількості кроків циклу t=-n отримаємо результат [M→m, N→n, R→ (-m)*(-n), A→ -m, B→0].

Умова циклу S² (gr,B=>, ) = false.

Отже, гіпотезу доведено.

Обґрунтування повної коректності.

Покажемо, що при правильних вхідних даних програма завершується (зупиняється). Фактично, треба показати завершеність циклу F₃ , оскільки інші оператори не впливають на завершення програми. З часткової коректності видно, що за правильних вхідних даних перед виконанням циклу дані мають вигляд [M→m, N→n, R→0, A→m, B→n]. Після кожного виконання циклу R збільшується на m і b зменшується на 1. Отже,отримаємо спадну послідовність b і в силу її скінченності, якщо програма входить у цикл, то він завжди завершується. При інших варіантах правильних вхідних даних програма не заходить в цикл, а послідовно виконує прості оператори, тому програма завжди зупиняється в силу скінченності кількості операторів.

Завдання 1.4. За допомогою операцій віднімання і додавання розробити програму, яка обчислює результат ділення rez невід’ємного числа a на додатне число b та остачу від цього ділення – ost. Виконати:

1) побудувати програму для розв’язку задачі на мові SIPL,

2) побудувати дерево синтаксичного виводу програми,

3) побудувати композиційний семантичний терм програми,

4) довести коректність програми.

Розв’язок.

1) Програма для розв’язку задачі:

Begin

    rez:= 0;

    k:= 0;

    if (a = 0) then skip else[S5]

        if (a < b) then skip else[S6]

                  while k <= a – b do

                  begin

                            rez:= rez+1;

                            k:= k+b

              end;

ost:= a – k

End

2) Дерево синтаксичного виводу програми:

3) Семантичний композиційний терм:

sem_P(Program) = sem_P(Begin rez:= 0; k:= 0; if (a = 0) then skip else if (a < b) then skip else while k <= a – b do begin rez:= rez+1; k:= k+b end; ost:=a - k End)=

= sem_S(rez:= 0; k:= 0; if (a = 0) then skip else if (a < b) then skip else while k <= a – b do begin rez:= rez+1; k:= k+b end; ost:=a - k) =

= sem_S(rez:= 0)•sem_S(k:= 0; if (a = 0) then skip else if (a < b) then skip else while k <= a – b do begin rez:= rez+1; k:= k+b end; ost:=a - k)=

= sem_S(rez:= 0)•sem_S(k:= 0; if (a = 0) then skip else if (a < b) then skip else while k <= a – b do begin rez:= rez+1; k:= k+b end)•sem_S(ost:=a - k) =

= AS^rez(sem_A(0))•sem_S(k:= 0)•sem_S(if (a = 0) then skip else if (a < b) then skip else while k <= a – b do begin rez:= rez+1; k:= k+b end) •AS^ost(sem_A(a-k))=

= AS^rez( )• AS^k(sem_A(0))•IF(sem_B(a = 0), sem_S(skip), sem_S(if (a < b) then skip else while k <= a – b do begin rez:= rez+1; k:= k+b end))•AS^ost(S²(sub, sem_A(a), sem_A(k)))=

= AS^rez( )• AS^k( )• IF(sem_B(a = 0), sem_S(skip), sem_S(if (a < b) then skip else while k <= a – b do begin rez:= rez+1; k:= k+b end)) •AS^ost(S²(sub, a=>, k=>))=

= AS^rez( )• AS^k( )• IF(S²(eq, sem_A(a), sem_A(0)), id, IF(sem_B(a<b), sem_S(skip), sem_S(while k <= a – b do begin rez:= rez+1; k:= k+b end))) •AS^ost(S²(sub, a=>, k=>))=

= AS^rez( )• AS^k( )• IF(S²(eq, a=>, ), id, IF(S²(less, sem_A(a), sem_A(b)), id, WH(sem_B(k <= a - b), sem_S(begin rez:= rez+1; k:= k+b end)))) •AS^ost(S²(sub, a=>, k=>))=

= AS^rez( )• AS^k( )• IF(S²(eq, a=>, ), id, IF(S²(less, a=>, b=>), id, WH(S²(less, sem_A(k=>), sem_A(a-b)), sem_S(rez:= rez+1; k:= k+b)))) •AS^ost(S²(sub, a=>, k=>))=

= AS^rez( )• AS^k( )• IF(S²(eq, a=>, ), id, IF(S²(less, a=>, b=>), id, WH(S²(less, k=>, S²(sub, a=>, b=>)), sem_S(rez:= rez+1)•sem_S(k:= k+b)))) •AS^ost(S²(sub, a=>, k=>))=

= AS^rez( )• AS^k( )• IF(S²(eq, a=>, ), id, IF(S²(less, a=>, b=>), id, WH(S²(less, k=>, S²(sub, a=>, b=>)), AS^rez(sem_A(rez+1))•AS^k(sem_A(k+b))))) •AS^ost(S²(sub, a=>, k=>))=

= AS^rez( )• AS^k( )• IF(S²(eq, a=>, ), id, IF(S²(less, a=>, b=>), id, WH(S²(less, k=>, S²(sub, a=>, b=>)), AS^rez((S²(add, sem_A(rez), sem_A(1))))•AS^k(S²(add, sem_A(k), sem_A(b)))))) •AS^ost(S²(sub, a=>, k=>))=

= AS^rez( )• AS^k( )• IF(S²(eq, a=>, ), id, IF(S²(less, a=>, b=>), id, WH(S²(less, k=>, S²(sub, a=>, b=>)), AS^rez((S²(add, rez=>, )))•AS^k(S²(add, k=>, b=>))))) •AS^ost(S²(sub, a=>, k=>))

4) Доведення часткової коректності:

        Для скорочення запису будемо записувати дані у впорядкованому виді, тобто [a,b,rez,k,ost], замість [a→ , b→ , rez→ , k→ , ost → ].

Позначимо

F = AS^k( )• IF(S²(eq, a=>, ), id, IF(S²(less, a=>, b=>), id, WH(S²(less, k=>, S²(sub, a=>, b=>)), AS^rez((S²(add, rez=>, )))•AS^k(S²(add, k=>, b=>))))) •AS^ost(S²(sub, a=>, k=>)),

тоді маємо

sem_S([a,b,rez,k,ost])=F(AS^rez( ))([a,b,rez,k,ost])=F([a,b,rez,k,ost]Ñ[rez→0])=F([a,b,0,k,ost])

Позначимо

F₁ = IF(S²(eq, a=>, ), id, IF(S²(less, a=>, b=>), id, WH(S²(less, k=>, S²(sub, a=>, b=>)), AS^rez((S²(add, rez=>, )))•AS^k(S²(add, k=>, b=>))))) •AS^ost(S²(sub, a=>, k=>)).

Маємо

F = AS^k( )•F₁

F([a,b,0,k,ost]) =

F₁(AS^k( ))([a,b,0,k,ost])=F₁([a,b,0,k,ost]▼[k→0])= F₁([a,b,0,0,ost]).

F₁([a,b,0,0,ost]) =

IF(S²(eq, a=>, ), id, IF(S²(less, a=>, b=>), id, WH(S²(less, k=>, S²(sub, a=>, b=>)), AS^rez((S²(add, rez=>, ))) •AS^k(S²(add, k=>, b=>))))•AS^ost(S²(sub, a=>, k=>)) ([a,b,0,0,ost])=

AS^ost(S²(sub, a=>, k=>))(IF(S²(eq, a=>, ), id, IF(S²(less, a=>, b=>), id, WH(S²(less, k=>, S²(sub, a=>, b=>)), AS^rez((S²(add, rez=>, ))) •AS^k(S²(add, k=>, b=>)))))([a,b,0,0,ost])=

=     =

.

Позначимо

G = WH(S²(less, k=>, S²(sub, a=>, b=>)), AS^rez((S²(add, rez=>, ))) •AS^k(S²(add, k=>, b=>)))))

Маємо F₁([a,b,0,0,ost]) =

За допомогою методу математичної індукції за кількістю кроків циклу знайдемо, G([a,b,0,0,ost]), враховуючи, що a ≥ b і a ≠ 0 .

Гіпотеза: при виконанні n кроків тіла циклу G([a, b, 0, 0, ost]) =

База. 1 крок: G([a,b,0,0,ost]) = |(k < a-b)=true => k < a-b => 0 < a-b => b<a|=

=AS^rez( (S²(add, rez=>, ))) •AS^k(S²(add, k=>, b=>)))) ([a,b,0,0,ost])=AS^rez( (S²(add, , ))) •AS^k(S²(add, , b=>))=AS^rez( ) •AS^k(b=>)=[a,b,0,0,ost] Ñ[rez→1, k→b] = [a,b,1,b,ost]

Припущення: припустимо, що виконано t-1 кроків тіла циклу, тоді дані мають вид [a,b,t-1,b*(t-1),ost]. Покажемо, як зміняться дані після виконання ще одного кроку циклу :

G([a,b,t-1,b*(t-1),ost]) = [a,b,t,b*t,ost]. Оскільки тіло циклу виконується, то (less, k=>, S²(sub, a=>, b=>)) = true, тобто (k < a-b) = true, k < a-b, k = t-1, t-1 < a-b виконується тіло циклу AS^rez(S²(add, rez=>, )) •AS^k(S²(add, k=>, b=>))([a,b,t-1,b*(t-1),ost]) = [a,b,t-1,b*(t-1),ost] Ñ[rez→t; k→b*t] = [a,b,t,b*t,ost].

Отже, гіпотезу доведено.

Нехай G(d) зупиняється на даному : [a,b,n,b*n,ost], це значить, що умова циклу приймає значення false. Маємо : S²(less, b*n=>, (a=>)-(b=>)) = false => (b*n < a-b) = false => b*n≥a-b, враховуючи, що умова на n-1 кроі виконання циклу була істиною, маємо : b*n ≥a – b≥ b*(n-1) => b*(n+1)≥a≥b*n. Отже n – ціла частина від ділення a на b.

Маємо F₁([a,b,0,0,ost]) =

= = = =

= =

= =

=

Отже, ми показали часткову коректність програми при правильних вхідних даних (тобто a≥0 і b>0).

Обґрунтування повної коректності.

Покажемо, що при правильних вхідних даних програма завершується (зупиняється). Фактично, треба показати завершеність циклу G, оскільки інші оператори не впливають на завершення програми. З часткової коректності видно, що за правильних вхідних даних перед виконанням циклу дані мають вигляд [a,b,rez=0,k=0,ost], де a ≥ b, b > 0 і a ≠ 0. Після кожного виконання циклу k збільшується на b і k+b < a. Отже, в силу скінченності a і b, якщо програма входить у цикл, то він завжди завершується. При інших варіантах правильних вхідних даних програма не заходить в цикл, а послідовно виконує прості оператори, тому програма завжди зупиняється в силу скінченності кількості операторів.

Завдання 1.5. Розробити програму, яка обчислює значення N! за вхідним цілим N з використанням одного циклу. Виконати:

1) побудувати програму для розв’язку задачі на мові SIPL,

2) побудувати дерево синтаксичного виводу програми,

3) побудувати композиційний семантичний терм програми,

4) довести коректність програми.

Розв’язок.

1) Програма для розв’язку задачі:

     Begin

              If N<0 then R:=0 else

              begin

                        R:=1; M:=N;

                        while M>1 do begin R:=R*M; M:=M–1 end

              end

     End

     begin[S7]

              If N<0 then

                        R:=0

              else

              begin

                        R:=1;

                        while N>1 do

                        begin

                                 R:=R*N;

                                 N:=N–1

                        end

              end

     end

2) Дерево синтаксичного виводу програми:

3) Семантичний композиційний терм:

sem_P(Program) = sem_P(Begin If N<0  then R:=0 begin R:=1; M:=N; while M>1 do begin R:=R∙M; M:=M-1 end end end) = sem_S(If N<0 then R:=0 begin R:=1; M:=N; while M>1 do begin R:=R∙M; M:=M-1 end end) = IF(sem_B(N<0), sem_S(R:=0), sem_S(R:=1; M:=N while M>1 do begin R:=R∙M; M:=M-1 end) ) =IF(sem_B(N<0), sem_S(R:=0), sem_S(R:=1;M:=N) ◦ WH(sem_B(M>1), sem_S(R:=R∙M; M:=M-1) ) )= IF(sem_B(N<0), sem_S(R:=0), sem_S(R:=1) ◦ sem_S(M:=N) ◦ WH(sem_B(M>1), sem_S(R:=R∙M) ◦ sem_S( M:=M-1) ) )=

IF(S² (less, sem_A(N), sem_A(0)), AS^R(sem_A(0)), AS^R(sem_A(1)) ◦ AS^M(sem_A(N))  ◦ WH(S² (gr, sem_A(M), sem_A(1)), AS^R(sem_A(R∙M)) ◦ AS^M(sem_A(M-1)) ) ) =IF(S² (less, N=>, ), AS^R( ), AS^R( ) ◦ AS^M(N=>) ◦ WH(S² (gr, M=>, ), AS^R(S²(mult, sem_A(R), sem_A(M))) ◦ AS^M(S²(sub, sem_A(M), sem_A( ))) ) ) =IF(S² (less, N=>, ), AS^R( ), AS^R( ) ◦ AS^M(N=>) ◦ WH(S² (gr, M=>, ), AS^R(S²(mult, R=>,M=>)) ◦ AS^M(S²(sub, M=>, )) ) )

4) Доведення часткової коректності.

Нехай маємо дані d=[N->n]. Доведемо, що на них програма працює правильно, тобто що при завершенні обчислень отримується очікуваний результат:

F=IF(S² (less, N=>, ), AS^R( ), AS^R( ) ◦ AS^M(N=>) ◦ WH(S² (gr, M=>, ), AS^R(S²(mult, R=>,M=>)) ◦ AS^M(S²(sub, M=>, )) ) )

F₁= AS^R( );

F₂=AS^M(N=>);

F₃= WH(S² (gr, M=>, ), AS^R(S²(mult, R=>,M=>)) ◦ AS^M(S²(sub, M=>, )));

F₄=AS^R( );

F₅=AS^R(S²(mult, R=>,M=>));

F₆= AS^M(S²(sub, M=>, ));

1) нехай n<0

Sem_p(F)(d)= =F₄(d)=F₄(d▼[R->0]) =

= F₄(d▼[R->0]) = dr = [N->n, R->0] ;

факторіал для від’ємних чисел не існує і результат дорівнює нулю (помилка у ввідних даних).

2) нехай n≥0

Sem_p(F)(d)= = F₃(F₂(F₁(d))) =

= F₃(F₂(d▼[R->1]) = F₃(F₂([N->n,R->1]) =  =

= F₃(d₁▼ [M->N=>(d₁)]) = F₃(d₁▼ [M->n]) =  =

= F₃(d₂);

Далі за допомогою методу математичної індукції за кількістю кроків циклу знайдемо F₃(d₂), враховуючи, що n≥ 1, а потім n<1. Нехай спочатку n≥ 1.

Гіпотеза: при виконанні n кроків тіла циклу F₃(d₂)=[ ]

База: Нульовий крок: При m=0 умова циклу не виконується, маємо таке результуюче дане: [ ] => R= p*m! = p. Гіпотеза справджується.

Припущення: припустимо, що виконано t-1 кроків тіла циклу, тоді дані мають вид dw= [N->n,R->p,M->t-1]. Покажемо, як зміняться дані після виконання ще одного кроку циклу:

F₃ (dw)= F₃ ([N->n,R->p,M->t]) = ;

При t=0:

F₃ (dw) = F₃ ([N->n,R->p,M->0])= [N->n,R->p,M->0];

dr = [N->n,R->p∙0!,M->0] = dw; гіпотеза справджується.

При t>0:      

F₃ (dw) = F₅ ◦ F₆ ◦ F₃(dw) =  = F₃(dd) =

=  =  = dq = dr;

=> F₃(dw) =

Отже, гіпотезу доведено.

Обчислення завершене. Результат поміщується у вихідному даному R. Маємо R->1∙n!. Оскільки у вхідному даному значення змінної N було n, то дійсно отримали обчислення факторіалу.

Обґрунтування повної коректності.

Покажемо, що при правильних вхідних даних програма завершується (зупиняється). Фактично, треба показати завершуваність циклу F₃ , оскільки інші оператори не впливають на завершення програми. З часткової коректності видно, що за правильних вхідних даних перед виконанням циклу дані мають вигляд [N->n,R->1,M->m] (де n>0). Після кожного виконання циклу R збільшується у m разіві m зменшується на 1. Отже,отримаємо спадну послідовність m і в силу її скінченності, якщо програма входить у цикл, то він завжди завершується. При інших варіантах правильних вхідних даних програма не заходить в цикл, а послідовно виконує прості оператори, тому програма завжди зупиняється в силу скінченності кількості операторів.

Завдання 1.6. Розробити програму, яка за допомогою операції додавання обчислює результат піднесення значення a до степеня b. Оба числа додатні. Виконати:

1) побудувати програму для розв’язання задачі на мові SIPL,

2) побудувати дерево синтаксичного виводу програми,

3) побудувати композиційний семантичний терм програми,

4) довести коректність програми.

Розв’язок.

1) Програма на мові SIPL, яка обчислює a^b через додавання

begin

i:=1;

r:=1;

while i ≤ b do

begin

k:=1;

p:=r;

while a ≠ k do

begin

r:=r+p;

k:=k+1

end;

i:=i+1

end

end

begin[S8]

r:=1;

while  b>0 do

begin

k:=1;

p:=r;

while k<a do

begin

r:=r+p;

k:=k+1

end;

b:=b-1

end

end

2) Дерево синтаксичного виводу програми :

3) Семантичний терм програми:

Sem_P(a^b) = Sem_P(begin i:=1;r:=1;while i≤b do begin k:=1;p:=r; while a≠ k do begin r:=r+p; k:=k+1 end; i:=i+1 end end) =

Sem_S(i:=1;r:=1;while i≤b do begin k:=1;p:=r; while a≠ k do begin r:=r+p; k:=k+1 end; i:=i+1 end) =

Sem_S(i:=1) ◦ Sem_S(r:=1) ◦ Sem_S(while i≤b do begin k:=1;p:=r; while a≠ k do begin r:=r+p; k:=k+1 end; i:=i+1 end) =

ASⁱ(Sem_A(1)) ◦ AS^r(Sem_A(1)) ◦ WH(Sem_B(i≤b),Sem_S(begin k:=1;p:=r; while a≠ k do begin r:=r+p; k:=k+1 end; i:=i+1 end))=

ASⁱ( ) ◦ AS^r( ) ◦WH(S²(leq,Sem_A(i),Sem_A(b)),Sem_S(k:=1;p:=r; while a≠ k do begin r:=

r+p; k:=k+1 end; i:=i+1)) =

ASⁱ( ) ◦ AS^r( ) ◦WH(S²(leq,i=>,b=>),Sem_S(k:=1) ◦Sem_S(p:=r) ◦ Sem_S(while a≠ k do begin r:=r+p; k:=k+1 end; i:=i+1)) =

ASⁱ( ) ◦ AS^r( ) ◦WH(S²(leq,i=>,b=>),AS^k(Sem_A(1)) ◦AS^p(Sem_A(r)) ◦ WH(Sem_B (a≠ k) , Sem_S(begin r:=r+p; k:=k+1 end)) ◦Sem_S( i:=i+1) =

ASⁱ( ) ◦ AS^r( ) ◦WH(S²(leq,i=>,b=>),AS^k( ) ◦AS^p(r=>) ◦ WH(S²(neq,Sem_A (a),Sem_A (k)) , Sem_S(r:=r+p; k:=k+1)) ◦ASⁱ(Sem_A(i+1)) =

ASⁱ( ) ◦ AS^r( ) ◦WH(S²(leq,i=>,b=>),AS^k( ) ◦AS^p(r=>) ◦ WH(S²(neq,a=>,k=>) , Sem_S(r:=r+p) ◦Sem_S(k:=k+1)) ◦ASⁱ(S² (add,Sem_A(i),Sem_A(1))) =

ASⁱ( ) ◦ AS^r( ) ◦WH(S²(leq,i=>,b=>),AS^k( ) ◦AS^p(r=>) ◦ WH(S²(neq,a=>,k=>) , AS^r(Sem_A(r+p)) ◦AS^k (Sem_A(k+1))) ◦ASⁱ(S² (add,i=>, )) =

ASⁱ( ) ◦ AS^r( ) ◦WH(S²(leq,i=>,b=>),AS^k( ) ◦AS^p(r=>) ◦ WH(S²(neq,a=>,k=>) , AS^r(S²(add,Sem_A(r),Sem_A(p))) ◦AS^k (S²(add,Sem_A(k),Sem_A(1))) ) ◦ASⁱ(S² (add,i=>, )) =

ASⁱ( ) ◦ AS^r( ) ◦WH(S²(leq,i=>,b=>),AS^k( ) ◦AS^p(r=>) ◦ WH(S²(neq,a=>,k=>) , AS^r(S²(add,r=>,p=>)) ◦AS^k (S²(add,k=>, )) ) ◦ASⁱ(S² (add,i=>, )) )

4) Довести коректність програми

а) Часткова коректність

Нехай st = [a®m, b®n], m>0, n≥0. Тоді необхідно показати, що якщо Sem_P(a^b)(st)↓ = str, то rÞ(str) = m^n.

Для зручності позначимо: p1 = S²(neq,aÞ,kÞ) ,

f1 = AS^r(S²(add,rÞ,pÞ)) ◦AS^k(S²(add,kÞ, )) , mul(a, r) = WH(p1, f1) ,

p2 = S²(leq, iÞ,bÞ) , f2= AS^k( ) ◦AS^p(rÞ) ◦ mul(a, r) ◦ASⁱ(S² (add,iÞ, ))

Тоді програму можна записати у вигляді:

Sem_P(a^b) = ASⁱ( ) ◦ AS^r( ) ◦WH(p2,f2)

Спочатку покажемо, що mul(a, r) ([a®a₀, k®k₀, r®r₀, p®p₀]) = [a®a₀, k®a₀, r®r₀+(a₀–k₀)*p₀, p®p₀] , для a₀–k₀ ≥ 0. Доведемо це індукцією за величиною t = (a₀–k₀) = (aÞ –kÞ). Позначимо st₀ = [a®a₀, k®k₀, r®r₀, p®p₀].

База індукції: t = 0. У цьому випадку st₀ = [a®a₀, k®a₀, r®r₀, p®p₀]. Перевіримо: mul(a, r) (st₀) = WH(p1, f1) (st₀) = WH(S²(neq,aÞ,kÞ), f1) (st₀) = | neq(aÞ,kÞ) (st₀) = neq(a₀, a₀) = false | = st₀ = [a®a₀, k®a₀, r®r₀+(a₀–k₀)*p₀, p®p₀]. Отже, базу індукції доведено.

Крок індукції: припустимо, що для всіх t £ H (H ≥ 0) виконується припущення індукції mul(a, r) ([a®a₀, k®k₀, r®r₀, p®p₀]) = [a®a₀, k®a₀, r®r₀+(a₀–k₀)*p₀, p®p₀] , для a₀–k₀≥0 і покажемо, що при t = H+  припущення також вірне. Обчислимо mul(a, r) (st₀), де a₀–k₀ = H+  (H ≥ 0): mul(a, r) (st₀) = WH(S²(neq,aÞ,kÞ), f1) (st₀) = | neq(aÞ,kÞ) (st₀) = neq(a₀, a₀– (H+ )) = false | = ( f1 ◦ mul(a, r) ) (st₀) = mul(a, r) (f1(st₀)) = mul(a, r) ( (AS^r(S²(add,rÞ,pÞ)) ◦AS^k(S²(add,kÞ, )) ) (st₀) ) = mul(a, r) ([a®a₀, k® k₀+ , r®r₀+p₀, p®p₀]) = | тепер (aÞ –kÞ) = a₀ –(k₀+ ) = a₀ –(a₀– H) =H, отже можна застосувати припущення індукції для t = H | = [a®a₀, k®a₀, r®(r₀+p₀)+(a₀–(k₀+ ))*p₀, p®p₀] = [a®a₀, k®a₀, r®r₀+(a₀–k₀)*p₀, p®p₀]. Отже, для t = H+  припущення також вірне.

Тепер покажемо, що WH(p2,f2) ([a®a₀, b®b₀, r®r₀, i®i₀]) = [a®a₀, b®b₀, r®r₀*a₀^(b₀–i₀+ ), i®b₀+ , k®k_x, p®p_x] для b₀–i₀+ ≥0. Доведемо це твердження індукцією за величиною t = (b₀–i₀+ ) = (bÞ –iÞ + ). Позначимо st₀ = [a®a₀, b®b₀, r®r₀, i®i₀].

База індукції: t = 0. У цьому випадку st₀ = [a®a₀, b®b₀, r®r₀, i®b₀+ ]. Перевіримо: WH(p2,f2) (st₀) = WH(S²(leq, iÞ,bÞ), f2) (st₀) = | leq(iÞ,bÞ) (st₀) = leq(b₀+ , b₀) = false | = st₀ = [a®a₀, b®b₀, r®r₀*a₀^(0), i®b₀+ ] = [a®a₀, b®b₀, r®r₀*a₀^(b₀–i₀+ ), i®b₀+ ]  . Отже, базу індукції доведено.

Крок індукції: припустимо, що для всіх t £ H (H ≥ 0) виконується припущення індукції WH(p2,f2) ([a®a₀, b®b₀, r®r₀, i®i₀]) = [a®a₀, b®b₀, r®r₀*a₀^(b₀–i₀+ ), i®b₀+ , k®k_x, p®p_x] , для 0 £ b₀–i₀+  £ H (тобто 0 £ bÞ –iÞ +  £ H) і покажемо, що при t = H+  припущення також вірне. Обчислимо WH(p2,f2) (st₀), де b₀–i₀+  = H+  (H ≥ 0) у стані st₀: WH(p2,f2) (st₀) = WH(S²(leq, iÞ,bÞ),f2) (st₀) = | leq(iÞ,bÞ) (st₀) = leq(i₀, b₀) = true, оскільки i₀ = b₀ – H у st₀ | = ( f2 ◦ WH(p2,f2) ) (st₀) = WH(p2,f2) (f2(st₀)) = WH(p2,f2) (AS^k( ) ◦AS^p(rÞ) ◦ mul(a, r) ◦ASⁱ(S²(add,iÞ, )) (st₀)) = WH(p2,f2) (ASⁱ(S²(add,iÞ, )) ( mul(a, r) ( [a®a₀, b®b₀, r®r₀, i®i₀, k® , p®r₀] ) ) ) = WH(p2,f2) ( ASⁱ(S²(add,iÞ, )) ([a®a₀, b®b₀, r®r₀+(a₀– )*r₀, i®i₀, k®a₀, p®r₀]) ) = WH(p2,f2) ([a®a₀, b®b₀, r®a₀*r₀, i®i₀+ , k®a₀, p®r₀]) = | тепер t = bÞ –iÞ +  = b₀–( i₀+ )+  = H, отже можна скористатися припущенням індукції та отримати наступне | = [a®a₀, b®b₀, r®a₀*r₀*a₀^(b₀–(i₀+ )+ ), i®b₀+ , k®k_x, p®p_x] = [a®a₀, b®b₀, r®r₀*a₀^(b₀–i₀+ ), i®b₀+ , k®k_x, p®p_x], що і потрібно було довести. Отже, для t = H+  припущення також вірне.

Тепер, Sem_P(a^b) (st) = ASⁱ( ) ◦ AS^r( ) ◦WH(p2,f2) (st) = WH(p2,f2) ( AS^r( ) ( ASⁱ( ) ( [a®m, b®n] ) ) ) = WH(p2,f2) ( [a®m, b®n, i® , r® ] ) = [a®m, b®n, r® *m^(n– + ), i®n+ , k®k_x, p®p_x] = [a®m, b®n, r®m^n, i®n+ , k®k_x, p®p_x] = str, тобто rÞ(str) = m^n. Ми отримали очікуваний результат обчислень за програмою.

Отже, твердження доведене і програма є частково коректною.

б) Тотальна коректність

Покажемо, що обчислення за програмою завжди зупиняються.

Для початку доведемо завершуваність циклу WH(p1, f1). Позначимо st₀=st (початковий стан для циклу WH(p1, f1)), st₁=f1(st₀), st₂=f1(st₁) і т.д. Для того, щоб цикл завершувався, потрібно показати, що існує такий стан, на якому виконується умова aÞ =kÞ або aÞ –kÞ = 0. Припустимо, що такого стану не існує. Тоді розглянемо послідовність різниць цих змінних, яка має бути нескінченою:

 t₀= aÞ(st₀) –kÞ(st₀), t₁= aÞ(st₁) –kÞ(st₁), t₂= aÞ(st₂) –kÞ(st₂), …

Очевидно, що t₀ ≥ 0 в початковому стані st₀, і те, що t₀ > t₁ > t₂… , тобто послідовність є строго спадною. Тоді ця послідовність не є нескінченою, оскільки вона обмежена знизу числом 0 (різницею однакових чисел), що і треба було довести.

Аналогічно покажемо завершуваність циклу WH(p2, f2). Позначимо st₀=st (початковий стан для циклу WH(p2, f2)),  st₁=f2(st₀), st₂=f2(st₁) і т.д. Для того, щоб цикл завершувався, потрібно показати, що існує такий стан, на якому виконується умова iÞ > bÞ або bÞ –iÞ < 0. Припустимо, що такого стану не існує. Тоді розглянемо послідовність різниць таких змінних, яка має бути нескінченою:

t₀= bÞ(st₀) –iÞ(st₀), t₁= bÞ(st₁) –iÞ(st₁), t₂= bÞ(st₂) –iÞ(st₂), …

Відомо, що b не змінює своє значення протягом виконання циклу і є фіксованим невід’ємним значенням. Оскільки змінна i на кожній ітерації збільшує своє значення на 1, то можна стверджувати, що t₀ > t₁ > t₂… , тобто послідовність є строго спадною. Тоді ця послідовність не є нескінченою, оскільки вона обмежена знизу числом 0, отже, змінна i набуде значення змінної b – що і потрібно було показати.

Таким чином, з часткової коректності та факту зупинки циклів (внутрішнього та зовнішнього) випливає тотальна коректність програми, що розглядається.

Мы поможем в написании ваших работ!