论文标题
面向过渡的编程:开发可证明正确的系统
Transition-Oriented Programming: Developing Provably Correct Systems
论文作者
论文摘要
正确性是系统有效满足人类需求的必要条件,从而在系统开发中起着至关重要的作用。但是,正确性通常在实践中表现为一个模糊的概念,从而导致了准确创建规范的挑战,有效地证明了正确性的满足感并有效地实施了正确的系统。通过解决这些挑战的激励,本文介绍了以过渡为导向的编程(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.