Алгоритмічна логіка Гоара (також відома як Флойда-Гоара) — це формальна система з множиною логічних правил для строгого доведення [en]. Запропонована в 1969 британським інформатиком та логіком Тоні Гоаром, і пізніше вдосконалена ним же, та іншими дослідниками. Початкові ідеї були закладені в роботі Роберта Флойда, який опублікував подібну систему для блок-схем.
Вступ
На початку 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 та Q — припущення а C — команда. P — передумова (англ. precondition) а Q — післяумова (англ. postcondition): якщо виконується передумова, то команда приведе нас до виконання післяумови. Припущення є формулами логіки предикатів.
Логіка Гоара надає аксіоми та правила виведення для всіх конструкцій простих імперативних мов програмування. На додачу до правил для імперативних мов в роботі Гоара та пізніше ним й іншими були розроблені правила для інших мовних конструкцій. Існують правила для паралелізму, процедур , переходів , та вказівників.
Часткова та тотальна коректність
Звичайна логіка Гоара доводить тільки часткову коректність, а завершуваність потрібно доводити окремо. Тому трійки Гоара що задають часткову коректність треба читати так: Якщо P і C — завершується, то після цього Q. Якщо ж C — не завершується, то ніякого «після» немає, і Q може бути яким завгодно. Можна навіть для позначення незавершимості C присвоїти Q False.
Також з додаванням розширення до правила про цикли можна доводити тотальну коректність. Тоді трійка Гоара означає: «Якщо P, то C завершується і Q».
Правила
Основою для логіки виведення правильних програм служать аксіоми Гоара. Вони допускають інтерпретації в термінах програмних конструкцій. Сформулюємо аксіоми Гоара, які визначають передумови як достатні умови, які гарантують, що виконання відповідних операторів при вдалому завершенні приведе до бажаних після умов.
Аксіома про порожній оператор
Аксіома про порожній оператор каже нам що він не змінює стан програми, тому що було правдою до його виконання, залишається таким же і після.
Аксіома про присвоєння
Аксіома про присвоєння каже що після присвоєння для змінної виконується предикат, який виконувався для правої частини оператора присвоєння:
Тут позначає вираз P у якому всі вільні входження змінної x були замінені виразом E.
Аксіома про присвоєння означає що істинність еквівалентна істинності після присвоєння. Тобто якщо була істинна до присвоєння, то буде після. І навпаки, якщо була хибною до присвоєння, то теж має бути хибною після.
Приклади правильних трійок:
Правило композиції
Правило композиції застосовується до послідовно виконуваних програм S та T, де S виконується до T і записується S;T.
Наприклад, розглянемо такі два присвоєння:
та
З правила композиції:
Правило умови
З трійки для умовного оператора можна вивести дві трійки: одну для випадку істинності умови, іншу для її хибності:
Правило висновків
Передумову та/або постумову можна замінити, якщо для них виконуються певні імплікації:
Правило While
Тут P .
Правило While для тотальної коректності
- В цьому правилі на додачу до інваріанта циклу, також доводять завершуваність додаванням (тут t), чиє значення строго спадає згідно з фундованим відношенням протягом кожної ітерації. Через те що відношення «<» well-founded, кожна ітерація циклу перелічується спадними членами скінченного ланцюга. Також зауважте, що тут для позначення тотальної коректності використовуються квадратні дужки. (Це одне з можливих позначень тотальної коректності.)
Аксіоми можна використовувати для перевірки узгодженості передачі даних від оператора до оператора, для аналізу структурних властивостей текстів програм, для встановлення умов закінчення циклу. Крім того, правила можна використовувати для аналізу результатів виконання програми, що пов'язано з семантикою програми.
Приклади
Приклад 1 (Аксіома присвоєння) (Правило висновків) Приклад 2 (Аксіома присвоєння) ( для цілих x, 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 рік)
- А. К. Гуц, Математична логіка і теорія алгоритмів, Видавництво Спадок. Омськ, 2003 р.
Посилання
- описав подібні правила для підмножини мови Java для використання з системою доведення теорем
- j-Algo-modul Hoare calculus [ 5 травня 2011 у Wayback Machine.] — Візуалізація числення Гоара в програмі візуалізації алгоритмів j-Algo
- напівавтоматична система верифікації що побудована на базі системи доведення теорем .
- Використано матеріали зі статті в формальна система з англійської Вікіпедії.
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
Algoritmichna logika Goara takozh vidoma yak Flojda Goara ce formalna sistema z mnozhinoyu logichnih pravil dlya strogogo dovedennya en Zaproponovana v 1969 britanskim informatikom ta logikom Toni Goarom i piznishe vdoskonalena nim zhe ta inshimi doslidnikami Pochatkovi ideyi buli zakladeni v roboti Roberta Flojda yakij opublikuvav podibnu sistemu dlya blok shem VstupNa pochatku 70 h rokiv XX stolittya vinikli algoritmichni logiki Voni buli stvoreni z metoyu opisu semantiki movoyu programuvannya Cya logichna mova majzhe odnochasno bula stvorena R U Flojdom 1967 Toni Goarom 1969 i predstavnikami polskoyi logichnoyi shkoli A ta inshi 1970 V 1969 roci Goar viznachiv prostu movu programuvannya cherez logichnu sistemu aksiom i pravila vivedennya dlya dovedennya chastkovoyi pravilnosti programi V jogo roboti pokazano sho dlya viznachennya semantiki movi ne v terminah vikonannya programi a v terminah dovedennya yiyi pravilnosti sproshuye proces stvorennya programi V 70 h rokah na bazi roboti Goara pochinayutsya doslidzhennya v oblasti aksiomnih viznachen movi programuvannya Z yavlyayetsya bagato robit z aksiomatizaciyi riznih konstrukcij vid operatora prisvoyuvannya do riznih form cikliv vid vikliku procedur do spivprogram Golovnim nedolikom doslidnikiv v ti roki bulo te sho voni ne pridilyali dostatno uvagi formalnij logici V 1972 roci vijshla chergova stattya Goara pro dokaz pravilnogo podannya danih sho priskorilo doslidzhennya abstraktnih tipiv danih V SRSR roboti v cij oblasti provodilis v Novosibirsku A P Yershov V N Agafonov A V Zamulin I N Skopina V 1973 roci buli sformulovani pravila dovedennya pravilnosti dlya bilshosti konstrukcij movi Paskal V 1975 roci bula pobudovana avtomatichna sistema verifikaciyi dlya pidmnozhini movi Paskal zasnovana na aksiomah i pravilah vivedennya V 1979 roci bula viznachena mova programuvannya Evklida v proekt yakogo z samogo pochatku bula zakladena ideya aksiomatizaciyi V 1976 roci vijshla kniga E Dejkstri Disciplina programuvannya v yakij proponuyetsya metod dovedennya pravilnosti programi Sut metodu polyagaye v tomu shob buduvati programu razom z dovedennyam prichomu dovedennya povinno viperedzhati pobudovu programi E Dejkstr viznachiv dlya prostoyi movi programuvannya slabki peredbachennya i pokazav yak yih mozhna vikoristovuvati yak pidrahuvannya dlya vivedennya programi Stalo zrozumilo sho koristuvannya formalizmom mozhe prizvesti do pobudovi program bilsh nadijnim sposobom Osnovni ideyi GoaraOsnovna ideya Goara dati dlya kozhnoyi konstrukciyi imperativnogo movi pered i post umovi zapisane u viglyadi logichnoyi formuli Tomu i vinikaye u nazvi trijka peredumova konstrukciya movi post umovoyu Yasno sho dlya porozhnogo operatora pered i postumovi zbigayutsya Dlya operatora prisvoyuvannya postumova okrim peredumovi maye vrahovuvati fakt sho znachennya zminnoyi stalo inshim Dlya skladenogo operatora v Python ce vidstupi v C ce mayemo lancyuzhok peredumov i postumov U rezultati dlya skladenogo operatora mozhna zalishiti pershu peredumovu i ostannyu postumovu Pravilo vivodu kazhe sho mozhna pidsiliti pered i poslabiti postumovu yaksho nam ce znadobitisya Nemaye sensu volokti cherez vsyu programu yakes tverdzhennya yake ne dopomagaye virishiti postavlene zavdannya Operator rozgaluzhennya abo prosto if Jogo umovno mozhna rozbiti na dvi gilki then i else Yaksho do peredumovi dodati istinnist logichnogo umovi te sho stoyit pid if to pislya vikonannya gilki then povinna sliduvati postumova Analogichno yaksho do peredumovoyu dodati zaperechennya logichnogo umovi te sho stoyit pid if to pislya vikonannya gilki else maye sliduvati postumova Operator ciklu Ce najnetrivialnishe i najskladnishe oskilki cikl mozhe vikonuyetsya bagato raziv i navit ne skinchitsya Shob virishiti problemu mozhlivo bagatorazovogo povtoru tila ciklu vvodyat invariant ciklu Invariant ciklu ce te sho istinno pered jogo vikonannyam istinno pislya kozhnogo vikonannya tila ciklu i otzhe istinno i pislya jogo zakinchennya Peredumova dlya operatora ciklu ce prosto jogo invariant ciklu Yaksho istinna umova prodovzhennya ciklu te sho stoyit pid while to pislya vikonannya tila ciklu povinna sliduvati istinnist invariant ciklu V rezultati pislya zakinchennya ciklu mayemo yak postumovu istinnist invariantu ciklu i zaperechennya umovi prodovzhennya ciklu Operatora ciklu z povnoyu korektnistyu Dlya cogo do poperednogo punktu dodayut obmezhuvalnu funkciyu za dopomogoyu yakoyi legko dovesti sho cikl bude vikonuvatisya obmezhenu kilkist raziv Na neyi nakladayut umovi sho vona zavzhdi gt 0 suvoro ubuvaye pislya kozhnogo vikonannya tila ciklu i v tochnosti 0 koli cikl zakinchuyetsya Programu sho pracyuye pravilno mozhna napisati duzhe bagatma sposobami a takozh vona u velikij kilkosti vipadkiv bude efektivnoyu Ce svavillya i same vono vin uskladnyuye programuvannya Dlya cogo vvodyat stil Ale cogo viyavlyayetsya malo Dlya bagatoh program napriklad pov yazanih pobichno z zhittyam lyudini potribno dovesti i yih korektnist Viyavilosya sho dokaz korektnosti robit programu dorozhche na poryadok priblizno v 10 raziv Trijki GoaraOsnovnim instrumentom logiki Goara ye trijki Goara Trijki opisuyut yak vikonannya chastini kodu zminyuye stan programi Yih zapisuyut v takij formi P C Q displaystyle P C Q de P ta Q pripushennya a C komanda P peredumova angl precondition a Q pislyaumova angl postcondition yaksho vikonuyetsya peredumova to komanda privede nas do vikonannya pislyaumovi Pripushennya ye formulami logiki predikativ Logika Goara nadaye aksiomi ta pravila vivedennya dlya vsih konstrukcij prostih imperativnih mov programuvannya Na dodachu do pravil dlya imperativnih mov v roboti Goara ta piznishe nim j inshimi buli rozrobleni pravila dlya inshih movnih konstrukcij Isnuyut pravila dlya paralelizmu procedur perehodiv ta vkazivnikiv Chastkova ta totalna korektnistZvichajna logika Goara dovodit tilki chastkovu korektnist a zavershuvanist potribno dovoditi okremo Tomu trijki Goara sho zadayut chastkovu korektnist treba chitati tak Yaksho P i C zavershuyetsya to pislya cogo Q Yaksho zh C ne zavershuyetsya to niyakogo pislya nemaye i Q mozhe buti yakim zavgodno Mozhna navit dlya poznachennya nezavershimosti C prisvoyiti Q False Takozh z dodavannyam rozshirennya do pravila pro cikli mozhna dovoditi totalnu korektnist Todi trijka Goara oznachaye Yaksho P to C zavershuyetsya i Q PravilaOsnovoyu dlya logiki vivedennya pravilnih program sluzhat aksiomi Goara Voni dopuskayut interpretaciyi v terminah programnih konstrukcij Sformulyuyemo aksiomi Goara yaki viznachayut peredumovi yak dostatni umovi yaki garantuyut sho vikonannya vidpovidnih operatoriv pri vdalomu zavershenni privede do bazhanih pislya umov Aksioma pro porozhnij operator Aksioma pro porozhnij operator kazhe nam sho vin ne zminyuye stan programi tomu sho bulo pravdoyu do jogo vikonannya zalishayetsya takim zhe i pislya P skip P displaystyle frac P textbf skip P Aksioma pro prisvoyennya Aksioma pro prisvoyennya kazhe sho pislya prisvoyennya dlya zminnoyi vikonuyetsya predikat yakij vikonuvavsya dlya pravoyi chastini operatora prisvoyennya P E x x E P displaystyle frac P E x x E P Tut P E x displaystyle P E x poznachaye viraz P u yakomu vsi vilni vhodzhennya zminnoyi x buli zamineni virazom E Aksioma pro prisvoyennya oznachaye sho istinnist P E x displaystyle P E x ekvivalentna istinnosti P displaystyle P pislya prisvoyennya Tobto yaksho P E x displaystyle P E x bula istinna do prisvoyennya to P displaystyle P bude pislya I navpaki yaksho P E x displaystyle P E x bula hibnoyu do prisvoyennya to P displaystyle P tezh maye buti hibnoyu pislya Prikladi pravilnih trijok x 1 43 y x 1 y 43 displaystyle x 1 43 y x 1 y 43 x 1 N x x 1 x N displaystyle x 1 leq N x x 1 x leq N Pravilo kompoziciyi Pravilo kompoziciyi zastosovuyetsya do poslidovno vikonuvanih program S ta T de S vikonuyetsya do T i zapisuyetsya S T P S Q Q T R P S T R displaystyle frac P S Q Q T R P S T R Napriklad rozglyanemo taki dva prisvoyennya x 1 43 y x 1 y 43 displaystyle x 1 43 y x 1 y 43 ta y 43 z y z 43 displaystyle y 43 z y z 43 Z pravila kompoziciyi x 1 43 y x 1 z y z 43 displaystyle x 1 43 y x 1 z y z 43 Pravilo umovi Z trijki dlya umovnogo operatora mozhna vivesti dvi trijki odnu dlya vipadku istinnosti umovi inshu dlya yiyi hibnosti B P S Q B P T Q P if B then S else T endif Q displaystyle 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 Pravilo visnovkiv Peredumovu ta abo postumovu mozhna zaminiti yaksho dlya nih vikonuyutsya pevni implikaciyi P P P S Q Q Q P S Q displaystyle 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 Pravilo While P B S P P while B do S done B P displaystyle frac P wedge B S P P textbf while B textbf do S textbf done neg B wedge P Tut P Pravilo While dlya totalnoyi korektnosti lt is well founded P B t z S P t lt z P while B do S done B P displaystyle frac lt textrm is well founded P wedge B wedge t z S P wedge t lt z P textbf while B textbf do S textbf done neg B wedge P V comu pravili na dodachu do invarianta ciklu takozh dovodyat zavershuvanist dodavannyam tut t chiye znachennya strogo spadaye zgidno z fundovanim vidnoshennyam protyagom kozhnoyi iteraciyi Cherez te sho vidnoshennya lt well founded kozhna iteraciya ciklu perelichuyetsya spadnimi chlenami skinchennogo lancyuga Takozh zauvazhte sho tut dlya poznachennya totalnoyi korektnosti vikoristovuyutsya kvadratni duzhki Ce odne z mozhlivih poznachen totalnoyi korektnosti dd Aksiomi mozhna vikoristovuvati dlya perevirki uzgodzhenosti peredachi danih vid operatora do operatora dlya analizu strukturnih vlastivostej tekstiv program dlya vstanovlennya umov zakinchennya ciklu Krim togo pravila mozhna vikoristovuvati dlya analizu rezultativ vikonannya programi sho pov yazano z semantikoyu programi dd PrikladiPriklad 1 x 1 43 displaystyle x 1 43 y x 1 displaystyle y x 1 y 43 displaystyle y 43 Aksioma prisvoyennya x 1 43 x 42 displaystyle x 1 43 Leftrightarrow x 42 x 42 displaystyle x 42 y x 1 displaystyle y x 1 y 43 x 42 displaystyle y 43 land x 42 Pravilo visnovkiv Priklad 2 x 1 N displaystyle x 1 leq N x x 1 displaystyle x x 1 x N displaystyle x leq N Aksioma prisvoyennya x lt N x 1 N displaystyle x lt N implies x 1 leq N dlya cilih x N x lt N displaystyle x lt N x x 1 displaystyle x x 1 x N displaystyle x leq N Pravilo visnovkiv VisnovkiOtzhe mi rozglyanuli yak zastosovuyetsya logika u prostij movi programuvannya ta viznachili yiyi skladnist Zastosuvannya logichnogo algoritmu dlya virishennya konkretnoyi zadachi ye dosit skladnoyu problemoyu virishennya yakoyi potrebuye ne lishe doskonalogo volodinnya same cim algoritmom ale j vsebichnogo rozglyadannya togo chi inshogo algoritmu tobto viznachennya usih jogo perevag i nedolikiv Goar viznachiv prostu movu programuvannya cherez logichnu sistemu aksiom i pravila vivedennya dlya dovedennya chastkovoyi pravilnosti programi V jogo roboti pokazano sho dlya viznachennya semantiki movi ne v terminah vikonannya programi a v terminah dovedennya yiyi pravilnosti sproshuye proces stvorennya programi Goar provodiv doslidzhennya v oblasti aksiomnih viznachen movi programuvannya Golovnim nedolikom doslidnikiv bulo te sho voni ne pridilyali dostatno uvagi formalnij logici Osnovoyu dlya logiki vivedennya pravilnih program sluzhat aksiomi Goara Otzhe golovnoyu zadacheyu yaku maye virishiti lyudina stvoriti suchasnishij prostishij metod dovedennya pravilnosti program A takozh zaznachiti yak pozitivni tak i usi negativni harakteristiki riznih metodiv rozv yazuvannya zadach z vikoristannyam algoritmichnih logik ta z peredbachennyam kincevogo rezultatu Div takozhChislennya sekvencij Denotacijna semantika Edsger Dejkstra Formalna verifikaciyaZnoskiC A R Hoare An axiomatic basis for computer programming 17 lipnya 2011 u 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 grudnya 2008 u Wayback Machine Proceedings of the American Mathematical Society Symposia on Applied Mathematics Vol 19 pp 19 31 1967 LiteraturaRobert D Tennent Specifying Software 23 lyutogo 2003 u Wayback Machine pidruchnik sho vklyuchaye vstup do logiki Goara 2002 rik ISBN 0 521 00401 2 A K Guc Matematichna logika i teoriya algoritmiv Vidavnictvo Spadok Omsk 2003 r Posilannyaopisav podibni pravila dlya pidmnozhini movi Java dlya vikoristannya z sistemoyu dovedennya teorem j Algo modul Hoare calculus 5 travnya 2011 u Wayback Machine Vizualizaciya chislennya Goara v programi vizualizaciyi algoritmiv j Algo napivavtomatichna sistema verifikaciyi sho pobudovana na bazi sistemi dovedennya teorem Vikoristano materiali zi statti v formalna sistema z anglijskoyi Vikipediyi