Алгоритмическая логика

Алгоритмическая логика — исчисление программ, позволяющее выразить семантические свойства программ соответствующими логическими формулами . Он обеспечивает основу , которая позволяет доказывать формулы на основе аксиом программных конструкций, таких как инструкции присваивания, итерации и композиции, а также на основе аксиом структур данных рассматриваемых , см. Mirkowska & Salwicki (1987) , Banachowski et al. (1977) .

Следующая диаграмма помогает найти алгоритмическую логику среди других логик . $\qquad \left[{\begin{array}{l}\mathrm {Propositional\ logic} \\or\\\mathrm {Sentential\ calculus} \end{array}}\right]\subset \left[{\begin{array}{l}\mathrm {Predicate\ calculus} \\or\\\mathrm {First\ order\ logic} \end{array}}\right]\subset \left[{\begin{array}{l}\mathrm {Calculus\ of\ programs} \\or\\{\mbox{Algorithmic logic}}\end{array}}\right]$
Формализованный язык алгоритмической логики (и алгоритмических теорий различных структур данных) содержит три типа правильно сформированных выражений: термины - т.е. выражения, обозначающие операции над элементами структур данных; формулы - т.е. выражения, обозначающие отношения между элементами структур данных, программы - т.е. алгоритмы - эти выражения описывают вычисления.Семантику терминов и формул можно узнать на страницах, посвященных логике первого порядка и семантике Тарского. Смысл программы $K$ — множество возможных вычислений программы.

Алгоритмическая логика — одна из многих логик программ.Другая логика программ — динамическая логика, см. динамическую логику , Harel, Kozen & Tiuryn ​​(2000) .

Библиография

1. Мирковская, Гражина; Салвицкий, Анджей (1987). Алгоритмическая логика (PDF) . Варшава и Бостон: PWN & D. Reidel Publ. стр. 372. ISBN  8301068590 . ]
2. [Баначовский и др.] | Банаховский, Лех; Кречмар, Антони; Мирковская, Гражина; Расёва, Хелена; Салвицкий, Анджей (1977). Введение в алгоритмическую логику - Метаматематические исследования теории программ . Публикации Банахового центра. Том 2. Варшава: PWN. стр. 7–99.
3. Харель, Дэвид ; Козен, Декстер ; Тюрин, Ежи (2000). Динамическая логика . Кембридж, Массачусетс: MIT Press. стр. 459 .