Логіка Гоара

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

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

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

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

\{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.
  • Використано матеріали зі статті в англійській Вікіпедії.
  • Використано матеріали зі статті в [а) - це формальна система з множи англійській Вікіпедії].