Не понял. f1() = f2() уже не написать?
...
Это масло маляное. Непроиниченные переменные потому и непроиниченные, что про них забыли. Ассерт забудут с тем же успехом.
Если f1() из этого же модуля, то при вызове сравнивается ее входной АССЕРТ и соответствие состояние переменных до ее вызова (то же самое для f2)
Внутри f1 (и других) проверяется, что условие ассерта выхода выводится из входного ассерта (если не возможно, то об этом сообщается).
Если же f1 из другого модуля, то считается, что данное условие корректно (тут надо подумать).
Для непроиниченных наверное конкретно ассерты не надо ставить, просто проверять, что они присваиваются каким либо способом до места сравнения.
Получается, что обязательными надо сделать для процедур и циклов входные и выходные ассерты, и уже на них строить проверки.
Думаю без каких-то еще допущений нельзя будет обойтись, но пока считаю, что реализовать проверку можно (хоть и сложно).
