说明具有当地能力的机器的理由:可安全可靠堆叠和返回点管理----技术附录,包括证明和细节 (Reasoning About a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management - Technical Appendix Including Proofs and Details)

2019 年 2 月 14 日

Reasoning About a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management - Technical Appendix Including Proofs and Details

翻译：说明具有当地能力的机器的理由:可安全可靠堆叠和返回点管理----技术附录,包括证明和细节

Lau Skorstengaard,Dominique Devriese,Lars Birkedal

We propose a calling convention for capability machines with local capabilities. The calling convention ensures local-state encapsulation and well-bracketed control flow. We use the calling convention in a hand-full of program examples and prove that they behave correctly. The correctness proofs use a logical relation that is also presented in this appendix. This is the technical appendix for the paper with the same name and authors accepted at ESOP18 and under review for TOPLAS.

翻译：我们提出了具有当地能力的能力机器呼叫公约。呼叫公约确保了当地状态的封装和良好的控制流动。我们使用呼吁公约的手动程序实例,并证明它们的行为正确。正确性证明使用了本附录中也列出的逻辑关系。这是ESOP18所接受的、正在接受《反恐法案》审查的、名称和作者相同的文件的技术附录。