Вікіпедія

Логіка Гоара: відмінності між версіями

Інтерактивний перегляд історії
[неперевірена версія][неперевірена версія]
← Попереднє редагуванняНаступне редагування →
Вилучено вміст Додано вміст
ВізуальнийВікірозмітка
Hjvfy (обговорення | внесок)
19 792 редагування
Рядок 1:
'''Логіка ХоараГоара''' (також відома як '''Флойда-Гоара''') - це [[формальна система]] з множиною логічних правил для строгого доведення [[коректність програми|коректності програм]]. Запропонована в 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> для [[Блок-схема|блок-схем]].
 
== Трійки ГоараХоара ==
Основним інструментом логіки Гоара є '''трійки Гоара'''. Трійки описують як виконання частини коду змінює стан програми. Їх записують в такій формі
 
Рядок 16:
 
== Правила ==
Основою для логіки виведення правильних програм служать аксіоми [[Тоні Гоар|Гоара]]. Вони допускають інтерпретації в термінах програмних конструкцій.
Сформулюємо аксіоми [[Тоні Гоар|Гоара]], які визначають передумови як достатні умови, які гарантують, що виконання відповідних операторів при вдалому завершенні приведе до бажаних після умов.
=== Аксіома про порожній оператор ===
Аксіома про порожній оператор каже нам що він не змінює стан програми, тому що було правдою до його виконання, залишається таким же і після.
Рядок 131 ⟶ 133:
== Література ==
* Robert D. Tennent. ''[http://www.cs.queensu.ca/home/specsoft/ Specifying Software]'' (підручник що включає вступ до логіки Гоара, 2002 рік) ISBN 0-521-00401-2
* А.К. Гуц, Математична логіка і теория алгоритмов, 2003р.
 
== Посилання ==
* {{en|http://en.wikipedia.org/wiki/Hoare_logic}}
* [http://isabelle.in.tum.de/Bali/ Project Bali] описав подібні правила для підмножини мови Java для використання з системою доведення теорем [[Isabelle]]
* [http://www.key-project.org/download/hoare/ KeY-Hoare] напівавтоматична система верифікації що побудована на базі системи доведення теорем [[KeY]].▼
* [http://j-algo.binaervarianz.de/index.php?language=en j-Algo-modul Hoare calculus] — Візуалізація числення Гоара в програмі візуалізації алгоритмів j-Algo
▲* [http://www.key-project.org/download/hoare/ KeY-Hoare] напівавтоматична система верифікації що побудована на базі системи доведення теорем [[KeY]].{{en|http://en.wikipedia.org/wiki/Hoare_logic}}
*<font size="2">Використано матеріали зі статті в [а''') - це [[формальна система]] з множи англійській Вікіпедії].</font>
 
[[Категорія:Математична логіка]]
Отримано з https://uk.wikipedia.org/wiki/Логіка_Гоара