WikiDer > Логика Хоара

Hoare logic

Логика Хоара (также известен как Логика Флойда – Хора или Правила Хора) это формальная система с набором логических правил для строгого рассуждения о правильность компьютерных программ. Он был предложен в 1969 году британским ученым-компьютерщиком и логик Тони Хоар, а затем уточнены Хоаром и другими исследователями.[1] Оригинальные идеи были заложены в результате работы Роберт В. Флойд, опубликовавший аналогичную систему[2] за блок-схемы.

Хоар тройной

Центральная особенность Логика Хоара это Хоар тройной. Тройка описывает, как выполнение фрагмента кода меняет состояние вычисления. Тройка Хоара имеет вид

где и находятся утверждения и это команда.[примечание 1] назван предварительное условие и то постусловие: когда предварительное условие выполнено, выполнение команды устанавливает постусловие. Утверждения - это формулы в логика предикатов.

Логика Хоара обеспечивает аксиомы и правила вывода для всех конструкций простого императивный язык программирования. В дополнение к правилам для простого языка из оригинальной статьи Хора, с тех пор Хоаром и многими другими исследователями были разработаны правила для других языковых конструкций. Есть правила для параллелизм, процедуры, прыгает, и указатели.

Частичная и полная правильность

Используя стандартную логику Хоара, только частичная правильность может быть доказано, а прекращение нужно доказывать отдельно. Таким образом, интуитивное прочтение тройки Хоара: удерживает государство до исполнения , тогда будет держаться потом, или не прекращается. В последнем случае "после" нет, поэтому может быть любое высказывание. Действительно, можно выбрать быть ложным, чтобы выразить это не прекращается.

Полная правильность также можно проверить с помощью расширенной версии правила Пока.[нужна цитата]

В своей статье 1969 года Хоар использовал более узкое понятие завершения, которое также влекло за собой отсутствие каких-либо ошибок времени выполнения:«Отказ завершить может быть из-за бесконечного цикла; или это может быть из-за нарушения ограничения, определенного реализацией, например диапазона числовых операндов, размера хранилища или ограничения времени операционной системы».[3]

Правила

Схема аксиомы пустого оператора

В пустой оператор Правило утверждает, что оператор не изменяет состояние программы, поэтому все, что выполняется до также верно и в дальнейшем.[заметка 2]

Схема аксиомы присваивания

Аксиома присваивания утверждает, что после присваивания любой предикат, который ранее был истинным для правой части присваивания, теперь выполняется для переменной. Формально пусть - утверждение, в котором переменная является свободный. Потом:

где обозначает утверждение в котором каждый свободное вхождение из был заменены выражением .

Схема аксиом присваивания означает, что истинность эквивалентно истине после присвоения . Так были истина до присваивания по аксиоме присваивания, то будет верно после чего. Наоборот, были ложь (т.е. истина) перед оператором присваивания, после этого должно быть ложным.

Примеры допустимых троек:

Все предварительные условия, которые не изменяются выражением, могут быть перенесены в постусловие. В первом примере присвоение не меняет того факта, что , поэтому оба оператора могут появиться в постусловии. Формально этот результат получается применением схемы аксиом с существование ( и ), что дает существование ( и ), которое, в свою очередь, может быть упрощено до заданного предварительного условия .

Схема аксиомы присваивания эквивалентна утверждению, что для нахождения предусловия сначала возьмите постусловие и замените все вхождения левой части присваивания правой частью присваивания. Будьте осторожны, не пытайтесь сделать это в обратном порядке, следуя этому неверный способ мышления: ; это правило приводит к бессмысленным примерам вроде:

Другая неверный правило, которое на первый взгляд кажется заманчивым, ; это приводит к бессмысленным примерам вроде:

Пока заданное постусловие однозначно определяет предусловие обратное неверно. Например:

  • ,
  • ,
  • , и

являются действительными примерами схемы аксиомы присваивания.

Аксиома присваивания, предложенная Хоаром не применяется когда несколько имен могут относиться к одному и тому же сохраненному значению. Например,

неправильно, если и относятся к той же переменной (сглаживание), хотя это правильный пример схемы аксиом присваивания (с обоими и будучи ).

Правило композиции

Правило композиции Хоара применяется к последовательно выполняемым программам. и , где выполняется до и написано ( называется промежуточное состояние):[4]

Например, рассмотрим следующие два случая аксиомы присваивания:

и

По правилу последовательности можно сделать вывод:

Другой пример показан в правом поле.

Условное правило

Условное правило гласит, что постусловие общий для и часть также является постусловием целого заявление. и часть, незадействованное и отрицательное условие можно добавить к предварительному условию соответственно. , не должно иметь побочных эффектов. пример приведен в следующий раздел.

Этого правила не было в оригинальной публикации Хора.[1]Однако, поскольку заявление

имеет тот же эффект, что и конструкция одноразового цикла

условное правило может быть получено из других правил Хоара. Аналогичным образом правила для других производных программных конструкций, таких как петля, петля, , , может быть уменьшено преобразование программы к правилам из оригинальной статьи Хора.

Правило следствия

Это правило позволяет усилить предусловие и / или ослабить постусловие .Это используется, например, достичь буквально идентичных постусловий для и часть.

Например, доказательство

необходимо применить условное правило, которое, в свою очередь, требует доказательства

, или упрощенный

для часть, и

