аксиомы и правила вывода. Такие инструментальные средства также позволяют применять систематический перебор с целью поиска различных направлений продолжения доказательства из текущего состония.
Верификация моделей программ.
В основе метода верификации лежит предположение о том, что существует программная документация, соответствие которой требуется доказать. Документация должна содержать:
спецификацию ввода-вывода (описание данных, не зависящих от процесса обработки);свойства отношений между элементами векторов состояний в выбранных точках программы;
спецификацию структур данных, зависящих от процесса обработки.
К такому методу доказательства правильности программ относится метод индуктивных утверждений, независимо сформулированный К. Флойдом и П. Науром.
Принципы model checking: