программа верификации, верификатор
условий
программа, анализирующая
текст программы, снабженный условиями и операторами контроля (assertion),
которые должны выполняться в
определенных ее точках,
и доказывающая их истинность или ложность при
заданных предусловиях (precondition)