StorageStackSemantics

存储堆栈语义 这是一个存储库，用于展示我们在 HotOS 2015 上发表的最近工作中讨论的证明风格。我们的论文可以在这里找到： : . 这个回购中有什么？ 有一个 Isabelle thoery 文件，它展示了如何对简单的 KV 存储及其操作进行建模，并证明诸如原子放置等属性。 什么是伊莎贝尔？ Isabelle 是一个定理证明环境。 此 repo 中的理论文件最好在 Isabelle 安装程序 tar 附带的 jEdit 中打开和编辑。 您可以从下载 Isabelle。 为什么我实际上看不到像 ==> 这样的符号，但是像 RightArrow 这样的按键？ 如上一个问题所述，该文件是在 jEdit 中编辑的，最好在相同的环境中查看。 我怎样才能运行这个证明片段？ 如果您已成功安装 Isabelle，则只需从安装目录运行 Isabelle201X - 这将打开 jEdit。