Логіка Гоара

Алгоритмічна логіка Гоара (також відома як Флойда-Гоара) — це формальна система з множиною логічних правил для строгого доведення коректності програм^[en]. Запропонована в 1969 британським інформатиком та логіком Тоні Гоаром, і пізніше вдосконалена ним же, та іншими дослідниками.^[1] Початкові ідеї були закладені в роботі Роберта Флойда, який опублікував подібну систему^[2] для блок-схем.

Вступ[ред. | ред. код]

На початку 70-х років XX століття виникли алгоритмічні логіки. Вони були створені з метою опису семантики мовою програмування. Ця логічна мова майже одночасно була створена Р. У. Флойдом (1967), Тоні Гоаром (1969) і представниками польської логічної школи (А. Сальвініцький та інші (1970)). В 1969 році Гоар визначив просту мову програмування через логічну систему аксіом і правила виведення для доведення часткової правильності програми. В його роботі показано, що для визначення семантики мови не в термінах виконання програми, а в термінах доведення її правильності, спрощує процес створення програми. В 70-х роках на базі роботи Гоара починаються дослідження в області аксіомних визначень мови програмування. З'являється багато робіт з аксіоматизації різних конструкцій: від оператора присвоювання до різних форм циклів, від виклику процедур до співпрограм. Головним недоліком дослідників в ті роки було те, що вони не приділяли достатньо уваги формальній логіці. В 1972 році вийшла чергова стаття Гоара про доказ правильного подання даних, що прискорило дослідження абстрактних типів даних. В СРСР роботи в цій області проводились в Новосибірську (А. П. Єршов, В. Н. Агафонов, А. В. Замулин, И. Н. Скопина). В 1973 році були сформульовані правила доведення правильності для більшості конструкцій мови Паскаль. В 1975 році була побудована автоматична система «верифікації для підмножини» мови Паскаль, заснована на аксіомах і правилах виведення. В 1979 році була визначена мова програмування Евкліда, в проект якого з самого початку була закладена ідея аксіоматизації. В 1976 році вийшла книга Е. Дейкстри «Дисципліна програмування», в якій пропонується метод доведення правильності програми. Суть методу полягає в тому, щоб будувати програму разом з доведенням, причому доведення повинно випереджати побудову програми. Е.Дейкстр визначив для простої мови програмування слабкі передбачення і показав, як їх можна використовувати як підрахування для виведення програми. Стало зрозуміло, що користування формалізмом може призвести до побудови програм більш надійним способом."

Основні ідеї Гоара[ред. | ред. код]

Основна ідея Гоара дати для кожної конструкції імперативного мови перед і пост-умови записане у вигляді логічної формули. Тому і виникає у назві трійка — передумова, конструкція мови, пост-умовою.

