Synthesizing robust data structures-an introduction

A formal approach is presented for the analysis and synthesis of robust data structures. The entire data structure is viewed as a collection of data elements related via some attributes. The relationships are specified by a set of axioms in first-order logic. Faults in attributes invalidate some of the axioms. The invalidated axioms are used to detect and correct the faulty attributes. The authors show how detection and correction can be localized to small portions of the data structure, thereby allowing concurrent repair in several disjoint portions. This property makes local correction attractive for B-trees and other structures used in databases. They then show how the ideas developed for attaining structural integrity can be applied to achieve data integrity as well