Many representations for sets are available in programming languages libraries. The paper focuses on sparse sets used, e.g., in some constraint solvers for representing integer variable domains which are finite sets of values, as an alternative to range sequence. We propose in this paper verified implementations of sparse sets, in three deductive formal verification tools, namely EventB, $\{log\}$ and Why3. Furthermore, we draw some comparisons regarding specifications and proofs.

翻译：许多编程语言库中提供了多种集合表示方法。本文聚焦于稀疏集的应用，例如在某些约束求解器中用于表示整数变量域（即值的有限集合）作为区间序列的替代方案。我们提出在三种演绎形式化验证工具——EventB、$\{log\}$和Why3中实现已验证的稀疏集。此外，我们还对其规约和证明进行了比较分析。