Верификация предикатной программы бинарного поиска объекта произвольного типа
Язык статьиРусский
Аннотация
Описывается построение и дедуктивная верификация предикатной программы бинарного поиска, идентичной программе bsearch на языке Си из библиотеки ОС Linux. В языке предикатного программирования определяются новые конструкции для произвольных типов в качестве параметров программ. Для объектов произвольного типа вводятся трансформации кодирования через указатели.
Ключевые слова
DOI10.31144/si.2307-6410.2019.n15.p45-64
УДК004.05
Номер
№ 15,
Страницы45-64
Файл
bsearchsi.pdf
(888.42 КБ)
Библиографическая ссылка
Шелехов В.И. Верификация предикатной программы бинарного поиска объекта произвольного типа // Системная информатика, 2019. – № 15. – С. 45-64. – DOI: https://doi.org/10.31144/si.2307-6410.2019.n15.p45-64.