Deriving Pretty-Big-Step Semantics from Small-Step Semantics
Deriving Pretty-Big-Step Semantics from Small-Step Semantics
复制标题
从小步语义导出相当大步语义
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Peter D. Mosses
中科院分区：
文献类型：
--
作者：
Casper Bach Poulsen;Peter D. Mosses
语言的大步骤语义突然终止和/或分歧遭受严重的重复问题，解决了由Chargueraud在ESOP'13提出的新颖的'漂亮的大步骤'风格。这种规则不如相应的小步规则简洁，但在程序正确性证明方面，它们具有与大步规则相同的优点。在这里，我们展示了如何通过“重新聚焦”直接从小步规则自动导出相当大的步长规则。这是两全其美：我们只需要编写相对简洁的小步规范，但我们的推理可以是大步也可以是小步。使用严格性注释来推导小步全等规则进一步简洁。
Big-step semantics for languages with abrupt termination and/or divergence suffer from a serious duplication problem, addressed by the novel 'pretty-big-step' style presented by Chargueraud at ESOP'13. Such rules are less concise than corresponding small-step rules, but they have the same advantages as big-step rules for program correctness proofs. Here, we show how to automatically derive pretty-big-step rules directly from small-step rules by 'refocusing'. This gives the best of both worlds: we only need to write the relatively concise small-step specifications, but our reasoning can be big-step as well as small-step. The use of strictness annotations to derive small-step congruence rules gives further conciseness.