Рекурсивні та індуктивні методи грають важливу роль в специфікації та верифікації програмних систем. Формалізація таких методів базується на різноманітних операторах нерухомої точки в різних алгебрах. В статті визначаються предикатні алгебри, розглядаються властивості та структури множин нерухомих точок монотонних та неперервних операторів для різних типів частково впорядкованих множин предикатів. Представлені нові нотації операторів Т-нерухомих точок та досліджені їх властивості.
Recursive and inductive methods play an important rote in software systems specification and verification. Formalization of such methods is based on different fixed point operators in various algebras. In the paper we define predicate algebras and study properties and structures of fixed point sets of monotone and continuous operators for different types of partially ordered sets of predicates. New notions of T-fixed point operators are introduced and their properties are investigated.
