Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law

Raphaël Monat, Aymeric Fromherz, Denis Merigoux

TL;DR

This work presents a novel, formal semantics for date computations, and formally establish several semantic properties through a mechanization in the F* proof assistant, and proposes a static analysis by abstract interpretation to automatically detect ambiguities in date computations.

Abstract

Legal expert systems routinely rely on date computations to determine the eligibility of a citizen to social benefits or whether an application has been filed on time. Unfortunately, date arithmetic exhibits many corner cases, which are handled differently from one library to the other, making faithfully transcribing the law into code error-prone, and possibly leading to heavy financial and legal consequences for users. In this work, we aim to provide a solid foundation for date arithmetic working on days, months and years. We first present a novel, formal semantics for date computations, and formally establish several semantic properties through a mechanization in the F* proof assistant. Building upon this semantics, we then propose a static analysis by abstract interpretation to automatically detect ambiguities in date computations. We finally integrate our approach in the Catala language, a recent domain-specific language for formalizing computational law, and use it to analyze the Catala implementation of the French housing benefits, leading to the discovery of several date-related ambiguities.

Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law

TL;DR

This work presents a novel, formal semantics for date computations, and formally establish several semantic properties through a mechanization in the F* proof assistant, and proposes a static analysis by abstract interpretation to automatically detect ambiguities in date computations.

Abstract

Legal expert systems routinely rely on date computations to determine the eligibility of a citizen to social benefits or whether an application has been filed on time. Unfortunately, date arithmetic exhibits many corner cases, which are handled differently from one library to the other, making faithfully transcribing the law into code error-prone, and possibly leading to heavy financial and legal consequences for users. In this work, we aim to provide a solid foundation for date arithmetic working on days, months and years. We first present a novel, formal semantics for date computations, and formally establish several semantic properties through a mechanization in the F* proof assistant. Building upon this semantics, we then propose a static analysis by abstract interpretation to automatically detect ambiguities in date computations. We finally integrate our approach in the Catala language, a recent domain-specific language for formalizing computational law, and use it to analyze the Catala implementation of the French housing benefits, leading to the discovery of several date-related ambiguities.
Paper Structure (11 sections, 12 theorems, 5 equations, 5 figures)

This paper contains 11 sections, 12 theorems, 5 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Formally Capturing Date Computations.
  3. Automatically Detecting Date Ambiguities.
  4. Contribution to Date Arithmetic Libraries.
  5. Case Study: Integration in the Catala Language.
  6. Formalizing Date Arithmetic
  7. Mechanizing Semantics
  8. Semantic properties
  9. Non-properties and counter-examples
  10. A Static Analysis For Rounding-Insensitivity
  11. The YMD domain combinator

Key Result

theorem thmcountertheorem

For any date $d$, and any integer $n$, there exists a value $v_\delta$ such that $d +_\delta n \overset{*}{\rightarrow}\xspace v_\delta$.

Figures (5)

  • Figure 1: Date expressions
  • Figure 2: Semantics for date addition
  • Figure 3: Semantics for date rounding
  • Figure 4: Example extracted from Catala code modeling the French housing benefits
  • Figure 5: Concretization of the YMD domain

Theorems & Definitions (15)

  • definition thmcounterdefinition: Ambiguous expression
  • theorem thmcountertheorem: Normalization
  • lemma thmcounterlemma: Well-formedness of day addition
  • lemma thmcounterlemma: Well-formedness of year/month addition
  • lemma thmcounterlemma: Well-formedness of rounding
  • theorem thmcountertheorem: Well-formedness
  • theorem thmcountertheorem: Monotonicity
  • lemma thmcounterlemma: Equivalence of year and month addition
  • lemma thmcounterlemma: Monotonicity of year and month addition
  • lemma thmcounterlemma: Monotonicity of day addition
  • ...and 5 more