.png){kind=icon}
返回
Co-Developing Programs and Their Proof of Correctness
.png){kind=icon}
OA
AI
DOI：10.1145/3624728.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
The SPARK programming language and analyzer. TWENTY YEARS AGO, Sir Tony Hoare proposed a grand challenge to the computing research community: to develop a verifying compiler [which] uses mathematical and logical reasoning to check the correctness of the programs that it compiles. Hoare went on to set demanding success criteria for this effort: If the project is successful, a verifying compiler will be available as a standard tool in some widely used programming productivity toolset.(26) While there have been some notable successes with program verification systems,a the use of such systems is still perceived as a niche activity for the most critical and specialized projects(1,23,29,30,34) Program verification systems based on automatic techniques have also emerged.(9,11,14,16,33) These systems occupy a middle ground in the landscape of verification techniques, between push-button tools that require minimal setup and fully interactive proof assistants. The approach has been called auto-activea portmanteau of automatic and interactive-where users develop the proof and the program at the same time through the use of assertions and other contracts in the programming language. The open source SPARK technology is a prominent member of that family, with a history dating back to 1987. The objective of this article is to explain the auto-active approach for co-developing programs and their proof of correctness, present the key design and technological choices that made SPARK industrially successful, and what this means for the future of SPARK or analyzers of that same family.
Keyword:
VERIFICATION
SOFTWARE
SPECIFICATION
期刊
IF:
12.2
论文数:
1.2W
被引数:
3.7W
机构
暂无机构信息
引用论文
.png){kind=icon}
分享收藏分享收藏
查看更多内容