Correct by construction

TL;DR

This paper introduces matrix code as a method to generate correct-by-construction algorithms, simplifying verification, especially for dense and precision-critical code, demonstrated through Quicksort partitioning and fast exponentiation.

Contribution

It presents matrix code as a novel approach to produce correct and verifiable code directly from algorithms, reducing verification effort.

Findings

Matrix code enables correct-by-construction programming.

The method is effective for dense and precision-critical code.

Illustrations include Quicksort partition and fast exponentiation.

Abstract

Matrix code allows one to discover algorithms and to render them in code that is both compilable and is correct by construction. In this way the difficulty of verifying existing code is avoided. The method is especially important for logically dense code and when precision programming is called for. The paper explains both these concepts. Logically dense code is explained by means of the partition stage of the Quicksort algorithm. Precision programming is explained by means of fast exponentiation.