Transition-Oriented Programming: Developing Provably Correct Systems

TL;DR

This paper introduces Transition-Oriented Programming (TOP), a new paradigm that integrates correctness specification, verification, and implementation to help develop provably correct systems more effectively.

Contribution

It presents a unified theoretical framework for TOP, addressing challenges in specifying, verifying, and implementing correct systems.

Findings

TOP provides a formal foundation for correctness in system development

The paradigm simplifies the process of creating provably correct systems

It enhances the reliability of systems through integrated correctness methods

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.