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评估了该方法，并证明了一组数据结构操作程序的正确性。