Меню сайта
Категории раздела
Друзья сайта
Статистика
Онлайн всего: 1
Гостей: 1
Пользователей: 0
| Главная » Статьи » Реферати » Логіка |
Реферат на тему Алгоритмічна логіка Хоара
|
Реферат на тему: Алгоритмічна логіка Хоара. Алгоритмічна логіка Хоара План Вступ Алгоритмічні логіки Біографія Хоара Алгоритмічна логіка Хоара Аксіоми Хоара; Приклад розв’язування задачі з використанням аксіом. Висновок Вступ Логіка – це теорія, яка вивчає, як правильно потрібно міркувати, правильно робити висновки, отримувати в результаті правильні висловлювання. Тому логіка це наука, яка повинна містити список правил отримання правильних висловлювань. Алгоритмічні логіки На початку 70-х років ХХ століття виникли алгоритмічні логіки. Вони були створені з метою опису семантики мовою програмування. Алгоритмічні логіки включають висловлювання вигляду , які читаються: «Якщо до виконання оператором S було виконано , то після нього буде ». Ця логічна мова майже одночасно була створена Р.У.Флойдом (1967), К.Хоаром (1969) і представниками польської логічної школи (А.Сальвініцький та інші (1970)). В 1969 році Хоар визначив просту мову програмування через логічну систему аксіом і правила виведення для доведення часткової правильності програми. В його роботі показано, що для визначення семантики мови не в термінах виконання програми, а в термінах доведення її правильності спрощує процес створення програми. В 70-х роках на базі роботи Хоара починаються дослідження в області аксіомних визначень мови програмування. З’являється багато робіт з аксіоматизації різних конструкцій: від оператора присвоювання до різних форм циклів, від виклику процедур до співпрограм. Головним недоліком дослідників в ті роки було те, що вони не приділяли достатньо уваги формальній логіці. В 1972 році вийшла чергова стаття Хоара про доказ правильного подання даних, що прискорило дослідження абстрактних типів даних. В СРСР роботи в цій області проводились в Новосибірську (А.П.Єршов, В.Н.Агафонов, А.В.Замулин, И.Н.Скопина). В 1973 році були сформульовані правила доведення правильності для більшості конструкцій мови Паскаль. В 1975 році була побудована автоматична система «верификации для подмножества» мови Паскаль, заснована на аксіомах і правилах виведення. В 1979 році була визначена мова програмування Евкліда, в проект яого з самого початку була закладена ідея аксіоматизації. В 1976 році вийшла книга Е.Дейкстри «Дисципліна програмування», в якій пропонується метод доведення правильності програми. Суть методу полягає в тому, щоб будувати програму разом з доведенням, причому доведення повинно випереджати побудову програми. Е.Дейкстр визначив для простої мови програмування слабкі передбачення і показав, як їх можна використовувати в якості підрахування для виведення програми. Стало зрозуміло, що користування формалізмом може призвести до побудови програм більш надійним способом.» [3] Біографія Хоара Чарльз Ентоні Річард Хоар – британський вчений, який спеціалізується в області інформатики і обчислювальної техніки. Найбільш відомий як винахідник алгоритму «швидкого сортування» (1960), на сьогоднішній день являється найпопулярнішим алгоритмом сортування. Інші відомі результати його роботи: мова Z специфікацій і паралельна модель взаємодії послідовних процесів (CSP, Communicating Sequential Process). В числі його заслуг – розробка логіки Хоара (Hoare Logic), наукової основи для конструювання коректних програм, які використовуються для визначення і розробки мови програмування. Хоар створив ряд робіт по створенню специфікацій, проектуванню, реалізації та супроводженню програм, які показують важливість наукових результатів для збільшення продуктивності комп’ютерів і підвищення надійності програмного забезпечення. Народився Чарльз Ентоні Річард Хоар в Коломбо В Шрі-Ланці. Отримав класичну ступінь бакалавра в Університеті Оксфорда (Merton College) в 1956 році. Проходив службу в ВМС Великобританії в 1956-1958 роках. Вивчив російську мову, він навчався комп’ютерному перекладу під керівництвом А.Н.Колмогорова в Московському державному університеті. В 1960 році, через політичну кризу, пов’язану з винищенням розвідувального літака У-2, він залишив Радянський Союз і почав працювати в невеликій компанії по виробництву комп’ютерів Elliott Brothers, де займався реалізацією мови ALGOL60. Там він закінчив займатися розробкою алгоритмів. В 1968 році став професором інформатики та обчислювальної техніки в Королівському Університеті Белфаста (Queen’s University Belfast). В 1977 році повернувся в Оксфорд, як професор обчислювальної техніки, щоб очолити дослідницьку групу Programming Research Group, в завдання якої входить укріплення зв’язку промислових, академічних і державних структур, працюючих в області ІТ-індустрії. Тематика його винахідницької роботи в Оксфорді: коректність програмних специфікацій, проектування та розробка критичних та некритичних систем. В 1999 році вийшов на пенсію в званні почесного професора та перейшов на посаду головного досліджувача в Microsoft Research в Кембриджі, де і працює по сьогоднішній день. В 1980 році він отримав Приз Тюрінга за « його видатні досягнення в визначенні і дизайні мови програмування». В 2000 році йому було присвоєно звання рицарського титулу за заслуги в області освіти та комп’ютерних наук, Премії Кіото. [1], [2] Алгоритмічна логіка Хоара Основою для логіки виведення правильних програм служать аксіоми Хоара. Вони допускають інтерпретації в термінах програмних конструкцій. Сформулюємо аксіоми Хоара, які визначають передумови як достатні умови, які гарантують, що виконання відповідних операторів при вдалому завершенні приведе до бажаних після умов. [3] А1. Аксіома присвоювання: Неформальне пояснення аксіоми: так як після виконання буде містити значення , тоді буде істинне після виконання, якщо результат підстановки замість в істинне перед виконанням. А2. А3. Нехай — це послідовність з двох операторів і . А4. Аксіома А5 відповідає інтерпретації умовного оператора в мові програмування. Сформулюємо правило для альтернативного оператора (повна форма умовного оператора): А6. і для операторів циклу. Передумови та після умови циклу until (до) задовольняють правило: А7. Правило вводить важливе поняття інваріанта циклу. Предикат , істинний перед виконанням і після виконання кожного кроку циклу, називається інваріантним відношенням або просто інваріантом циклу. В математиці термін «інваріантний» означає не змінюючий під впливом сукупності розглядаючи математичних операцій. В даному випадку єдина операція – це виконання кроку циклу при умові істинності спочатку. Передумови і після умови циклу while (поки) задовольняють правило: А8. Аксіоми А1 – А8 можна використовувати для перевірки узгодження передачі даних від оператора до оператора, для аналізу структурних властивостей текстів програм, для встановлення умов закінчення циклу. Крім того, правила можна використовувати для аналізу результатів виконання програми, що пов’язано з семантикою програми. Приклад. Нехай потрібно визначити частку і остачу від ділення на . Вхідні дані: , — цілі невід’ємні числа, причому > 0. Вихідні дані: , — цілі невід’ємні числа. Опис програми : Сформулюємо передумову : — цілі числа. Сформулюємо після умову : Потрібно довести, що або Доведення. | Мова | Метамова 1 | Виведення в формальній арифметиці 2 | Аксіома А1 3 | АксіомаА1 4 | А3 до пунктів 1 і 2 5 | А4 до пунктів 3 і 4 6 | арифметика 7 | Аксіома А1 8 | Аксіома А1 9 | А4 до пунктів 7 і 8 10 | А2 до пунктів 6 і 9 11 | А8 до пункту 10 12 | А4 до пунктів 5 і 11 Доведемо, що виконання програми закінчується. Припустимо, що програма не закінчується. Тоді повинна існувати нескінченна послідовність значень і , яка задовольняє умови: 1) 2) — цілі невід’ємні числа. Значення на кожному кроці циклу зменшується на додатну величину: . Отже, послідовність значень і є скінченою, тобто знайдеться таке значення , для якого не буде виконуватись умова , і циклічний процес завершується. Таким чином, встановлено, що Інакше кажучи, наша програма є тотально вірною. Висновок Отже, ми розглянули як застосовується логіка у простій мові програмування та визначили її складність. Застосування логічного алгоритму для вирішення конкретної задачі є досить складною проблемою, вирішення якої потребує не лише досконалого володіння саме цим алгоритмом, але й всебічного розглядання того чи іншого алгоритму, тобто визначення усіх його переваг і недоліків. Хоар визначив просту мову програмування через логічну систему аксіом і правила виведення для доведення часткової правильності програми. В його роботі показано, що для визначення семантики мови не в термінах виконання програми, а в термінах доведення її правильності спрощує процес створення програми. Хоара проводив дослідження в області аксіомних визначень мови програмування. Головним недоліком дослідників було те, що вони не приділяли достатньо уваги формальній логіці. Основою для логіки виведення правильних програм служать аксіоми Хоара. Отже, головною задачею, яку має вирішити людина, створити сучасніший, простіший метод доведення правильності програм. А також зазначити як позитивні, так і усі негативні характеристики різних методів розв’язування задач, з використанням алгоритмічних логік та з передбаченням кінцевого результату. | |
| Просмотров: 435 | Рейтинг: 0.0/0 |
| Всего комментариев: 0 | |