На основе формальной логики, лежащей в основе методов формального описания языков программирования, производится вывод "аксиом"для условного оператора и оператора вызова процедуры. Применение выведенных "аксиом" иллюструется на примере процедуры с весьма глубокой рекурсией.
