Towards Substructural Property-Based Testing

TL;DR

This paper introduces a novel approach to property-based testing by extending it to substructural logics, specifically implementing a system for linear logic programming language Lolli, and validating it through encoding and mutation testing.

Contribution

It is the first to develop a property-based testing system for substructural logics, utilizing foundational proof certificates for data generation strategies.

Findings

Successfully encoded a simple imperative language and its compilation.

Validated the approach through mutation analysis.

Demonstrated the feasibility of property-based testing in substructural logics.

Abstract

We propose to extend property-based testing to substructural logics to overcome the current lack of reasoning tools in the field. We take the first step by implementing a property-based testing system for specifications written in the linear logic programming language Lolli. We employ the foundational proof certificates architecture to model various data generation strategies. We validate our approach by encoding a model of a simple imperative programming language and its compilation and by testing its meta-theory via mutation analysis.