并发程序安全性与进展性质的双向证明
编程语言
2017-04-07 v1 计算机科学中的逻辑
摘要
本文提出了一种并发程序的可组合规约理论，允许：（1）针对给定规约验证程序代码，以及（2）组合各组件的规约以生成程序的规约。该规约既包含在程序执行结束时（若执行终止）成立的终止性质，也包含在整个执行过程中成立的永久性质。我们设计了（1）用于验证的证明技术，以及（2）从组件规约推导程序规约的组合规则。我们利用组件的终止性质推导程序的永久性质，反之亦然。因此，该证明策略被称为双向的。该理论的可组合性在由部分源代码可能不可用的组件组装程序时非常重要，正如跨供应商程序集成中日益出现的情况。
引用
@article{arxiv.1704.01814,
title = {Bilateral Proofs of Safety and Progress Properties of Concurrent Programs},
author = {Jayadev Misra},
journal= {arXiv preprint arXiv:1704.01814},
year = {2017}
}