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.

翻译：正确性对于系统有效满足人类需求是必要条件，因此在系统开发中起着关键作用。然而，在实践中，正确性常表现为一个模糊的概念，导致在精确创建规范、有效证明正确性可满足性以及高效实现正确系统方面面临诸多挑战。为应对这些挑战，本文引入了面向转换的编程（TOP），这是一种通过将正确性规范、验证与实现在统一的理论框架内交织，从而促进开发可证明正确系统的编程范式。