Журнал ИМТ
АннотацияФрагмент документа
260_1
http://libmeta.ru/resource/imt/seg/260_1
Текст фрагмента
Представлен метод предикатного программирования в применении к известной программе и нвертирования односвязных списков. Данная программа признана крайне трудн ой для дедуктивной верификации ( verification challenge ). Описыва ются построение и дедуктивная верификация предикатной программы инвертирования списка как объекта алгебраического типа. Эффективная императивная программа получена применением оптимизирующих трансформаций. Дедуктивная верификация предикатной программы на порядок проще верификации аналогичной императивной программы, использующей указатели.
Данные
| hasConfidence | 1.0 |
| hasOrderIndex | 1 |
| wasManuallyVerified | false |
extractedFrom
generatedBy
Входящие связи
← содержит фрагмент · 1