Логіка Гоара

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

Логіка Хоара (також відома як Флойда-Гоара) - це формальна система з множиною логічних правил для строгого доведення коректності програм. Запропонована в 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.

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

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

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