ReferatFolder.Org.Ua — Папка українських рефератів!


Загрузка...

Головна Логіка → Алгоритмічна логіка Хоара

Реферат на тему:

Алгоритмічна логіка Хоара

План

        1. Вступ

        2. Алгоритмічні логіки

        3. Біографія Хоара

        4. Алгоритмічна логіка Хоара

  1. Аксіоми Хоара;

  2. Приклад розв\'язування задачі з використанням аксіом.

        1. Висновок

Вступ

Логіка – це теорія, яка вивчає, як правильно потрібно міркувати, правильно робити висновки, отримувати в результаті правильні висловлювання. Тому логіка це наука, яка повинна містити список правил отримання правильних висловлювань.

Алгоритмічні логіки

На початку 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. Аксіома присвоювання:

Неформальне пояснення аксіоми: так як Алгоритмічна логіка Хоара після виконання буде містити значення Алгоритмічна логіка Хоара , тоді Алгоритмічна логіка Хоара буде істинне після виконання, якщо результат підстановки замість в істинне перед виконанням.