Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Transition-Oriented Programming: Developing Provably Correct Systems

Yepeng Ding

TL;DR

This work introduces Transition-Oriented Programming (TOP), a unifying paradigm built on Graph Transition Systems (GTSs) to integrate correctness specification, verification, and implementation within a single formal framework. It formalizes varying computation models (transition and rewriting systems) and logics (temporal and equational) and then grounds TOP in the Seni language, which supports modularization, progressive specification, context perception, and automated proof techniques (bounded model checking and iterative deepening theorem proving). The approach aims to produce provably correct systems by ensuring that a provably correct specification also yields a provably correct implementation, demonstrated across distributed protocols, security infrastructures, and program analysis contexts. The paper also outlines TOD and TOPA as development and analysis workflows, and sketches broad future directions including toolchains for compiling, explainable AI, and hardware design, underpinned by extensions to Seni and external proof assistants.

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.

Transition-Oriented Programming: Developing Provably Correct Systems

TL;DR

This work introduces Transition-Oriented Programming (TOP), a unifying paradigm built on Graph Transition Systems (GTSs) to integrate correctness specification, verification, and implementation within a single formal framework. It formalizes varying computation models (transition and rewriting systems) and logics (temporal and equational) and then grounds TOP in the Seni language, which supports modularization, progressive specification, context perception, and automated proof techniques (bounded model checking and iterative deepening theorem proving). The approach aims to produce provably correct systems by ensuring that a provably correct specification also yields a provably correct implementation, demonstrated across distributed protocols, security infrastructures, and program analysis contexts. The paper also outlines TOD and TOPA as development and analysis workflows, and sketches broad future directions including toolchains for compiling, explainable AI, and hardware design, underpinned by extensions to Seni and external proof assistants.

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.

Paper Structure

This paper contains 72 sections, 7 theorems, 31 equations, 15 figures, 1 table, 5 algorithms.

Table of Contents

  1. Introduction
  2. Correctness
  3. Formal Model
  4. Transition System
  5. Basic Transition System
  6. Kripke Structure
  7. Rewriting System
  8. Basic Rewriting System
  9. Graph Rewriting System
  10. Incomparability
  11. Formal Logic
  12. Temporal Logic
  13. Linear-Time Logic
  14. Branching-Time Logic
  15. Equational Logic
  16. ...and 57 more sections

Key Result

Proposition 2.1

If there exists a correctness verification $\leftindex^V{\textit{Corr}}$, such that $\leftindex^V{\textit{Corr}}(\mathfrak{M}, \Phi) = \top$, then $\mathfrak{M} \vdash \Phi$.

Figures (15)

  • Figure 1: Inclusion of demands, specifications, provable specifications, and provably correct systems.
  • Figure 2: Examples of transition systems.
  • Figure 3: Examples of Kripke structures.
  • Figure 4: Examples of rewriting systems.
  • Figure 5: Examples of node-labeled graphs.
  • ...and 10 more figures

Theorems & Definitions (79)

  • Definition 2.1: Transition System
  • Example 2.1: Transition System
  • Definition 2.2: Labeled Transition System
  • Example 2.2: Labeled Transition System
  • Definition 2.3: Kripke Structure
  • Example 2.3: Kripke Structure
  • Definition 2.4: Labeled Kripke Structure
  • Example 2.4: Labeled Kripke Structure
  • Definition 2.5: Abstract Rewriting System
  • Example 2.5: Abstract Rewriting System
  • ...and 69 more