Portal de Periódicos da CAPES

Algorithmic theories of data structures

1982; Springer Science+Business Media; Linguagem: Inglês

10.1007/bfb0012792

1611-3349

Andrzej Salwicki,

Formal Methods in Verification

We are arguing that main problems of data structures i.e. can be approached and solved by developping and studying theories of data structures which are based on algorithmic logic AL. we propose to specify a data structure by a proper set of algorithmic axioms. Then verification of a corresponding property of a program consists in proving the formula which expresses the property. The proof making use of axioms of the data structure. We present a case study of the algorithmic theory of priority queues ATPQ. we show that the axiomatization of ATPQ is proper by proving the representation theorem, Namely, every model of the theory is isomorphic with the two-sorted model of a linearly ordered set of elements and the family of all finite subsets of the given set of elements, Next, we prove the correctness of an implementation of priority queues in binary search trees. We relate theoretical results to corresponding modules of software written in LOGLAN programming language. Remarks on dynamization of abstract theories of data structures by adding notion of reference, also axiomatizable in AL, are given. Finally, we compare our approach with others known in the literature.