'''Логіка Хоара''' (також відома як '''Флойда-ХоараГоара''') - це [[формальна система]] з множиною логічних правил для строгого доведення [[коректність програми|коректності програм]]. Запропонована в 1969 британськмим інформатиком та [[Математична логіка|логіком]] [[Тоні Хоар|ХоаромГоар]]ом, і пізніше вдосконалена ним же, та іншими дослідниками.<ref>[[Тоні ХоарГоар|C. A. R. Hoare]]. "[http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf An axiomatic basis for computer programming]". ''[[Communications of the ACM]]'', 12(10):576–580,583 October 1969. {{doi|10.1145/363235.363259}}</ref> Початкові ідеї були закладені в роботі [[Роберт Флойд|Роберта Флойда]], який опублікував подібну систему<ref>[[Роберт Флойд|R. W. Floyd]]. "[http://laser.cs.umass.edu/courses/cs521-621.Spr06/papers/Floyd.pdf Assigning meanings to programs.]" Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967.</ref> для [[Блок-схема|блок-схем]].
== Трійки ХоараГоара ==
Основним інструментом логіки ХоараГоара є '''трійки ХоараГоара'''. Трійки описують як виконання частини коду змінює стан програми. Їх записують в такій формі
:<math>\{P\}\;C\;\{Q\}</math>
Рядок 8:
де ''P'' та ''Q'' - ''[[Припущення (програмування)|припущення]]'' а ''C'' - команда . ''P'' - передумова ({{lang-en|precondition}}) а ''Q'' - післяумова ({{lang-en|postcondition}}): якщо виконується передумова, то команда приведе нас до виконання післяумови. Припущення є формулами [[логіка предикатів|логіки предикатів]].
Логіка ХоараГоара надає [[Аксіома|аксіоми]] та [[правила виведення]] для всіх конструкцій простих [[Імперативне програмування|імперативних мов програмування]]. На додачу до правил для імперативних мов в роботі ХоараГоара та пізніше ним й іншими були розроблені правила для інших мовних конструкцій. Існують правила для [[Паралелізм (інформатика)|паралелізму]], процедур <!-- [[procedure (computer science)|procedure]]s -->, переходів <!--[[jump (computer science)|jump]]s-->, та [[вказівник]]ів.
== Часткова та тотальна корректність ==
Звичайна логіка ХоараГоара доводить тільки часткову коректність, а завершуваність потрібно доводити окремо. Тому трійки ХоараГоара що задають часткову коректність треба читати так: Якщо ''P'' і ''C'' - завершується, то після цього ''Q''. Якщо ж ''C'' - не завершується, то ніякого "після" немає, і ''Q'' може бути яким завгодно. Можна навіть для позначення незавершимості ''C'' присвоїти ''Q'' False.
Також з додаванням розришення до правила про цикли можна доводити тотальну коректність. Тоді трійка ХоараГоара означає: "Якщо ''P'', то ''C'' завершується і ''Q''".
