A trustworthy mechanized formalization of R
A trustworthy mechanized formalization of R
复制标题
R 的值得信赖的机械化形式化
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
É. Tanter
中科院分区：
文献类型：
--
作者：
Martin Bodin;Tomás Díaz;É. Tanter
R编程语言在开发统计软件和数据分析方面非常受欢迎，这要归功于丰富的库，简洁而富有表现力的语法以及对交互式编程的支持。然而，R的语义相当复杂，包含许多微妙的角落情况，并且没有正式指定。这使得对R程序进行推理变得困难。在这项工作中，我们开发了一个大步骤的操作语义R的形式的解释器编写的Coq证明助手。我们通过引入一元编码来确保形式化的可信度，该编码允许Coq解释器CoqR与参考R解释器GNU R直接视觉对应。此外，我们提供了一个测试框架，支持CoqR和GNU R的系统比较。在目前的状态下，CoqR涵盖了R语言的核心以及许多附加功能，使其通过了来自GNU R和FastR项目的大量实际测试用例。要行使正式规范，我们证明在Coq的保存内存不变量的解释器的选定部分。这项工作是迈向R程序形式化验证的强大环境的重要的第一步。
The R programming language is very popular for developing statistical software and data analysis, thanks to rich libraries, concise and expressive syntax, and support for interactive programming. Yet, the semantics of R is fairly complex, contains many subtle corner cases, and is not formally specified. This makes it difficult to reason about R programs. In this work, we develop a big-step operational semantics for R in the form of an interpreter written in the Coq proof assistant. We ensure the trustworthiness of the formalization by introducing a monadic encoding that allows the Coq interpreter, CoqR, to be in direct visual correspondence with the reference R interpreter, GNU R. Additionally, we provide a testing framework that supports systematic comparison of CoqR and GNU R. In its current state, CoqR covers the nucleus of the R language as well as numerous additional features, making it pass a significant number of realistic test cases from the GNU R and FastR projects. To exercise the formal specification, we prove in Coq the preservation of memory invariants in selected parts of the interpreter. This work is an important first step towards a robust environment for formal verification of R programs.
值得信赖的机械化 JavaScript 规范
DOI：
10.1145/2535838.2535876
发表时间：
2014
期刊：
--
影响因子：
--
作者：
Bodin M
通讯作者：
Bodin M