Towards substructural property-based testing

DOI10.1007/978-3-030-98869-2_6MaRDI QIDQ6102253zbMATH OpenOpenAlexFDO

Authors Marco Mantovani, Alberto Momigliano

Publication date 8 May 2023

Published in Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2108.01610, http://hdl.handle.net/2434/922029

zbMATH Keywords

linear logicfocusingsemantics of programming languagesproperty-based testing

Mathematics Subject Classification ID

Theory of programming languages (68N15) Randomized algorithms (68W20) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

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.

Recommendations

• Foundational property-based testing
• Beginner's luck: a language for property-based generators
• Do judge a test by its cover. Combining combinatorial and property-based testing
• CurryCheck: checking properties of Curry programs
• Functional Testing in the Focal Environment

Cites work

• scientific article; zbMATH DE number 1670740 (Why is no real title available?)
• A linear logical framework
• A meta linear logical framework
• A semantic framework for proof evidence
• A two-level logic approach to reasoning about computations
• A type system for logic programs
• Abella: a system for reasoning about relational specifications
• Automatic proof and disproof in Isabelle/HOL
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• Celf – A Logical Framework for Deductive and Concurrent Systems (System Description)
• Efficient resource management for linear logic proof search
• Focusing and polarization in linear, intuitionistic, and classical logics
• Formalization of metatheory of the Quipper quantum programming language in a linear logic
• Forum: A multiple-conclusion specification logic
• Foundational property-based testing
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Linear logic
• Logic programming in a fragment of intuitionistic linear logic
• Mechanized semantics
• Reasoning with higher-order abstract syntax in a logical framework
• Semantics engineering with PLT Redex
• Substructural logics: a primer
• Testing noninterference, quickly
• The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof
• Translating between implicit and explicit versions of proof
• Types for Proofs and Programs
• Uniform proofs as a foundation for logic programming
• \textsc{Lincx}: a linear logical framework with first-class contexts
• αCheck: A mechanized metatheory model checker

Cited in

(5)

• Do judge a test by its cover. Combining combinatorial and property-based testing
• Functional Testing in the Focal Environment
• CurryCheck: checking properties of Curry programs
• Foundational property-based testing
• Generating tests by example

This page was built for publication: Towards substructural property-based testing

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6102253)