Реферат на тему:
Алгоритмічна логіка Хоара
План
Вступ
Алгоритмічні логіки
Біографія Хоара
Алгоритмічна логіка Хоара
Аксіоми Хоара;
Приклад розв’язування задачі з використанням аксіом.
Висновок
Вступ
Логіка – це теорія, яка вивчає, як правильно потрібно міркувати,
правильно робити висновки, отримувати в результаті правильні
висловлювання. Тому логіка це наука, яка повинна містити список правил
отримання правильних висловлювань.
Алгоритмічні логіки
На початку 70-х років ХХ століття виникли алгоритмічні логіки. Вони були
створені з метою опису семантики мовою програмування.
Алгоритмічні логіки включають висловлювання вигляду
,
».
Ця логічна мова майже одночасно була створена Р.У.Флойдом (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]
Алгоритмічна логіка Хоара
Основою для логіки виведення правильних програм служать аксіоми Хоара.
Вони допускають інтерпретації в термінах програмних конструкцій.
: - R ????? - F H J L ¬ ® I I o oe o u jy R ????Сформулюємо аксіоми Хоара, які визначають передумови як достатні умови, які гарантують, що виконання відповідних операторів при вдалому завершенні приведе до бажаних після умов. [3] А1. Аксіома присвоювання: істинне перед виконанням. . Аксіома А5 відповідає інтерпретації умовного оператора в мові програмування. Сформулюємо правило для альтернативного оператора (повна форма умовного оператора): і для операторів циклу. Передумови та після умови циклу until (до) задовольняють правило: спочатку. Передумови і після умови циклу while (поки) задовольняють правило: Аксіоми А1 – А8 можна використовувати для перевірки узгодження передачі даних від оператора до оператора, для аналізу структурних властивостей текстів програм, для встановлення умов закінчення циклу. Крім того, правила можна використовувати для аналізу результатів виконання програми, що пов’язано з семантикою програми. Приклад. . Вхідні дані: > 0.
Вихідні дані:
— цілі невід’ємні числа.
:
:
— цілі числа.
:
Потрібно довести, що
або
Доведення.
А4 до пунктів 5 і 11
, яка задовольняє умови:
— цілі невід’ємні числа.
, і циклічний процес завершується.
Таким чином, встановлено, що
є тотально вірною.
Висновок
Отже, ми розглянули як застосовується логіка у простій мові
програмування та визначили її складність.
Застосування логічного алгоритму для вирішення конкретної задачі є
досить складною проблемою, вирішення якої потребує не лише досконалого
володіння саме цим алгоритмом, але й всебічного розглядання того чи
іншого алгоритму, тобто визначення усіх його переваг і недоліків.
Хоар визначив просту мову програмування через логічну систему аксіом і
правила виведення для доведення часткової правильності програми. В його
роботі показано, що для визначення семантики мови не в термінах
виконання програми, а в термінах доведення її правильності спрощує
процес створення програми.
Хоара проводив дослідження в області аксіомних визначень мови
програмування. Головним недоліком дослідників було те, що вони не
приділяли достатньо уваги формальній логіці. Основою для логіки
виведення правильних програм служать аксіоми Хоара.
Отже, головною задачею, яку має вирішити людина, створити сучасніший,
простіший метод доведення правильності програм. А також зазначити як
позитивні, так і усі негативні характеристики різних методів
розв’язування задач, з використанням алгоритмічних логік та з
передбаченням кінцевого результату.
Нашли опечатку? Выделите и нажмите CTRL+Enter
