We propose a novel mechanism of defining data structures using intrinsic definitions that avoids recursion and instead utilizes monadic maps satisfying local conditions. We show that intrinsic definitions are a powerful mechanism that can capture a variety of data structures naturally. We show that they also enable a predictable verification methodology that allows engineers to write ghost code to update monadic maps and perform verification using reduction to decidable logics. We evaluate our methodology using Boogie and prove a suite of data structure manipulating programs correct.

翻译：我们提出了一种利用内在定义定义数据结构的新机制，该机制避免递归，转而使用满足局部条件的单子映射。研究表明，内在定义是一种强大的机制，能够自然地描述多种数据结构。同时，该机制支持一种可预测的验证方法，允许工程师编写幽灵代码来更新单子映射，并通过归约到可判定逻辑进行验证。我们使用Boogie评估了这一方法，并证明了一系列数据结构操作程序的正确性。