Scalable Computing Through Reusability: Encapsulation, Specification, and Verification for a Navigable Tree Position.

Design, development, and reuse of generic data abstractions are at the core of scalable computing. This paper presents a novel data abstraction that captures a navigable tree position. The mathematical modeling of the abstraction encapsulates the current tree position, which can be used to navigate and modify the tree. The encapsulation of the tree position in the data abstraction specification avoids explicit references and aliasing, thereby simplifying verification of (imperative) client code that uses the data abstraction. The generic data abstraction is reusable, and its design makes verification scalable. A general tree theory, rich with mathematical notations and results, has been developed to ease the specification and verification tasks. The paper contains an example to illustrate automated verification ramifications and issues in scalability. With sufficient tree theory development, automated proving seems plausible even in the absence of a special-purpose tree solver.