, или упрощенный

для часть.

Однако правило назначения для часть требует выбора так как ; применение правила, следовательно, дает

, что логически эквивалентно
.

Правило следствия необходимо для усиления предусловия полученный из правила присвоения требуется для условного правила.

Аналогично для часть, правило присваивания дает

, или эквивалентно
,

следовательно, правило следствия должно применяться с и будучи и соответственно, чтобы снова усилить предусловие. Неформально, эффект правила последствий состоит в том, чтобы «забыть», что известно на входе часть, поскольку правило присваивания, используемое для часть не нуждается в этой информации.

Пока правило

Здесь это инвариант цикла, который должен быть сохранен телом цикла .После завершения цикла этот инвариант все еще держится, и более того должен был привести к завершению цикла. Как и в условном правиле, не должно иметь побочных эффектов.

Например, доказательство

к тому времени правило требует доказать

, или упрощенный
,

которое легко получается с помощью правила присваивания. Наконец, постусловие можно упростить до .

В качестве другого примера, правило while можно использовать для формальной проверки следующей странной программы для вычисления точного квадратного корня произвольного числа -даже если является целочисленной переменной и не квадратное число:

После применения правила while с будучи , осталось доказать

,

что следует из правила пропуска и правила следствия.

На самом деле странная программа частично правильно: если это случилось, то наверняка должен был содержать (случайно) ценность квадратный корень. Во всех остальных случаях он не завершается; поэтому это не полностью правильный.

Хотя правило абсолютной правильности

Если выше обычного в то время как правило заменяется следующим, исчисление Хоара также может быть использовано для доказательства полная правильность, т.е. прекращение[заметка 3] а также частичная правильность. Обычно здесь вместо фигурных скобок используются квадратные скобки для обозначения различных представлений о правильности программы.

В этом правиле, помимо сохранения инварианта цикла, также доказывается прекращение посредством выражения , называется вариант петли, значение которой строго убывает по обоснованные отношения на некотором наборе доменов во время каждой итерации. С обоснованно, строго убывающий цепь членов может иметь только конечную длину, поэтому не может уменьшаться вечно. (Например, обычный порядок основан на положительном целые числа , но ни на целые числа ни на положительные действительные числа ; все эти множества подразумеваются в математическом, а не в вычислительном смысле, в частности, все они бесконечны.)

Учитывая инвариант цикла , условие должно означать, что это не минимальный элемент из , иначе тело не мог уменьшиться в дальнейшем, т.е. посылка правила будет ложной. (Это одно из различных обозначений для полной правильности.)[примечание 4]

Возобновляя первый пример предыдущий раздел, для доказательства полной корректности

правило while для полной корректности можно применить, например, неотрицательные целые числа в обычном порядке, а выражение будучи , что, в свою очередь, требует доказательства

Неформально говоря, мы должны доказать, что расстояние убывает в каждом цикле цикла, при этом всегда остается неотрицательным; этот процесс может продолжаться только конечное число циклов.

Предыдущая цель доказательства может быть упрощена до

,

что можно доказать следующим образом:

получается по правилу присваивания, а
можно усилить до по правилу следствия.

Для второго примера предыдущий раздел, конечно без выражения может быть найдено, что уменьшается на пустое тело цикла, следовательно, прерывание не может быть доказано.

Смотрите также

Примечания

  1. ^ Первоначально Хоар написал "" скорее, чем "".
  2. ^ В этой статье используется естественный вычет обозначение стиля для правил. Например, неофициально означает "Если оба и держись, тогда также держит "; и называются антецедентами правила, называется его преемником. Правило без антецедентов называется аксиомой и записывается как .
  3. ^ «Завершение» здесь означает в более широком смысле, что вычисление в конечном итоге будет завершено; оно делает нет подразумевают, что никакое нарушение предела (например, нулевое деление) может преждевременно остановить программу.
  4. ^ В статье Хоара 1969 года не было правила полной правильности; ср. его обсуждение на стр.579 (вверху слева). Например, учебник Рейнольдса (Джон С. Рейнольдс (2009). Теория языков программирования. Издательство Кембриджского университета.), Раздел 3.4, стр.64 дает следующую версию правила полной корректности: когда - целочисленная переменная, которая не встречается бесплатно в , , , или же , и является целочисленным выражением (переменные Рейнольдса переименованы, чтобы соответствовать настройкам этой статьи).

Рекомендации

  1. ^ а б Хоар, К.А.Р. (Октябрь 1969 г.). «Аксиоматическая основа компьютерного программирования» (PDF). Коммуникации ACM. 12 (10): 576–580. Дои:10.1145/363235.363259.
  2. ^ Р. В. Флойд. "Придание смысла программам."Труды симпозиумов Американского математического общества по прикладной математике. Том 19, стр. 19–31. 1967.
  3. ^ стр.579 вверху слева
  4. ^ Хут, Майкл; Райан, Марк (2004-08-26). Логика в информатике (второе изд.). КРУЖКА. п. 276. ISBN 978-0521543101.

дальнейшее чтение

внешняя ссылка

  • Кей-Хоар это полуавтоматическая система проверки, построенная на основе Ключ средство доказательства теорем. Он включает в себя исчисление Хоара для простого языка.
  • j-Алгомодульное исчисление Хоара - Визуализация исчисления Хоара в программе визуализации алгоритма j-Algo