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