Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Правила проверки корректности компьютерных программ
Rules to verify computer program correctness
Логика Хоара (также известная как логика Флойда — Хоара или правила Хоара) — это формальная система с набором логических правил для строгого обоснования корректности компьютерных программ. Она была предложена в 1969 году британским ученым-компьютерщиком и логиком Тони Хоаром и впоследствии доработана Хоаром и другими исследователями. Исходные идеи были заложены в работе Роберта В. Флойда, который опубликовал аналогичную систему для блок-схем.
Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician Tony Hoare, and subsequently refined by Hoare and other researchers. The original ideas were seeded by the work of Robert W. Floyd, who had published a similar system for flowcharts.
Трижды
Центральным элементом логики Хоара является тройка Хоара. Тройка описывает, как выполнение фрагмента кода изменяет состояние вычисления. Тройка Хоара имеет вид {P} C {Q}, где P и Q – утверждения, а C – команда. P называется предусловием, а Q – постусловием: если предусловие истинно, то выполнение команды гарантирует истинность постусловия. Утверждения – это формулы в логике предикатов. Логика Хоара предоставляет аксиомы и правила вывода для всех конструкций простого императивного языка программирования. Помимо правил для простого языка, представленных в оригинальной работе Хоара, с тех пор Хоаром и многими другими исследователями были разработаны правила для других языковых конструкций. Существуют правила для работы с конкурентностью, процедурами, переходами и указателями.
The central feature of Hoare logic is the Hoare triple. A triple describes how the execution of a piece of code changes the state of the computation. A Hoare triple is of the form
where and are assertions and is a command. is named the precondition and the postcondition: when the precondition is met, executing the command establishes the postcondition. Assertions are formulae in predicate logic. Hoare logic provides axioms and inference rules for all the constructs of a simple imperative programming language. In addition to the rules for the simple language in Hoare's original paper, rules for other language constructs have been developed since then by Hoare and many other researchers. There are rules for concurrency, procedures, jumps, and pointers.
Частичная и полная правильность
Используя стандартную логику Хоаре, можно доказать только частичную корректность. Полная корректность дополнительно требует доказательства завершения, которое можно доказать отдельно или с использованием расширенной версии правила While. Таким образом, интуитивное понимание тройки Хоаре заключается в следующем: если выполняется условие в состоянии перед выполнением , то будет выполняться после его выполнения, или не завершится. В последнем случае "после" не существует, поэтому может быть любым утверждением. Действительно, можно выбрать ложным, чтобы выразить, что не завершается. Под "завершением" здесь и во всей статье подразумевается в широком смысле конечное завершение вычислений, то есть отсутствие бесконечных циклов; это не подразумевает отсутствие нарушений предельных ограничений реализации (например, деления на ноль), приводящих к преждевременной остановке программы. В своей статье 1969 года Хоар использовал более узкое понятие завершения, которое также включало отсутствие нарушений ограничений реализации, и выразил предпочтение более широкому понятию завершения, поскольку оно обеспечивает независимость утверждений от реализации.
Using standard Hoare logic, only partial correctness can be proven. Total correctness additionally requires termination, which can be proven separately or with an extended version of the While rule. Thus the intuitive reading of a Hoare triple is: Whenever holds of the state before the execution of , then will hold afterwards, or does not terminate. In the latter case, there is no "after", so can be any statement at all. Indeed, one can choose to be false to express that does not terminate. "Termination" here and in the rest of this article is meant in the broader sense that computation will eventually be finished, that is it implies the absence of infinite loops; it does not imply the absence of implementation limit violations (e. g. division by zero) stopping the program prematurely. In his 1969 paper, Hoare used a narrower notion of termination which also entailed the absence of implementation limit violations, and expressed his preference for the broader notion of termination as it keeps assertions implementation independent:
Схема аксиомы пустого утверждения
Правило пустого оператора утверждает, что оператор не изменяет состояние программы, следовательно, все, что было истинно до его выполнения, останется истинным и после него.
The empty statement rule asserts that the statement does not change the state of the program, thus whatever holds true before also holds true afterwards.