Transition-Oriented Programming: Developing Provably Correct Systems
Programming Languages
2024-02-23 v3
Abstract
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.
Cite
@article{arxiv.2009.06029,
title = {Transition-Oriented Programming: Developing Provably Correct Systems},
author = {Yepeng Ding},
journal= {arXiv preprint arXiv:2009.06029},
year = {2024}
}