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.

翻译：法律专家系统通常依赖日期计算来确定公民是否具备社会福利资格，或申请是否按时提交。遗憾的是，日期算术存在许多边界情况，不同库的处理方式各异，导致将法律准确转录为代码容易出错，并可能给用户带来严重的财务和法律后果。本研究旨在为基于日、月、年的日期算术提供坚实基础。我们首先提出一种新颖的日期计算形式语义，并通过在F*证明助手上的机械化实现，正式确立了若干语义属性。基于此语义，我们进而提出一种基于抽象解释的静态分析方法，自动检测日期计算中的歧义。最后，我们将该方法集成到近期用于形式化计算法律的领域特定语言Catala中，并利用其分析法国住房补助的Catala实现，发现了若干与日期相关的歧义。