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

G 

(y = 5)), т.е. «после того, как x станет положительным, y не может 
все время оставаться не равным 5». Конструкция 

G (

P) имеет смысл «когда-
нибудь в будущем P выполнится» и для нее есть отдельная запись F P. 

Дальнейшим обобщением логики линейного времени (linear temporal logic, LTL), 
примеры формул которой приведены в предыдущем пункте, является логика 
дерева вычислений (Computation Tree Logic, CTL*) [111,113,114], в которой 
можно делать утверждения не только об отдельных событиях и их порядке во 
времени, но и о различных возможностях развития событий. 

Еще более общим исчислением, чем временные логики, является 

-исчисление 
(или исчисление неподвижных точек) [111,113,114]. 

Временные логики используют время неявно, только для рассмотрения 
возможных последовательностей событий. Если необходимо явно учитывать 
величину интервалов времени между событиями, используются логики явного 

---

50 
времени (timed temporal logics), в утверждениях которых участвуют переменные, 
обозначающие некоторые моменты времени, и явно указанные величины 
временных интервалов. 
В качестве примеров алгебраических моделей приведем следующие. 

Реляционные алгебры [115,116], лежащие в основе реляционных систем 
управления базами данных. 

Алгебраические модели абстрактных типов данных. Например, можно 
определить абстрактный тип данных Stack стека объектов типа T как алгебру с 
набором 
операций 
pop: Stack 

Stack

T 
и 
push: Stack

T 

Stack, 
удовлетворяющую соотношению pop(push(s, t)) = (s, t). В принципе, все свойства 
стека можно вывести из этого соотношения. Аналогичное описание для очереди 
объектов типа T, несмотря на небольшое содержательное отличие от стека, 
выглядит значительно сложнее. 

Алгебры процессов (исчисления процессов, process calculi) [117-123]. Это 
алгебраические исчисления, объектами которых являются события и процессы, 
создающие события или реагирующие на них. Обычно для процессов 
определены операции последовательной (‘;’) и параллельной (‘||’) композиции и 
операция выбора из двух альтернатив (альтернативная композиция, ‘+’). 
Процесс является моделью выполняющейся программы. Последовательная 
композиция процессов моделирует выполнение сначала первого из них, затем 
второго. Параллельная композиция моделирует параллельное выполнение обоих 
процессов. Выбор из двух процессов моделирует выполнение либо первого, 
либо второго. В большинстве таких исчислений процессы могут 
взаимодействовать, обмениваясь событиями (один процесс порождает событие, 
другой или другие его потребляют). 
Наиболее широко известны исчисления процессов CSP (Communicating 
Sequential Processes) [118], CCS (Calculus of Communicating Systems) [119], ACP 
(Algebra of Communicating Processes) [120,121]. Для моделирования мобильных 
вычислений, т.е. вычислений в среде с изменяющимися связями между узлами и 
с переносом самих вычислительных процессов с одного узла на другой, 
используют 

-исчисление [122] и исчисление окружений (ambient calculus) [123]. 

---

51