一句话：将整数内化到关系，扩展 Alloy 以优雅支持定量需求，并提供基于 SMT 的无界分析引擎。
Alloy 以关系逻辑为形式软件设计提供了优雅的规约语言，但其关系逻辑难以表达同时涉及结构与数量约束的问题。本文提出 QAlloy，将整数数量内化到关系之中，使域元素之间的关联带有定量属性，从而能用类似结构需求的方式书写定量需求，并借助类型系统提供基本的量纲分析支持。QAlloy Analyzer 还实现了一个基于 SMT 的分析引擎，使数量可以无界，从而避免 Alloy 当前有界整数语义带来的诸多问题。该工作展示了语言扩展及分析器设计，说明定量关系建模的可行性与优雅性。
Alloy is a popular language and tool for formal software design. A key factor to this popularity is its relational logic, an elegant specification language with a minimal syntax and semantics. However, many software problems nowadays involve both structural and quantitative requirements, and Alloy's relational logic is not well suited to reason about the latter. This paper introduces QAlloy, an extension of Alloy with quantitative relations that add integer quantities to associations between domain elements. Having integers internalised in relations, instead of being explicit domain elements like in standard Alloy, allows quantitative requirements to be specified in QAlloy with a similar elegance to structural requirements, with the side-effect of providing basic dimensional analysis support via the type system. The QAlloy Analyzer also implements an SMT-based engine that enables quantities to be unbounded, thus avoiding many problems that may arise with the current bounded integer semantics of Alloy.