Алгоритмічна логіка Гоара (також відома як Флойда-Гоара) — це формальна система з множиною логічних правил для строгого доведення коректності програм.
Запропонована в 1969 британським інформатиком та логіком Тоні Гоаром, і пізніше вдосконалена ним же, та іншими дослідниками. Початкові ідеї були закладені в роботі Роберта Флойда, який опублікував подібну систему для блок-схем.
На початку 70-х років XX століття виникли алгоритмічні логіки. Вони були створені з метою опису семантики мовою програмування. Ця логічна мова майже одночасно була створена Р. У. Флойдом (1967), Тоні Гоаром (1969) і представниками польської логічної школи (А. Сальвініцький та інші (1970)). В 1969 році Гоар визначив просту мову програмування через логічну систему аксіом і правила виведення для доведення часткової правильності програми. В його роботі показано, що для визначення семантики мови не в термінах виконання програми, а в термінах доведення її правильності, спрощує процес створення програми. В 70-х роках на базі роботи Гоара починаються дослідження в області аксіомних визначень мови програмування. З'являється багато робіт з аксіоматизації різних конструкцій: від оператора присвоювання до різних форм циклів, від виклику процедур до співпрограм. Головним недоліком дослідників в ті роки було те, що вони не приділяли достатньо уваги формальній логіці. В 1972 році вийшла чергова стаття Гоара про доказ правильного подання даних, що прискорило дослідження абстрактних типів даних. В СРСР роботи в цій області проводились в Новосибірську (А. П. Єршов, В. Н. Агафонов, А. В. Замулин, И. Н. Скопина). В 1973 році були сформульовані правила доведення правильності для більшості конструкцій мови Паскаль. В 1975 році була побудована автоматична система «верифікації для підмножини» мови Паскаль, заснована на аксіомах і правилах виведення. В 1979 році була визначена мова програмування Евкліда, в проект якого з самого початку була закладена ідея аксіоматизації. В 1976 році вийшла книга Е. Дейкстри «Дисципліна програмування», в якій пропонується метод доведення правильності програми. Суть методу полягає в тому, щоб будувати програму разом з доведенням, причому доведення повинно випереджати побудову програми. Е.Дейкстр визначив для простої мови програмування слабкі передбачення і показав, як їх можна використовувати як підрахування для виведення програми. Стало зрозуміло, що користування формалізмом може призвести до побудови програм більш надійним способом."
Основна ідея Гоара дати для кожної конструкції імперативного мови перед і пост-умови записане у вигляді логічної формули. Тому і виникає у назві трійка — передумова, конструкція мови, пост-умовою.
Основним інструментом логіки Гоара є трійки Гоара. Трійки описують як виконання частини коду змінює стан програми. Їх записують в такій формі
де P та Q — припущення а C — команда. P — передумова (англ. precondition) а Q — післяумова (англ. postcondition): якщо виконується передумова, то команда приведе нас до виконання післяумови. Припущення є формулами логіки предикатів.
Логіка Гоара надає аксіоми та правила виведення для всіх конструкцій простих імперативних мов програмування. На додачу до правил для імперативних мов в роботі Гоара та пізніше ним й іншими були розроблені правила для інших мовних конструкцій. Існують правила для паралелізму, процедур , переходів , та вказівників.
Звичайна логіка Гоара доводить тільки часткову коректність, а завершуваність потрібно доводити окремо. Тому трійки Гоара що задають часткову коректність треба читати так: Якщо P і C — завершується, то після цього Q. Якщо ж C — не завершується, то ніякого «після» немає, і Q може бути яким завгодно. Можна навіть для позначення незавершимості C присвоїти Q False.
Також з додаванням розширення до правила про цикли можна доводити тотальну коректність. Тоді трійка Гоара означає: «Якщо P, то C завершується і Q».
Основою для логіки виведення правильних програм служать аксіоми Гоара. Вони допускають інтерпретації в термінах програмних конструкцій. Сформулюємо аксіоми Гоара, які визначають передумови як достатні умови, які гарантують, що виконання відповідних операторів при вдалому завершенні приведе до бажаних після умов.
Аксіома про порожній оператор каже нам що він не змінює стан програми, тому що було правдою до його виконання, залишається таким же і після.
Аксіома про присвоєння каже що після присвоєння для змінної виконується предикат, який виконувався для правої частини оператора присвоєння:
Тут позначає вираз P у якому всі вільні входження змінної x були замінені виразом E.
Аксіома про присвоєння означає що істинність еквівалентна істинності після присвоєння. Тобто якщо була істинна до присвоєння, то буде після. І навпаки, якщо була хибною до присвоєння, то теж має бути хибною після.
Приклади правильних трійок:
Правило композиції застосовується до послідовно виконуваних програм S та T, де S виконується до T і записується S;T.
Наприклад, розглянемо такі два присвоєння:
та
З правила композиції:
З трійки для умовного оператора можна вивести дві трійки: одну для випадку істинності умови, іншу для її хибності:
Передумову та/або постумову можна замінити, якщо для них виконуються певні імплікації:
Тут P інваріант циклу.
Аксіоми можна використовувати для перевірки узгодженості передачі даних від оператора до оператора, для аналізу структурних властивостей текстів програм, для встановлення умов закінчення циклу. Крім того, правила можна використовувати для аналізу результатів виконання програми, що пов'язано з семантикою програми.
Приклад 1 | |||
(Аксіома присвоєння) | |||
(Правило висновків) | |||
Приклад 2 | |||
(Аксіома присвоєння) | |||
( для цілих x, N) | |||
(Правило висновків) |
Отже, ми розглянули як застосовується логіка у простій мові програмування та визначили її складність.
Застосування логічного алгоритму для вирішення конкретної задачі є досить складною проблемою, вирішення якої потребує не лише досконалого володіння саме цим алгоритмом, але й всебічного розглядання того чи іншого алгоритму, тобто визначення усіх його переваг і недоліків. Гоар визначив просту мову програмування через логічну систему аксіом і правила виведення для доведення часткової правильності програми. В його роботі показано, що для визначення семантики мови не в термінах виконання програми, а в термінах доведення її правильності спрощує процес створення програми.
Гоар проводив дослідження в області аксіомних визначень мови програмування. Головним недоліком дослідників було те, що вони не приділяли достатньо уваги формальній логіці. Основою для логіки виведення правильних програм служать аксіоми Гоара.
Отже, головною задачею, яку має вирішити людина, створити сучасніший, простіший метод доведення правильності програм. А також зазначити як позитивні, так і усі негативні характеристики різних методів розв'язування задач, з використанням алгоритмічних логік та з передбаченням кінцевого результату.
This article uses material from the Wikipedia Українська article Логіка Гоара, which is released under the Creative Commons Attribution-ShareAlike 3.0 license ("CC BY-SA 3.0"); additional terms may apply (view authors). Вміст доступний на умовах CC BY-SA 4.0, якщо не вказано інше. Images, videos and audio are available under their respective licenses.
®Wikipedia is a registered trademark of the Wiki Foundation, Inc. Wiki Українська (DUHOCTRUNGQUOC.VN) is an independent company and has no affiliation with Wiki Foundation.