A New Method of Verification of Functional Programs

TL;DR

This paper introduces a novel approach for verifying functional programs over strings by analyzing their state diagrams, demonstrated through a sorting program example.

Contribution

It presents a new method that reduces FP verification to state diagram analysis, enabling property verification through composition of functional programs.

Findings

Verification reduces to state diagram analysis

Method successfully applied to sorting program

Provides a new framework for FP property verification

Abstract

In the paper the problem of verification of functional programs (FPs) over strings is considered, where specifications of properties of FPs are defined by other FPs, and a FP S1 meets a specification defined by another FP S2 iff a composition of functions defined by the FPs S1 and S2 is equal to the constant 1. We introduce a concept of a state diagram of a FP, and reduce the verification problem to the problem of an analysis of the state diagrams of FPs. The proposed approach is illustrated by the example of verification of a sorting program.