В работе проведен разносторонний анализ сложностей и ограничений, препятствующих широкому внедрению формальных методов в практику проектирования программного обеспечения. Показано, что наряду с общеметодологическими проблемами и человеческими факторами, ряд сложностей заключен в математическом аппарате этих методов. Предложен новый математический аппарат, аппарат ограниченных функций и lf-функций, для описания функциональной семантики программ, их формализованного анализа и верификации. Предлагаемый аппарат по своей структуре ориентирован на упрощение разработки и теоретического обоснования языковых средств анализа и верификации программ и их классов. Препринт рассчитан на широкий круг читателей - специалистов по формальным методам создания программного обеспечения: верификации, спецификации, формализованному анализу программ.