Тема 5. Аксіоматична семантика

 

Завдання 5.1. Довести часткову коректність програми DIV(a,b) (див. завдання 1.2) за допомогою логіки Хоара (в аксіоматичній семантиці).

 

Розв’язок.

Введемо позначення:

DIV(a,b) =     rez:=0; k:=0; if a=0 then skip else if a<0 then skip else while k<=a-b do begin rez:=rez+1;k:=k+b end; ost:=a-k	S1 = rez:=0; k:=0;   S2 = if a=0 then skip else if a<0 then skip else while k<=a-b do begin rez:=rez+1;k:=k+b end; ost:=a-k
IF1 = if a=0 then skip else if a<0 then skip else while k<=a-b do begin rez:=rez+1;k:=k+b end	IF2 = if a<0 then skip else while k<=a-b do begin rez:=rez+1;k:=k+b end
WH = while k<=a-b do begin rez:=rez+1;k:=k+b end	S3 = rez:=rez+1;k:=k+b

 

Тоді маємо наступне виведення в логіці Хоара:

 

 

(*) =

 

(**) =

 

(***) =

де предикати мають такий вигляд:

Інваріант цієї задачі для циклу while: P={rez=k/b}.

Розглянемо предикат qf: з нього випливає, що . Далі, і при цьому . Звідси випливає, що , тобто скільки разів b повністю укладається в a, або ж ціла частина від ділення, тоді  – залишок від ділення a на b за означенням.

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

 

 

Завдання 5.2.

1) Побудувати програму обчислення n! через операцію «+».

2) Довести часткову коректність побудованої програми за допомогою логіки Хоара (в аксіоматичній семантиці).

 

Розв’язок.

1) Програма обчислення n! через операцію додавання:

Prog(n) =

begin

    res := 1;

    i : = 1;

while i <= n do

begin

j := 1;

F3 або WH(…)1

F2

k := res;

while j < i do

F4

begin

F5

S2

WH(…)2

k := k + res;

j := j+1

end;

F6

res := k;

i := i + 1

end

end

 

На тексті програми введено позначення (скорочення), які ми будемо використовувати далі.

 

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

Деякі предикати, які зустрінуться в доведенні:

Необхідно показати, що в результаті обчислень за програмою ми отримаємо , що еквівалентно qf.

Решту предикатів ми будемо обчислювати в ході виведення (доведення) в логіці Хоара:

 

 

(1)

 

(2)

 

(3)

 

(4)

 

(5)

 

(6)

 

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

 

 

Завдання 5.3. Довести часткову коректність програми Sum_fac(n) обчислення суми факторіалів до вхідного n≥0 (включно) через множення і додавання (див. завдання 4.3) за допомогою логіки Хоара (в аксіоматичній семантиці).

 

Розв’язок.

Введемо позначення:

Sum_fac(n) =   i:=0;   fac:=1;   res:=1;   while i ≠ n    begin      i:=i+1;      fac:= fac*i;      res:=res+fac    end

W = while i ≠ n    begin      i:=i+1;      fac:= fac*i;      res:=res+fac;    end

Позначення предикатів:

P =

P₀ =

P₀₁ =

P₀₂ =

T =

T₀ =

T₁ =

B =

 

 

 

 

 

Таким чином, з істинності  (предиката P) як передумови випливає істинність  (як предиката , тобто  та {i = n})як післяумови, що і доводить часткову коректність програми.

 

 

Література

 

1. Nikitchenko N. A Composition Nominative Approach to Program Semantics. – Technical Report IT-TR: 1998-020. – Technical University of Denmark. – 1998. – 103 p.

2. Басараб И.А., Никитченко Н.С., Редько В.Н. Композиционные базы данных. – К.: Либідь, 1992. – 191 с.

3. Winskel G. The Formal Semantics of Programming Languages: An Introduction. – London: MIT Press Foundations of Computing Series, 1993. – 361 p.

4. Nielson H.R., Nielson F. Semantics with Applications: A Formal Introduction. – Wiley Professional Computing, 1992. – 240 p.

5. Редько В.Н. Семантические структуры программ // Программирование. – 1981. – № 1. – С. 3–19.

6. Никитченко Н.С. Композиционная семантика языков программирования // Программирование. – 1982. – № 6. – С. 9–18.

7. Нікітченко М. С., Панченко Т. В. Структури даних в композиційних мовах програмування //Вісник Київського університету. Серія: фіз.-мат. науки. – 2004. – вип. 2. – С. 316–325.

8. Панченко Т. В. Моделювання структур даних та функцій над ними в композиційно-номінативній мові ACoN //Проблемы программирова­ния. – 2004. – №1-2. – С. 7–15.

9. Панченко Т. В. Композиційні методи специфікації та верифікації програмних систем. Дисертація на здобуття наукового ступеня кандидата фізико-математичних наук. – Київ, 2006. – 177 с.

 

 

[S1]Добавить унарный минус

[S2]Альтернативный вариант если есть Dec()

[S3]Унарный минус отсутствует. Надо писать 0-M, 0-N

[S4]Оптимизированный вариант

[S5]Этот оператор лишний

[S6]Этот оператор лишний

[S7]Оптимизированный вариант

[S8]Оптимизированный вариант

---

Дата добавления: 2018-04-05; просмотров: 346; Мы поможем в написании вашей работы!

Поделиться с друзьями:

---

---

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