Методы и средства инженерии программного обеспечения
Общая характеристика формальных методов доказательства
Над этим направлением работали многие теоретики–программисты, некоторые из них, которые являются базовыми методами доказательства программ, кратко излагаются ниже.
Метод Флойда основан на определении условий для входных и выходных данных и в выборе контрольных точек в доказываемой программе так, чтобы путь прохождения по программе проходил хотя бы через одну контрольную точку. Для этих точек формулируются утверждения о состоянии переменных в этих точках (для циклов эти утверждения должны быть истинными при каждом прохождении цикла – инварианты цикла).
Каждая точка рассматривается, как индуктивное утверждение, т.е формула, которая остается истинной при возвращении в эту точку программы и зависит не только от входных и выходных данных, но от значений промежуточных переменных. На основе индуктивных утверждений и условий на аргументы программы строятся условия проверки правильности этой программы. Для каждого пути программы между двумя точками устанавливается соответствие условий правильности и определяется истинность этих условий при успешном завершении программы на данных, которые удовлетворяют входным условиям.
Формирование таких утверждений оказалось очень сложной задачей, особенно для программ с высокой степенью параллельности и взаимодействия с пользователем. Как оказалось на практике, достаточность таких утверждений трудно проверить.
Доказательство корректности применялось для уже написанных программ и тех, что разрабатываются путем последовательной декомпозиции задачи на подзадачи, для каждого из них формулировалось утверждение с учетом условий ввода и вывода и соответствующих входных и выходных утверждений. Доказать истинность этих условий – основа метода доказательства полноты, однозначности и непротиворечивости спецификаций.
Метод Хоара – это усовершенствованный метод Флойда, основанный на аксиоматическом описании семантики ЯП исходных программ. Каждая аксиома описывает изменение значений переменных с помощью операторов этого языка.
