论文标题
希伯来日历的属性
Properties of the Hebrew Calendar
论文作者
论文摘要
我们描述了一个实现希伯来语日历的ACL2程序，并对其几个属性进行了正式验证，包括确定新一年放置的算法确保每年的长度属于一小部分可允许的值的关键结果。尽管基础论点中有微妙之处，但这些属性已被接受了许多世纪，但没有明确的证据。为了吸引广泛的受众，该程序以限制算法C（RAC）进行编码，这是一种简单的语言，该语言由C的最基本结构组成，为其自动转换为ACL2逻辑。尽管RAC主要用于建模算术硬件设计，但该新颖的应用程序提供了对语言和翻译人员的相对简单说明。
We describe an ACL2 program that implements the Hebrew calendar and the formal verification of several of its properties, including the critical result that the algorithm that determines the placement of the new year ensures that the length of every year belongs to a small set of admissible values. These properties have been accepted for many centuries without the benefit of explicit proof, in spite of subtleties in the underlying arguments. For the sake of accessibility to a broad audience, the program is coded in Restricted Algorithmic C (RAC), a simple language consisting of the most basic constructs of C, for which an automatic translator to the ACL2 logic has been implemented. While RAC is primarily intended for modeling arithmetic hardware designs, this novel application provides a relatively simple illustration of the language and the translator.
