Functional Modeling, Verification and Access Optimization of Adaptive Priority Search Tree

The priority search tree (PST) is a data structure that combines the characteristics of search trees and priority queues, enabling efficient retrieval of high-priority elements while maintaining worst-case search efficiency comparable to that of search trees. Nipkow et al. further modeled and mechanized the verification of PST with a static priority mechanism, laying an important foundation for its formal analysis and subsequent theoretical exploration. However, static priority mechanisms can lead to degraded performance under highly skewed access distributions, limiting their applicability in practice. To overcome this limitation, a functional adaptive priority search tree (FAPST) is proposed. FAPST adopts dynamic priority adjustment based on access frequency and is formally modeled and verified at the formal level to ensure functional correctness and reliability. This structure preserves balance and worst-case efficiency while adaptively responding to access patterns, thereby significantly improving the retrieval of frequently accessed elements. To further address the shifting nature of data hotspots in practical scenarios, a hotspot migration mechanism is introduced. This mechanism incorporates a priority decay strategy to accelerate responses to emerging hotspots and mitigate the stagnation of outdated ones. Experimental results demonstrate that, in both access-sensitive and hotspot-shifting workloads, the formally verified FAPST achieves notable reductions in the number of key function calls of 64.8% and 46.3% respectively, compared to conventional PSTs.