|
Abstract : |
In software verication it is often required to prove statements about heterogeneous domains containing elements of various sorts, such as counters, stacks, lists, trees and queues. Any domain with counters, stacks, lists, and trees (but not queues) can be easily seen a special case of the term algebra, and hence a decision procedure for term algebras can be applied to decide the rst-order theory of such a domain. We prove that the rst-order theory of term algebras extended with queues is decidable by presenting a quantier-elimination procedure for this theory. Term algebras with queues Sorts. We assume a nite set of basic sort. We dene sort as follows: (i) every basic sort is a sort; (ii) if is a sort, then queue() is a sort, called a queue sort. We call a function type any expression of the form 1 : : : n! , where 1; : : : ; n; are sorts, n 0. When n = 0, we will write instead of! . A signature S is a pair consisting of a nite set of function symbols, and a function: mapping every function symbol f to a function type 1 : : : n! , called the type of f, where is a basic sort. The number n is called the, |
