论文标题

面向过渡的编程:开发可证明正确的系统

Transition-Oriented Programming: Developing Provably Correct Systems

论文作者

Ding, Yepeng

论文摘要

正确性是系统有效满足人类需求的必要条件,从而在系统开发中起着至关重要的作用。但是,正确性通常在实践中表现为一个模糊的概念,从而导致了准确创建规范的挑战,有效地证明了正确性的满足感并有效地实施了正确的系统。通过解决这些挑战的激励,本文介绍了以过渡为导向的编程(TOP),这是一种编程范式,旨在通过在一个统一的理论框架内交织正确性规范,验证和实施来促进可证明的正确系统的开发。

Correctness is a necessary condition for systems to be effective in meeting human demands, thus playing a critical role in system development. However, correctness often manifests as a nebulous concept in practice, leading to challenges in accurately creating specifications, effectively proving correctness satisfiability, and efficiently implementing correct systems. Motivated by tackling these challenges, this paper introduces Transition-Oriented Programming (TOP), a programming paradigm to facilitate the development of provably correct systems by intertwining correctness specification, verification, and implementation within a unified theoretical framework.

扫码加入交流群

加入微信交流群

微信交流群二维码

扫码加入学术交流群,获取更多资源