SPARK 2014 中的安全指针
编程语言
2017-10-20 v1
摘要
在演绎软件验证的背景下，由于指针别名问题，包含指针的程序构成了重大挑战。本文中，我们将指针引入 SPARK——Ada 语言的一个定义明确的子集，旨在用于关键任务软件的形式化验证。我们的解决方案基于受 Rust 借用检查器和仿射类型启发的静态别名分析，并强制执行并发读、独占写原则。该分析已在 GNAT Ada 编译器中实现，并针对包括实际应用部分内容在内的若干具有挑战性的示例进行了测试。我们的测试表明，仅需对源代码进行微小改动，即可使惯用的 Ada 代码适应扩展了指针的 SPARK，这相较于以往的最优水平是一项显著改进。所提议的扩展已获 SPARK 语言设计委员会批准，将纳入未来版本的 SPARK，并正由 Ada 报告员小组讨论，以纳入下一版本的 Ada。在报告中，我们给出了 SPARK 微型版本分析规则的形式化表述，并证明了其可靠性。我们讨论了实现与案例研究，并将我们的解决方案与 Rust 进行了比较。
引用
@article{arxiv.1710.07047,
title = {Safe Pointers in SPARK 2014},
author = {Georges-Axel Jaloyan},
journal= {arXiv preprint arXiv:1710.07047},
year = {2017}
}