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