1. 6.1.3. Специфікації завдань концепторним мовою Для постановки складних математичних задач (підсумовування...
2. 6.2.1. Характеристика формальних методів доказу

6.1.3. Специфікації завдань концепторним мовою

Наше деловое партнерство www.banwar.org

Для постановки складних математичних задач (підсумовування нескінченних рядів, теоретікомножественних операцій з нескінченними множинами, Гильбертів оператор та ін.) І завдань штучного інтелекту (ігри, розпізнавання образів і ін.) Запропонований общематематических процедурний мову, так званий концепторний мову - КЯ [ 6.17 ]. У цій мові процес опису складного завдання проводиться шляхом обґрунтування рішення задачі з математичної точки зору, потім формального опису постановок задач і, нарешті, робиться перехід до алгоритмическому опису.

Засоби специфікації складних завдань Основу КЯ становить теоретікомножественний мову, який містить декларативні і імперативні засоби теорії множин ЦермелоФренкеля. Ядро містить набір елементів (типи, вирази, оператори) і засоби визначення нових типів, виразів і операторів.

Декларативні кошти КЯ - це збірний, многосортность логікоматематіческій мову завдання виразів і структуризації безлічі значень (денотат). Вирази складаються з термів і формул, терми позначають об'єкти ПрО, а формули - твердження про об'єктах і відносинах між ними. До конструкторам складових типів і формул відносяться функтори, предикати, конектори і субнектори.

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

Імперативні засоби КЯ - це оператори та процедури для опису об'єктів ПрО за допомогою концепторов, що складаються з розділів для визначення об'єктів розв'язуваної задачі і дій над ними. Кожен концептор - це іменований набір визначень і дій з наступною структурою опису:

концептор К (<список параметрів>) <список імпортних параметрів> <визначення констант, типів, предикатів> <опис глобальних змінних> <визначення процедур> початок К <тіло концептора> кінець К.

Концептор - це декларативне опис об'єктів і імперативне опис операторів обчислення виразів тіла. Розглядається два випадки:

1. декларативний концептор складається з визначень параметрів і типів;
2. імперативний концептор - це тіло з операторів завдань.

Декларативний концептор задає опис об'єктів і понять, пов'язаних з математичною постановкою завдання, а опис методу її рішення за допомогою імперативних концепторов. Концепторное опис - це формальна специфікація завдання, яку можна трансформувати до алгоритмічного опису та верифікації.

Якщо отриманий концептор неефективний, то для підвищення ефективності будується алгоритм, еквівалентний даному концептору. Він будується аппроксимацией концепторного рішення шляхом заміни неконструктивних об'єктів і неефективних операцій конструктивними і більш ефективними аналогами.

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

Денотаціонний підхід полягає у визначенні семантики мови шляхом підстановки кожному виразу відповідного елемента з безлічі денотатов функції інтерпретації символів сигнатури мови. кожній константі , Функціональному символу і предикатні символу зіставляється об'єкт з безлічі денотат. Цей спосіб інтерпретації семантики виразів і операторів мови аналогічний денотаціонной семантики ЯП. Головна відмінність семантики КЯ від семантики програм - це її неконструктивність. З кожним КЯ можна зв'язати деяку дедуктивну теорію, яка відображає властивості концепторов.

Формальна дедуктивна теорія будується шляхом виділення з безлічі всіх формул підмножини аксіом і правил виведення. Для кожної пари , формул дедуктивної теорії і кожного оператора створюється операційна формула з твердженням, що якщо істинно перед виконанням оператора , То завершення оператора забезпечує істинність , Тобто формула - передумова, а - постусловіем оператора . За допомогою неконструктивних об'єктів і нерозв'язних формул цієї теорії можна адекватно описувати властивості неефективних процедур.

Аксіоматичне опис КЯ - це аксіоми і твердження щодо концепторного опису та проведення дедуктивного докази і верифікації цього опису.

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

Техніка доказового проектування. Засоби концепторной специфікації складних, алгоритмічно нерозв'язних завдань покладені в основу формалізованого опису поведінки дискретних систем. Для опису властивостей аппаратнопрограммних засобів динамічних систем застосовуються логіко-алгебраїчні специфікації КЯ, техніка опису яких включає два етапи.

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

На другому етапі система деталізується у вигляді сукупності взаємозалежних підсистем , Кожна з якої описується алгебраїчної специфікацією. В результаті виходить специфікація системи з функцій переходів і виходів, для яких необхідно доводити коректність. Процес деталізації виконується на рівні елементної бази або елементарних програм і супроводжується доказом їх коректності. В кінцевому підсумку виходить система S, еквівалентна вихідної специфікації. Приклади докази систем наведені в [ 6.17 ]. Розглянемо один з них.

Нехай потрібно побудувати специфікацію натуральних чисел з безлічі цих чисел з сигнатурою операцій . При побудові використовується число і функція проходження . Специфікація складається з наступних аксіом:

1. ,
2. ,
3. ,
4. ,
5. ,
6. 
7. 

При цьому алгебри стають багатоосновними алгебра, а аксіоми - специфікаціями: тотожними і Квазітотожні. Алгебраїчні специфікації - найбільш використовувані, оскільки для них існують ефективні алгоритми виконання, які перетворять специфікації в ЯП високого рівня. Тому такі мови називають мовами виконуваних логіко-алгебраїчних специфікацій. Їх операційна семантика заснована на переписуванні термів, а створювана алгебраїчна специфікація отримує логічну семантику, яка використовується при доказі теорем.

6.2. Методи доведення правильності програм

Формальні методи тісно пов'язані з математичними техніками специфікацій, верифікацією і доказом правильності програм. Ці методи містять математичну символіку, формальну нотацію і апарат виведення. Правила докази є громіздкими і тому на практиці рідко використовуються рядовими програмістами. Однак з теоретичної точки зору вони розвивають логіку застосування математичного методу індукції при перевірці правильності програм. На основі специфікації програм проводиться часткове і повне доведення правильності програм [ 6.4 , 6.5 ].

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

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

Теорема 6.1. Якщо виконані всі дії методу індуктивних тверджень для програми, то вона частково правильна щодо тверджень , , .

Потрібно довести що, якщо виконання програми закінчиться, то твердження буде справедливим. За індукції, при проходженні точок програми, в яких твердження буде справедливим, то і -я точка програми буде такою ж. Таким чином, якщо програма пройшла -точку і затвердження і справедливі, то тоді, потрапляючи з -ої точки в точку, твердження буде справедливим, що й треба було довести.

6.2.1. Характеристика формальних методів доказу

Найбільш відомими формальними методами докази програм є метод рекурсивної індукції або тверджень Флойда, Наура, метод структурної індукції Хоара та ін. [ 6.4 , 6.5 , 6.18 , 6.19 ].

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

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

Формування таких тверджень - досить складне завдання, особливо для програм з високим ступенем паралельності і взаємодії з користувачем. Крім того, важко перевірити достатність і правильність самих тверджень.

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

Даний метод докази зменшує число помилок і час тестування програми, забезпечує відпрацювання специфікацій програми на повноту, однозначність і несуперечливість.

Метод Хоара - це вдосконалений метод Флойда, заснований на аксіоматичному описі семантики мови програмування вихідних програм. Кожна аксіома описує зміна значень змінних за допомогою операторів цієї мови. Формалізація операторів переходу і викликів процедур забезпечується за допомогою правил виведення, що містять індуктивні висловлювання для кожної точки і функції вихідної програми.

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

Опис за допомогою системи правил тверджень - громіздке і відрізняється неповнотою, оскільки всі правила передбачити неможливо. Даний метод перевірявся експериментально на безлічі програм без застосування засобів автоматизації через їх відсутність.

Метод Маккарті полягає в структурній перевірці функцій, які працюють над структурними типами даних, структур даних і діаграм переходу під час символьного виконання програм. Ця техніка включає в себе моделювання виконання коду з використанням символів для змінюваних даних. Тестова програма має вхідний стан, дані і умови її виконання.

Виконувана програма розглядається як серія змін станів. Саме останнє стан програми вважається вихідним станом і якщо воно отримано, то програма вважається правильною. Даний метод забезпечує високу якість вихідного коду.

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

Основу методу складає математична індукція, абстрактне опис програми та її обчислення. Математична індукція застосовується при проходженні циклів і рекурсивних процедур, а також необхідних і достатніх умов тверджень. Абстракція дозволяє сформулювати деякі кількісні обмеження. При обчисленні на основі інваріантних відносин перевіряються на правильність кордону обчислень і одержувані результати.

Процес формального докази правильності програм методом математичної індукції зарекомендував себе як система правил статичної перевірки правильності програм за столом для виявлення в них формальних помилок. За допомогою цього методу можна довести істинність деякого припущення в залежності від параметра для всіх , І тим самим довести випадок . Виходячи з істинності для будь-якого значення , доводиться , Що досить для доведення істинності для всіх .

Шлях доказ наступний. Нехай дано опис деякої правильної програми (її логіки) і твердження щодо цієї програми, яка при виконанні досягає деякої певної точки. Проходячи через цю точку раз, можна отримати справедливість твердження , Якщо индуктивно довести, що:

1. справедливо при першому проході через задану точку,
2. якщо справедливо при проходах через задану точку, то справедливо і проходження через задану точку раз.

Виходячи з припущення, що програма в кінці кінців успішно завершиться, твердження про її правильності буде справедливим.