Верификация сортировки вставками и слиянием. Рекурсивные функции с неструктурной рекурсией. Плагин Program. Acc-предикат и рекурсивные функции.
Введение в формальную верификацию программ