下载PDF摘要:在法国,所得税是根据法国公共财政局(DGFiP)创作,设计和维护的,从纳税人的个人收益中计算得出的。该算法依赖于传统的自定义语言和最初于1990年设计的编译器,它与法国葡萄酒不同,没有随着时间的流逝而衰老。由于输入语言的不足和编译器的技术局限性,该算法越来越难以维护,它依靠临时行为和变通办法来实现税法的最新变化。能力丧失和代码老化也意味着该系统无法从任何可提高实现信心的现代编译器技术中受益。我们全面检查了此基础架构,并提出了Mlang,这是一个开源编译器工具链,其目标是替换现有的基础架构。 Mlang基于DGFiP系统的反向工程形式化,并且已针对privateDGFiP测试套件进行了全面验证。因此,Mlang具有形式语义。消除了C中以前的手写解决方法;编译为现代语言(Python);并启用各种工具,提供有关法国所得税计算本质的深刻见解。 DGFiP现在正式过渡到Mlang的生产系统。