Логіка Гоара

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

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

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

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

Тоні Гоар[ред.ред. код]

Сер Чарлз Ентоні Річард Гоар (англ. Charles Antony Richard Hoare або Tony Hoare або C.A.R. Hoare, народився 11 січня 1934, Коломбо, Цейлон, Британська імперія, сьогодні Шрі-Ланка) — англійський вчений, що працює в галузі інформатики та обчислювальної техніки. Найбільш відомий як розробник алгоритму «швидкого сортування» (англ. «quick sort»).

Інші відомі результати його праці: мова Z специфікацій та паралельна модель взаємодії послідовних процесів (CSP, Communicating Sequential Process). Серед його досягнень — розробка логіки Гоара, наукової основи для конструювання коректних програм, яка використовується для визначення та розробки мов програмування. Гоар написав низку праць зі створення специфікацій, проектування, реалізації та супроводу програм, що висвітлюють важливість наукових досліджень для збільшення продуктивності комп'ютерів та збільшення надійності програмного забезпечення.

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

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


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

 Для оператора присвоювання в постусловіем крім предусловия має враховувати факт, що значення змінної стало іншим.

 Для складеного оператора (в 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), чиє значення строго спадає згідно з en:well-founded relation протягом кожної ітерації. Через те що відношення "<" 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\}\ \! (Правило висновків)

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

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

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

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

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

Дивіться також[ред.ред. код]

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

  1. C. A. R. Hoare. "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576–580,583 October 1969. doi:10.1145/363235.363259
  2. R. W. Floyd. "Assigning meanings to programs." Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967.

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

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

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

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