Верифікація програм. Семантики мов програмування

7 ВЕРИФІКАЦІЯ ПРОГРАМ

7.1  Семантики мов програмування

Наука семіотика вивчає загальну теорію знакових систем, до яких належить і теорія програмування. У цій теорії прийнято виділяти три складові частини: синтаксис, який трактує правила побудови текстів мови, семантику, що вивчає зв’язки між текстом і його значенням, та прагматику, яка вивчає відношення між знаковими системами і користувачами.

У теорії програмування семантика – це інтерпретація (смислове значення) абстрактного синтаксису, виражена у термінах математично строгої формальної моделі. Іншими словами, це інтерпретація множини припустимих конструкцій мови програмування.

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

Точний опис семантики необхідний також для створення компіляторів з даної мови програмування.

Існує три основних підходи до формального опису семантики мов програмування.

Операційна семантика. Семантика описується в термінах деякої машини, реальної або віртуальної, наприклад, машини Тьюринга.

Смислове значення програми описується чітко описаною множиною операторів, які можуть бути реалізовані на цій машині. У результаті виконання операторів мови змінюється стан програми – сукупність значень її змінних. Результат виконання програми – це стан, при якому машина завершує роботу з даної програми, який, як правило, залежить від початкового стану.

Аксіоматична (дериваційна семантика). Семантику кожної синтаксичної конструкції мови задають у вигляді аксіом, яким повинні задовольняти вихідні дані, і правил виведення, за допомогою яких може бути отриманий результат (як теорема, що випливає з аксіом за допомогою правил виведення), тобто ця семантика є розширенням математичної теорії вирахування предикатів.

Нагадаємо деякі відомості з теорії предикатів.

Кожному n-відношенню на множинах А₁, …, А_n  можна зіставити  n-місну логічну функцію

Р:   А₁×…×А_n   → {true, falseл} ,

що набуває значення true тоді і тільки тоді, коли виконується дане відношення.

Така функція називається  предикатом.

Приклади предикатів:

isreal (x)   –   “x  є дійсне число” ;

less (x, y)    –  “x  менше  y” ;

div  (x, y)   –   “ у  ділиться на  z” ;

sum  (z, x, b)   –   “ z  є сума  х і b”.

Якщо замінити змінні, що входять у предикат, їх конкретними            значеннями, одержимо висловлення, наприклад: “3,12  є дійсне число”, “6  менше  7”.

Одномісні предикати, як правило, виражають властивості елементів.

Для зручності вводять також 0-місні предикати, що просто є висловленнями.

Метою роботи програми є досягнення завершального стану, що задовольняє якусь (бажану) умову. Цю умову називають постумовою і представляють предикатом Q.

Щоб коректно використовувати програму, нам потрібно знати початковий стан або множину початкових станів, при яких запуск програми  обов'язково приведе до завершалього стану, що задовольняє постумову  Q. Умову, яку задовольняють ці початкові стани, називають передумовою і представляють предикатом Р.

Нехай S – програма або оператор, або послідовність операторів.

Аксіоматична семантика оператора або деякого фрагмента програми задається у вигляді “трійки Хоара” {P}S{Q}. Запис  {P}S{Q}  означає: якщо виконання S почалося в стані, який задовольняє Р, то є гарантія, що воно завершиться через скінченний час у стані, що задовольняє умову Q.

Умову, яка характеризує множину усіх станів, для яких виконання S, що почалося у такому стані, обов'язково закінчиться через скінченний час у стані, що задовольняє умову Q, називають найслабшою передумовою.

Для найслабшої передумови використовують позначення      wp (S,Q) –   weakest pre-condition.

Приклад 7.1  Алгоритм Евкліда знаходження найбільшого спільного дільника НСД (a , b)

Постумова  x=HСД (a,b).                                                   

Найслабша передумова

(HСД(x,y)=HСД(a,b)) and (x>0) and (y>0).

Фрагмент відповідної програми на Pascal має вигляд:

х:=a; y:=b;                                                            

while   x <> y  do

if x>y  then  x:=x-y  else  y:=y-x;

Приклад 7.2

 S:   i:=i+1;         Q:   i <= 1;

 wp (S, Q):   i<=0 .

Найслабша умова означає найменш обмежуючу умову.

Наприклад:  Р1:  (х >3)    слабше, ніж  Р2:  (х >5).