К. М. Лавріщева програмна інженерія підручник Київ, 2008
 Скачать 5.23 Mb.
|
|
Приклад програми. Алгоритм реєстрації компонента (ком) в репозитарії (repoz). Опис даних на мові «Паскаль» з використанням мовних конструкцій VDM при опису роботи зі списком компонентів (list_ptr). post-Add_rd (r): Rn bool r elems l1.rds li’.rds =li.rds R_card = record r.name: string; ком: list_ptr end; repoz = record rdrs: list_ptr; ctlg: list_ptr; ril: list_ptr end; var L: repoz; procedure Add_rd(r=string); rcrd:R_card; LL : list_ptr; begin if find _rds, r) then begin writeln (‘компонент зареєстрований) end; new (Rcrd); Rcrd.r_name := r; Rcd.ком:=nil; new (LL); LL.next:=L.rds; LL.value:=ltcrd; L.rds:=LI end. 6.1.2. Мова формальної специфікації – RAISE Мова RAISE і RSL-специфікація (RAISE Specification Language) були розроблені в 80-роках XX ст. як результат попереднього дослідження формальних методів верифікації програм і поповнення їх новими можливостями щодо Розділ 6 151 доведення. Метод містить у собі нотації, техніку і інструменти для формального опису ( RSL, С++ і Паскаль) програм і доведення їх правильності [9, 10]. До складу мови RSL входять абстрактні параметричні типи даних (специфікації, алгебри) і конкретні типи даних (модельно-орієнтовані), підтипи, операції для завдання послідовних і паралельних програм. Тобто ця мова надає аплікативний і імперативний стиль специфікації абстрактних програм, а також формальне конструювання окремих програм в інших мовах програмування і апарат доведення їх правильності. Синтаксис цієї мови близький до синтаксису мов С++ і Паскаль. У мові RSL є абстрактні типи даних і конструктори складних типів даних, такі як добуток (product), множини (sets), списки (list), відображення (map), записи (record) і т.п. Добуток типів – це впорядкована скінченна послідовність типів Т 1 , Т 2 ., Т n добутку (product) Т 1 Т 2 ,..., Т n Кількість компонентів добутку d – це size (d) = id (null (couter inc(counter))). Конструктор добутку d 1 і d 2 будує добуток d 1 d 2 і значення типу product (Т1 Т, Тn), тобто make product (value 1 ., value n) = (value i 1) . (value n n), де значення value i має тип Т i , а результуюче значення – тип добутку Т 1 Т 2 , …, Т n має значення (value n). Списки типів – це послідовність значень одного типу list Т – можуть бути скінченним списком типів Тk і нескінченним списком типів Tn. За структуру даних типу списків можна взято бінарне дерево, в якому є голова (head), син ( tail), який слідує за ним у списку, і хвіст. До операцій списку належить операція hd – узяття першого елемента списку, тобто голови, і операція tl – узяття хвоста – решти елементів (як у мові VDM). Функція Caddr (I) = L tail tail Head вибирає із списку I елемент та індекс голови елемента, кількість елементів у списку і ін. Відображення – це структура (map), яка ставить у відповідність значенням одного типу значення іншого типу. Разом з тим відображення – це бінарне відношення декартових добутків двох множин як сукупності двокомпонентних пар, в яких перший компонент – arg, що містить у собі елементи аргументів відображення, а другий компонент – res – відповідні елементи значень цього відображення. Операції над відображеннями такі: накладення, об'єднання, композиція, зріз, композиція відображень (m 1 , m 2 ). Запис – це сукупність іменованих полів даних. Цей тип відповідає типу recordу мові Паскаль і struct у мові С++. У мові RAISE для запису визначено два конструктори – record, shurt record. Об'єднання– це конструктор union,що забезпечує об'єднання типів, наприклад, typeid = id 1 , id 2 ,., idn і тип id , який одержує одне із значень у списку елементів. Конструктор типу – це тип виду type id = id_from_ id1 (id_to_ id1: id1. Таким чином, мови VDM і RAISE слугують для математичного опису програм і конструювання структур даних як специфікацій, що використовуються при доведенні програм. 6.1.3. Концепторна мова специфікації Для постановки складних математичних задач (підсумовування нескінченних рядів, теоретико-множинних операцій з нескінченними множинами тощо) і задач штучного інтелекту (ігри, розпізнавання образів тощо) з метою їх формального опису запропонована загально математична процедурна мова, а саме, концепторна мова (КМ) [16]. У цій мові процес опису складного завдання проводиться шляхом обґрунтування розв’язку задачі з математичної точки зору, потім формального опису постановок задач і, нарешті, переходу до алгоритмічного опису. Специфікація складних завдань. Концепторна мова містить у собі декларативні й імперативні засоби теорії множин Цермело–Френкеля. Ядро цієї мови містить набір елементів (типи, вирази, оператори) і засоби визначення нових типів, виразів і операторів. Декларативні засоби КМ – це типізована логіко-математична мова для опису виразів і структуризації множин значень (денотат). Вирази складаються з термів і формул, терми позначають об'єкти ПрО, а формули – твердження про об'єкти і відношення між ними. Базові елементи мови – конструктори складених типів і формул, а саме функтори, предикати, конектори і субнектори. Функтор– це конструктор, що перетворює терми на терми. Предикати перетворюють терми на формули. Конекторывміщують логічні зв'язки і квантори для перетворення однієї формули в іншу. Субнектор (дескриптор) – це конструктор побудови термів з виразів і формул. Імперативні засоби КМ – це оператори і процедури для опису об'єктів ПрО за допомогою концепторів. Опис процедури має такий загальний вигляд: концептор К ( список параметрів ) список імпортних параметрів> визначення констант, типів, предикатів> опис глобальних змінних> визначення процедури> початок К тіло концептора> кінець К. Денотаційний підхід полягає у визначенні семантики і підстановці в кожний вираз опису елемента з множини денотатів функції символів з сигнатури мови. Кожній константі C c , функціональному символу F f і предикативному символу P p зіставляється об'єкт з множини денотат. Цей спосіб інтерпретації семантики виразів і операторів мови аналогічний денотаційній семантиці мов програмування. Аксіоматичний опис КМ – це аксіоми і твердження щодо концепторного опису і проведення дедуктивного доведення і верифікації цього опису. Логіко-алгебраїчні специфікації КМ призначені для специфікації ПрО, що задаються у вигляді алгебраїчної системи, за допомогою відповідних носіїв, сигнатури і трьох принципів. Перший принцип – логіко-алгебраїчна специфікація ПрО і уточнення понять ПрО, другий принцип – опис властивостей ПрО у вигляді Розділ 6 153 аксіом, які формулюються мовою предикатів першого порядку і хорновських атомарних формул, і, нарешті, третій принцип – це визначення термальних моделей з основних термів специфікації. Засоби КМ використовуються при формальній специфікації поведінки дискретних систем. Для опису властивостей апаратно-програмних засобів динамічних систем застосовуються логіко–алгебраїчні специфікації. Техніка опису таких систем складається з двох процесів. На першому процесі дискретна система S розглядається як «чорна скринька» з скінченним набором входів, виходів і станів. Області значень входів і виходів – довільні, а функціонування системи S – це набір часткових відображень і операцій алгебраїчної системи. Вони утворюють часткову алгебру, формальний опис якої виконується за допомогою алгебраїчних специфікацій, і це є програмою моделювання станів дискретної системи. На другому процесі система S деталізується у вигляді сукупності взаємозалежних підсистем S 1 ,..., Sn, кожна з яких описується алгебраїчною специфікацією. Внаслідок цього одержують специфікацію системи S із функцій переходів і виходів, для яких необхідно доводити коректність. Процес деталізації виконується на рівні елементної бази або елементарних програм і супроводжується доведенням їх коректності. Отже, маємо, що система S еквівалентна початковій абстрактній специфікації. Приклади доведення. Нехай треба побудувати специфікацію натуральних чисел з множини цих чисел і сигнатури операцій = (+, , ). При побудові використовується число 0 і функція проходження s: N N’. Специфікація складається з таких аксіом: х+0 = х х+s(у) = s (х+у) х 0 = 0 х+s(у) = s (х у) +х 0 х х в s (х) s (у) s (х) s (у) х в Алгебраїчні специфікації називають мовами логіко-алгебраїчних специфікацій, їх операційна семантика заснована на переписуванні термів, а утворена алгебраїчна специфікація одержує логічну семантику, використовувану при доведенні теорем. 6.1.4. Звичайна мова специфікації Spec# Сучасна мова специфікація Spec# є розширенням об’єктно-орієнтованої мови С# засобами, що забезпечують верифікацію програм для платформи .Net [27]. Ці засоби подаються до програми в С# невеликими додатковими описами, а саме: – ненульових посилань до параметрів викликів CALL; – контрактів між викликами і реалізаціями; – обробки виникаючих виключних ситуацій програми для інформування розробника; – змінювання полів даних об’єктів тощо. Ненульові типи даних помічаються типом Т! і відповідають деяким змінним програми, які можуть використовуватися при специфікації полів даних, формальних параметрів і з обернених цьому типу значень, локальних змінних програми. Цей тип не належить до елементів масиву. Головне призначення ненульових типів – забезпечити посилання до інших елементів, опис патернів, перевірку умов виходу з виразів і циклів, обумовлених контрактом. Контракт ставиться між тим, хто робить виклик, і хто – реалізацію. У передумові додається опис стану параметрів при виклику, в постумові визначається умова отримання результату об’єкта, що викликався, і передача цього результату протилежна. Spec# надає підтримку більш дисциплінованому використанню виключення, щоб забезпечити ясність і підтримку життєздатності програми. У програмі можуть бути відмови і помилки. У даному випадку у методі використовується аналіз забороненої умови, коли передумова була не задоволена. Більшість відмов у програмі – це, коли порушена умова контракту. Наприклад, отримання виходу з циклу при перевищенні значення параметра циклу, що не було визначено у передумові. Обробка виключних ситуацій виконується при роботі з масивами, коли елемент не відповідає типу. Якщо в передумові специфікується індекс, що знаходиться всередині меж масиву, а при виконанні цього не відбувається, то компілятор відповідає клієнту про невиконання передумови в реальному часі. Змінювання полів даних задається фреймовими умовами, що вміщується у контракт, і починаються modifies, за яким слідкує оператор частини програми методу реалізації, що дозволяє зміну. Приклад. Class C{ Int x, y; Void M () modifies x: {…}. }. Тут метод М дозволяє зміну х при умові, що на виході з цього методу у має те саме значення, що на вході. У випадку масиву такий оператор змінює не елементи масиву, а посилання – на цей масив. Фреймові умови для сервера використовуються під час виконання програми. При цьому modifies перевіряє на вході усі передумови і постумови виконання операторів програми в С#, на яких базуються описи специфікацій в Spec# і рахуються коректними. Успадкування специфікацій. Контрактний метод успадковується звичайним методом, який під час виконання звертається до нього. Специфікація в Spec# подає код виконання в більш наглядній формі і більш зручній для перевірки заданих постумов. Метод може додавати до опису специфікації додаткові постумови і різні реакції на виключні ситуації. Метод має об’яву в інтерфейсі, подібно до об’яві в класі. Коли клас виконує метод інтерфейса, то його опис містить у собі фреймові умови, котрі є суперкласом виконануваного методу. Для виконання фреймових умов використовується оператор expose. Він, як правило, визначає об’єкт, інваріантний модифікації. Специфікація в Spec# являє собою блок операторів, який явно вказує на те, коли об’єктний інваріант можуть явно використовувати оператори, що вказані після expose. При цьому можуть модифікуватися усі поля в структурі об’єкта. Підхід до реалізації специфікації. Опис специфікації в Spec# є самостійною програмою, що містить у собі перед- і постумови, а також різні дії над фреймовими структурами щодо програми, яка перевіряється мовою С#. Ця специфікація Розділ 6 155 подається в мово-незалежному форматі і перебудовується в мову С# за допомогою спеціального транслятора, що працює на платформі .Net. Цей транслятор має аналізатор і версифікатор для перевірки правильності опису специфікації. Транслятор виконує переклад у вигляді частини програми, для якої створювалася специфікація. Верифікація специфікації є статичною, вона орієнтована на перевірку правильності опису, а саме, меж масивів, явних значень змінних тощо. Прувер транслятора виконує перевірку деяких умов і операторів, а також значень змінних. Специфікації в Spec# накопичуються у репозитарії, і при застосуванні звертаються до Base Class Library, де накопичуються об’єкти, їхні інваріанти та контракти. Контракти і аналогічні механізми верифікації програм з мов програмування реалізовані також в системах Java, Eiffel і Spark. У мові Java контракти вміщуються в опис програми як стилізовані коментарі. Середовище Java має такі засоби: перевірку контрактів у динаміці, виконання, виклики та об’єктні інваріанти. В об’єктно-орієнтованій системі Eiffel є бібліотека констрейнів, котрі вставляються у опис об’єкта і виконують верифікацію в динаміці виконання. Однак механізми модифікації не дозволяють для callbacks об’єктних інваріантів і тому вони не вміщуються в модульні об’єкти. Система Spark підтримує підмножину мови Ада при вставці теорем для прувера, помічених як коментарі, але компілятор цієї мови їх не використовує. Засоби верифікації в Spark орієнтовані на окремий опис умов виконання Ада-програм для верифікації, аналогічно до методології Spec#. Вони окремо транслюються у вихідний код Ада-програми і виконуються разом з нею в режимі верифікації. 6.2. Методи доведення правильності програм Формальні методи тісно пов'язані з математичною специфікацією, верифікацією і доведенням правильності програм. Ці методи містять у собі математичну символіку, формальну нотацію і апарат виведення. Правила доведення є громіздкими і тому на практиці рідко використовуються рядовими програмістами. Проте з теоретичної точки зору вони слугують розвитку логіки застосування математичного методу індукції в процесі перевірки правильності програм [4, 5, 17, 18]. 6.2.1. Базові методи доведення Відомо багато методів доведення специфікацій програм, деяким з них дамо коротке визначення. Метод Флойда заснований на знаходженні умов для вхідних і вихідних даних і полягає у виборі контрольних точок у програмі, яка доводиться, таким чином, щоб шлях проходження перетинав хоча б одну контрольну точку. Для цих точок формулюються твердження про стан і значення змінних у них (для циклів ці твердження повинні бути істинними при кожному проходженні циклу – інваріанта). Кожна точка розглядається для індуктивного твердження того, що формула залишається істинною при поверненні програми в цю точку, і залежить не тільки від вхідних і вихідних даних, а й від значень проміжних змінних. На основі індуктивних тверджень і умов на аргументи програми створюються твердження з умовами перевірки правильності цієї програми в окремих її точках. Для кожного шляху програми між двома точками встановлюється перевірка на відповідність умов правильності і визначається істинність цих умов при успішному завершенні програми на даних, що задовольняють вхідні умови. Метод Хоара – це вдосконалений метод Флойда, заснований на аксіоматичному описі семантики мови програмування початкових програм. Кожна аксіома описує зміну значень змінних за допомогою операторів цієї мови. Формалізація операторів переходу і викликів процедур забезпечується за допомогою правил виводу, що містять у собі індуктивні вислови для кожної точки і функції початкової програми. Метод Маккарті полягає у структурній перевірці функцій, що працюють над структурними типами даних, структур даних і шляхів переходу під час символьного виконання програм. Ця техніка складається з моделювання виконання коду з використанням символів для змінних даних. Тестова програма має вхідний стан, дані і умови її виконання. Виконувана програма розглядається як серія змін станів. Саме останній стан програми вважається вихідним станом і, якщо його одержали, то програма вважається правильною. Даний метод забезпечує високу якість початкового коду. Метод Дейкстри пропонує два підходи до доведення правильності програм. Перший підхід заснований на моделі обчислень, що оперує історіями результатів обчислень програми, аналізом шляхів проходження і правил оброблення великого об'єму інформації. Другий підхід базується на формальному дослідженні тексту програми за допомогою предикатів першого порядку. У процесі виконання програма одержує деякий стан, який запам'ятовується для подальших порівнянь. Основу методу становить математична індукція, абстрактний опис програми і її обчислення. За допомогою цього методу можна довести істинність деякого припущення Р(n) залежно від параметра n для всіх n n 0 , і тим самим довести випадок Р (n 0 ). Виходячи з істинності Р(n) для будь-якого значення n, доводимо Р(n+1), що достатньо для доведення істинності Р(n) для всіх n n 0 . |