logo
otvety_all

Методы доказательства правильности программ.

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