带有数量的编程学科
摘要：物理和工程应用中经常使用以单位为体现的物理量（UoM）。火星气候轨道器的损失被归因于度量和英制单位系统之间的混淆，这使得错误处理测量值的灾难性后果变得普遍起来。维度分析可以用于确保包含注释值的表达式被正确评估。这导致了许多库、语言和验证器的开发，以确保开发人员可以在设计和代码中指定和验证UoM信息。许多工具还可以自动在相互可比的UoM之间进行转换，例如码和米。然而，这些系统不能区分数量和维度。例如，扭矩和功，它们共享相同的UoM，不能互换，因为它们不代表相同的实体。我们提出了一种命名数量层，通过确保不同数量的值得到安全管理，可以补充维度分析。我们的技术是分析和纪律的结合，涉及乘法的表达式被限制在函数中，以确保命名数量被正确处理。
作者：Steve McKeever
论文ID：2210.12359
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-10-25