类Java语言的帧栈语义的形式化
Formalisation of a frame stack semantics for a Java-like language
摘要：
我们提出了一个Coq形式化的小步操作语义的Jafun，一个小的类Java语言。这种语义格式使得自然地指定和证明应该在每个计算步骤中保持的不变量成为可能。与Featherweight Java方法相反，语义显式地操纵方法调用的帧堆栈。由于这一点，人们可以表示依赖于特定方法执行的计算属性。在语义的基础上，我们开发了一个类型系统，它可以描述一个复合值的概念，并将某些方法分类为对它们进行操作的扩展函数。在我们的形式化，我们作出了一个机械化的证明，操作语义的无类型版本的语义同意的类型之一。我们讨论了不同的方法，使这种形式化的努力，并提供实验，证实它。
英文摘要：
We present a Coq formalisation of the small-step operational semantics of Jafun, a small Java-like language with classes. This format of semantics makes it possible to naturally specify and prove invariants that should hold at each computation step. In contrast to the Featherweight Java approach the semantics explicitly manipulates frame stack of method calls. Thanks to that one can express properties of computation that depend on execution of particular methods. On the basis of the semantics, we developed a type system that makes it possible to delineate a notion of a compound value and classify certain methods as extensional functions operating on them. In our formalisation we make a mechanised proof that the operational semantics for the untyped version of the semantics agrees with the one for the typed one. We discuss different methods to make such formalisation effort and provide experiments that substantiate it.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
