增量 units-of-measure 验证
Incremental units-of-measure verification
AI总结：
提出一种支持增量标注的轻量级静态验证系统，通过生成全局约束系统为 Fortran 程序推断和检查多态 units-of-measure 规范，实现模块独立求解以扩展至大型项目。
摘要：
尽管有大量被提出的系统，但在科学计算中，程序内的 units-of-measure 验证仍然很少见。我们试图通过为 Fortran 程序中的 units-of-measure 提供一个轻量级的静态验证系统来解决这个问题，该系统支持大型项目的增量标注。我们采取了与 units-of-measure 类型化（在 F# 中）最主流的现有部署相反的方法，为程序生成一个全局的而非局部的约束系统。我们展示了这样一个系统能够为程序中欠定的部分推断（并检查）多态 units 规范。这种能力不仅允许检查部分标注的程序，而且还允许对全局约束问题进行分区。这种分区意味着我们可以通过独立求解每个程序模块的约束并存储模块边界处的推断 units（separate verification）来扩展到大型程序。我们提供了我们方法的实现，作为开源 Fortran 分析工具的扩展。
英文摘要：
Despite an abundance of proposed systems, the verification of units-of-measure within programs remains rare in scientific computing. We attempt to address this issue by providing a lightweight static verification system for units-of-measure in Fortran programs which supports incremental annotation of large projects. We take the opposite approach to the most mainstream existing deployment of units-of-measure typing (in F#) and generate a global, rather than local, constraints system for a program. We show that such a system can infer (and check) polymorphic units specifications for under-determined parts of the program. Not only does this ability allow checking of partially annotated programs but it also allows the global constraint problem to be partitioned. This partitioning means we can scale to large programs by solving constraints for each program module independently and storing inferred units at module boundaries (separate verification). We provide an implementation of our approach as an extension to an open-source Fortran analysis tool.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
