Методы верификации программного обеспечения

3.3. 
Формальные методы верификации 
Формальные методы верификации ПО используют формальные модели 
требований, поведения и окружения ПО для анализа его свойств. Такие модели 
являются либо логико-алгебраическими, либо исполнимыми, либо промежуточными, 
имеющими черты и логико-алгебраических, и исполнимых моделей. Прежде чем 
перейти к обсуждению методов анализа таких моделей, рассмотрим различные типы 
формальных моделей более подробно. 
3.3.1. Логико-алгебраические модели 
Логико-алгебраические модели (property-based models), они же — логические или 
алгебраические исчисления. При моделировании ПО модель такого типа описывает 
некоторый набор его свойств, быть может, изменяющийся со временем, но не дает 
точного представления о том, за счет чего изменяются эти свойства. 
Отличие между логическими и алгебраическими исчислениями довольно 
условно, но, несколько упрощая, можно считать, что логика имеет дело с 
утверждениями в рамках какого-то языка, а алгебра — с равенствами и неравенствами 
построенных в некотором языке выражений. В первом случае основным объектом 
внимания являются утверждения, ложные или истинные, а во втором — выражения или 
термы, относящиеся к какому-то типу. 
Примеры логических исчислений таковы. 

Исчисление высказываний (пропозициональное исчисление, propositional 
calculus) [108,109]. В нем есть атомарные высказывания, возможно, зависящие 
от объектных переменных, а также логические связки & («и», конъюнкция), 

(«или», дизъюнкция), 

(«не», отрицание), 

(«следовательно», импликация), 

(эквивалентность), с помощью которых можно из одних высказываний 
строить другие, более сложные. 

Исчисление предикатов (predicate calculus) [108,109] добавляет в исчисление 
высказываний возможность использовать кванторы по объектным переменным 
для построения новых утверждений. Кванторы в этом исчислении бывают двух 

---

48 
видов — 

«для любого» и 

«существует». 
В исчислении предикатов помимо объектных переменных есть функциональные 
и предикатные. Первые представляют собой разнообразные функции, результат 
применения функции к объекту является объектом. Вторые представляют 
неопределенные утверждения, результат их применения к объекту должен 
всегда быть истиной или ложью. В нетипизированном исчислении все объекты 
равноправны, функции и предикаты могут принимать любые объекты в качестве 
аргументов. В типизированных исчислениях каждый объект имеет тип, а 
функциональные и предикатные переменные — сигнатуру, т.е. список типов 
параметров и тип результата для функций. Соответственно, строить формулы 
можно только соблюдая соответствие типов параметров типам выражений, 
подставляемых на место этих параметров. 

Исчисления предикатов более высоких порядков (higher-order calculi). В этих 
исчислениях можно использовать кванторы не только по объектным 
переменным, но и по функциональным или предикатным. 
Например, определение равенства объектов иногда формулируется так: x = y 


P P(x) 

P(y), два объекта равны, если любое утверждение одновременно 
выполнено или не выполнено для них обоих. 


-исчисление (lambda calculus) [110] — с помощью ламбда-оператора позволяет 
строить функции из выражений, например, выражение 

x x*x обозначает 
функцию возведения в квадрат. В этом примере x также является связанной, не 
имеющей собственного содержания переменной. 
В 

-исчислении с типами, так же как и в типизированном исчислении 
предикатов, объекты имеют типы, а функции — сигнатуры.

-исчисления более высоких порядков [111] позволяют применять 

-оператор не 
только к объектам, но и к типам. При этом получаются функции, 
преобразующие типы в типы. Примером такого преобразования является 
построение по типу T типа списка объектов типа T. 
Часто расширения исчисления предикатов и 

-исчисления первого порядка 

---

49 
совместно называют логиками первого порядка, а расширения исчисления 
предикатов и 

-исчисления высших порядков — логиками высших порядков. 

Модальные логики [112] помимо связок допускают построение утверждений с 
помощью операторов с дополнительной смысловой нагрузкой, давая 
возможность строго анализировать связи между, например, утверждениями «x = 
3», «доказано, что x = 3», «может быть, что x = 3», «всегда будет x = 3» или 
«хотелось бы, чтобы было x = 3». 

Специальным случаем модальных логик являются временные логики (temporal 
logics) [111,113,114], в которых дополнительные операторы используются для 
описания временной последовательности событий — «как только x станет равно 
3, у должно стать равно 0», «после того, как x станет больше 0, спустя некоторое 
время y обязательно станет равно 5». 
В логиках с дискретным временем считается, что моменты времени отделены 
друг от друга и у каждого момента есть следующий. Утверждение X P означает, 
что утверждение P будет выполнено в следующий момент времени, а G P — что 
P будет выполнено во все будущие моменты времени. Первый пример из 
предыдущего абзаца можно записать как G (x = 3 

y = 0), а второй — как G (x 
> 0 