Ясно, що для порожнього оператора перед і постумови збігаються.
Для оператора присвоювання постумова окрім передумови має враховувати факт, що значення змінної стало іншим.
Для складеного оператора (в Python це відступи, в C це {}) маємо ланцюжок передумов і постумов. У результаті для складеного оператора можна залишити першу передумову і останню постумову.
Правило виводу каже, що можна підсилити перед і послабити постумову якщо нам це знадобитися. Немає сенсу волокти через всю програму якесь твердження, яке не допомагає вирішити поставлене завдання.
Оператор розгалуження або просто if. Його умовно можна розбити на дві гілки then і else. Якщо до передумови додати істинність логічного умови (те, що стоїть під if), то після виконання гілки then повинна слідувати постумова. Аналогічно, якщо до передумовою додати заперечення логічного умови (те, що стоїть під if), то після виконання гілки else має слідувати постумова.
Оператор циклу. Це найнетривіальніше і найскладніше, оскільки цикл може виконується багато разів і навіть не скінчиться. Щоб вирішити проблему можливо багаторазового повтору тіла циклу вводять інваріант циклу. Інваріант циклу це те, що істинно перед його виконанням, істинно після кожного виконання тіла циклу і отже істинно і після його закінчення. Передумова для оператора циклу це просто його інваріант циклу. Якщо істинна умова продовження циклу (те, що стоїть під while), то після виконання тіла циклу повинна слідувати істинність інваріант циклу. В результаті після закінчення циклу маємо як постумову істинність інваріанту циклу і заперечення умови продовження циклу.
Оператора циклу з повною коректністю. Для цього до попереднього пункту додають обмежувальну функцію, за допомогою якої легко довести, що цикл буде виконуватися обмежену кількість разів. На неї накладають умови, що вона завжди >=\ 0, суворо убуває після кожного виконання тіла циклу і в точності =\ 0, коли цикл закінчується.
Програму, що працює правильно можна написати дуже багатьма способами, а також вона у великій кількості випадків буде ефективною. Це свавілля і саме воно він ускладнює програмування. Для цього вводять стиль. Але цього виявляється мало. Для багатьох програм (наприклад, пов'язаних побічно з життям людини) потрібно довести і їх коректність. Виявилося, що доказ коректності робить програму дорожче на порядок (приблизно в 10 разів).

Трійки Гоара[ред. | ред. код]

Основним інструментом логіки Гоара є трійки Гоара. Трійки описують як виконання частини коду змінює стан програми. Їх записують в такій формі

\{P\}\;C\;\{Q\}

де P та Q — припущення а C — команда. P — передумова (англ. precondition) а Q — післяумова (англ. postcondition): якщо виконується передумова, то команда приведе нас до виконання післяумови. Припущення є формулами логіки предикатів.

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

Часткова та тотальна коректність[ред. | ред. код]

Звичайна логіка Гоара доводить тільки часткову коректність, а завершуваність потрібно доводити окремо. Тому трійки Гоара що задають часткову коректність треба читати так: Якщо P і C — завершується, то після цього Q. Якщо ж C — не завершується, то ніякого «після» немає, і Q може бути яким завгодно. Можна навіть для позначення незавершимості C присвоїти Q False.

Також з додаванням розширення до правила про цикли можна доводити тотальну коректність. Тоді трійка Гоара означає: «Якщо P, то C завершується і Q».

Правила[ред. | ред. код]

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

Аксіома про порожній оператор[ред. | ред. код]

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

{\frac {}{\{P\}\ {\textbf {skip}}\ \{P\}}}\!

Аксіома про присвоєння[ред. | ред. код]

Аксіома про присвоєння каже що після присвоєння для змінної виконується предикат, який виконувався для правої частини оператора присвоєння:

{\frac {}{\{P[E/x]\}\ x:=E\ \{P\}}}\!

Тут $P[E/x]$ позначає вираз P у якому всі вільні входження змінної x були замінені виразом E.

Аксіома про присвоєння означає що істинність $\{P[E/x]\}$ еквівалентна істинності $\{P\}$ після присвоєння. Тобто якщо $\{P[E/x]\}$ була істинна до присвоєння, то $\{P\}$ буде після. І навпаки, якщо $\{P[E/x]\}$ була хибною до присвоєння, то $\{P\}$ теж має бути хибною після.

Приклади правильних трійок:

$\{x+1=43\}\ y:=x+1\ \{y=43\}\!$
$\{x+1\leq N\}\ x:=x+1\ \{x\leq N\}\ \!$

Правило композиції[ред. | ред. код]

Правило композиції застосовується до послідовно виконуваних програм S та T, де S виконується до T і записується S;T.

{\frac {\{P\}\ S\ \{Q\}\ ,\ \{Q\}\ T\ \{R\}}{\{P\}\ S;T\ \{R\}}}\!

Наприклад, розглянемо такі два присвоєння:

\{x+1=43\}\ y:=x+1\ \{y=43\}

та

\{y=43\}\ z:=y\ \{z=43\}

З правила композиції:

\{x+1=43\}\ y:=x+1;z:=y\ \{z=43\}

Правило умови[ред. | ред. код]

З трійки для умовного оператора можна вивести дві трійки: одну для випадку істинності умови, іншу для її хибності:

{\frac {\{B\wedge P\}\ S\ \{Q\}\ ,\ \{\neg B\wedge P\}\ T\ \{Q\}}{\{P\}\ {\textbf {if}}\ B\ {\textbf {then}}\ S\ {\textbf {else}}\ T\ {\textbf {endif}}\ \{Q\}}}\!

Правило висновків[ред. | ред. код]

Передумову та/або постумову можна замінити, якщо для них виконуються певні імплікації:

{\frac {P^{\prime }\rightarrow \ P\ ,\ \lbrace P\rbrace \ S\ \lbrace Q\rbrace \ ,\ Q\rightarrow \ Q^{\prime }}{\lbrace P^{\prime }\ \rbrace \ S\ \lbrace Q^{\prime }\rbrace }}\!

Правило While[ред. | ред. код]

{\frac {\{P\wedge B\}\ S\ \{P\}}{\{P\}\ {\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {done}}\ \{\neg B\wedge P\}}}\!

Тут P інваріант циклу.

Правило While для тотальної коректності[ред. | ред. код]

{\frac {<\;{\textrm {is\ well-founded,}}\;[P\wedge B\wedge t=z]\ S\ [P\wedge t<z]}{[P]\ {\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {done}}\ [\neg B\wedge P]}}\!

В цьому правилі на додачу до інваріанта циклу, також доводять завершуваність додаванням варіанта циклу (тут t), чиє значення строго спадає згідно з фундованим відношенням протягом кожної ітерації. Через те що відношення «<» well-founded, кожна ітерація циклу перелічується спадними членами скінченного ланцюга. Також зауважте, що тут для позначення тотальної коректності використовуються квадратні дужки. (Це одне з можливих позначень тотальної коректності.)

Аксіоми можна використовувати для перевірки узгодженості передачі даних від оператора до оператора, для аналізу структурних властивостей текстів програм, для встановлення умов закінчення циклу. Крім того, правила можна використовувати для аналізу результатів виконання програми, що пов'язано з семантикою програми.

Приклади[ред. | ред. код]

Приклад 1
$\{x+1=43\}\!$	$\ y:=x+1\ \!$	$\{y=43\}\!$	(Аксіома присвоєння)
			$(x+1=43\Leftrightarrow x=42)$
$\{x=42\}\!$	$\ y:=x+1\ \!$	$\{y=43\land x=42\}\!$	(Правило висновків)
Приклад 2
$\{x+1\leq N\}\!$	$\ x:=x+1\ \!$	$\{x\leq N\}\ \!$	(Аксіома присвоєння)
			( $x<N\implies x+1\leq N$ для цілих x, N)
$\{x<N\}\!$	$\ x:=x+1\ \!$	$\{x\leq N\}\ \!$	(Правило висновків)

Висновки[ред. | ред. код]

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

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

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

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

Див. також[ред. | ред. код]

Зноски[ред. | ред. код]

↑ C. A. R. Hoare. «An axiomatic basis for computer programming [Архівовано 17 липня 2011 у Wayback Machine.]». Communications of the ACM, 12(10):576-580,583 October 1969. DOI:10.1145/363235.363259
↑ R. W. Floyd. «Assigning meanings to programs. [Архівовано 9 грудня 2008 у Wayback Machine.]» Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19-31. 1967.

Література[ред. | ред. код]

Robert D. Tennent. Specifying Software [Архівовано 23 лютого 2003 у Wayback Machine.] (підручник що включає вступ до логіки Гоара, 2002 рік) ISBN 0-521-00401-2
А. К. Гуц, Математична логіка і теорія алгоритмів, Видавництво Спадок. Омськ, 2003 р.

Посилання[ред. | ред. код]

Project Bali описав подібні правила для підмножини мови Java для використання з системою доведення теорем Isabelle
j-Algo-modul Hoare calculus [Архівовано 5 травня 2011 у Wayback Machine.] — Візуалізація числення Гоара в програмі візуалізації алгоритмів j-Algo
KeY-Hoare напівавтоматична система верифікації що побудована на базі системи доведення теорем KeY.
Використано матеріали зі статті в формальна система з англійської Вікіпедії.

[1] C. A. R. Hoare. «An axiomatic basis for computer programming [Архівовано 17 липня 2011 у Wayback Machine.]». Communications of the ACM, 12(10):576-580,583 October 1969. DOI:10.1145/363235.363259

[2] R. W. Floyd. «Assigning meanings to programs. [Архівовано 9 грудня 2008 у Wayback Machine.]» Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19-31. 1967.

[1]

[2]