Аннотация: Рассматривается проблема построения монотонной логики Флойда-Хоара, которая является расширением классической логики Флойда-Хоара для случая частичных предикатов. Обобщается построенная монотонная логика на случай многосортных логик. Для этого вводятся номинативные данные с типами. Доказывается монотонность композиций представленной логики, а также непрерывность композиции Флойда-Хоара.

Ключевые слова: программные логики, композиционно-номинативный подход, монотонные композиции, типизированные данные.

ACM Classification Keywords: F.3.1 Specifying and Verifying and Reasoning about Programs – Logics of Programs

Link:

МНОГОСОРТНАЯ МОНОТОННАЯ ЛОГИКА ФЛОЙДА-ХОАРА

Андрей Криволап, Николай Никитченко

http://www.foibg.com/ijita/vol20/ijita20-04-p04.pdf