Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Coverage Types for Resource-Based Policies

Angelo Passarelli, Gian-Luigi Ferrari

TL;DR

This work tackles the challenge of statically verifying resource policies while ensuring the completeness of input-test generators in Property-Based Testing. It introduces History Expressions to model latent resource effects (over-approximation) and Coverage Types to guarantee that input generators cover all relevant values (under-approximation), further enhanced by Extended Coverage Types that couple both aspects via a History Expression. A core language $\lambda^{\mathbf{TG}}$ is developed, featuring resource types, refinement types, and a history-aware type system that proves correctness and completeness together with policy verification, supported by algorithmic typing tools and a case study on palindromic word generation. The framework enables compositional reasoning about resource usage and generator coverage, with practical implications for secure API usage and robust PBT workflows, and points to future work in implementing the system and integrating it with existing PBT pipelines and theorem provers.

Abstract

Coverage Types provide a suitable type mechanism that integrates under-approximation logic to support Property-Based Testing. They are used to type the return value of a function that represents an input test generator. This allows us to statically assert that an input test generator not only produces valid input tests but also generates all possible ones, ensuring completeness. In this paper, we extend the coverage framework to guarantee the correctness of Property-Based Testing with respect to resource usage in the input test generator. This is achieved by incorporating into Coverage Types a notion of effect, which represents an over-approximation of operations on relevant resources. Programmers can define resource usage policies through logical annotations, which are then verified against the effect associated with the Coverage Type.

Coverage Types for Resource-Based Policies

TL;DR

This work tackles the challenge of statically verifying resource policies while ensuring the completeness of input-test generators in Property-Based Testing. It introduces History Expressions to model latent resource effects (over-approximation) and Coverage Types to guarantee that input generators cover all relevant values (under-approximation), further enhanced by Extended Coverage Types that couple both aspects via a History Expression. A core language is developed, featuring resource types, refinement types, and a history-aware type system that proves correctness and completeness together with policy verification, supported by algorithmic typing tools and a case study on palindromic word generation. The framework enables compositional reasoning about resource usage and generator coverage, with practical implications for secure API usage and robust PBT workflows, and points to future work in implementing the system and integrating it with existing PBT pipelines and theorem provers.

Abstract

Coverage Types provide a suitable type mechanism that integrates under-approximation logic to support Property-Based Testing. They are used to type the return value of a function that represents an input test generator. This allows us to statically assert that an input test generator not only produces valid input tests but also generates all possible ones, ensuring completeness. In this paper, we extend the coverage framework to guarantee the correctness of Property-Based Testing with respect to resource usage in the input test generator. This is achieved by incorporating into Coverage Types a notion of effect, which represents an over-approximation of operations on relevant resources. Programmers can define resource usage policies through logical annotations, which are then verified against the effect associated with the Coverage Type.

Paper Structure

This paper contains 26 sections, 8 theorems, 131 equations, 17 figures, 7 algorithms.

Table of Contents

  1. Introduction
  2. Overview
  3. History Expressions
  4. Coverage Types
  5. History Expressions
  6. $\alpha$-conversion History Expression
  7. Equality Relation
  8. Denotation
  9. Interpretation
  10. Policies
  11. Language & May-Types with Must-Types
  12. A Static Type System for Resource Policies
  13. Auxiliary Rules
  14. Type System
  15. Operational Semantic
  16. ...and 11 more sections

Key Result

Theorem 3.1

Given a History Expression $H$ and an interpretation $\mathcal{I}$ that maps each qualifier in $H$ with the value assigned by the interpretation itself, it holds that: This property tells us that for each terminal history $\eta$ that belongs to a History Expression $H$, there exists at least one interpretation $\mathcal{I}$ that satisfies the qualifiers taken into account by $H$ such that, by app

Figures (17)

  • Figure 2: Code that creates and opens a new file, and writes in a series of randomly generated numbers between 0 and 10 including extremes.
  • Figure 3: Equality Axioms of History Expressions
  • Figure 4: Definition of function Bind which aims to bind a variable within the qualifiers in the history.
  • Figure 5: Reduction Relation for History Expressions
  • Figure 6: Syntax of $\lambda^{\textbf{TG}}$ extended for resource use.
  • ...and 12 more figures

Theorems & Definitions (28)

  • Definition 3.1: History Expression
  • Definition 3.2: Resource Context
  • Definition 3.3: History Expression's Denotation without a Context
  • Definition 3.4: History Expression's Denotation under a Context
  • Theorem 3.1: Correctness of Denotation to Type Qualifiers
  • proof
  • proof : Correctness of $\alpha$-conversion rules
  • Definition 4.1: Ordering between events
  • Definition 4.2: Ownership of an event
  • Example 4.1
  • ...and 18 more