Context: Container data types are ubiquitous in computer programming, enabling developers to efficiently store and process collections of data with an easy-to-use programming interface. Many programming languages offer a variety of container implementations in their standard libraries based on data structures offering different capabilities and performance characteristics. Inquiry: Choosing the *best* container for an application is not always straightforward, as performance characteristics can change drastically in different scenarios, and as real-world performance is not always correlated to theoretical complexity. Approach: We present Primrose, a language-agnostic tool for selecting the best performing valid container implementation from a set of container data types that satisfy *properties* given by application developers. Primrose automatically selects the set of valid container implementations for which the *library specifications*, written by the developers of container libraries, satisfies the specified properties. Finally, Primrose ranks the valid library implementations based on their runtime performance. Knowledge: With Primrose, application developers can specify the expected behaviour of a container as a type refinement with *semantic properties*, e.g., if the container should only contain unique values (such as a `set`) or should satisfy the LIFO property of a `stack`. Semantic properties nicely complement *syntactic properties* (i.e., traits, interfaces, or type classes), together allowing developers to specify a container's programming interface *and* behaviour without committing to a concrete implementation. Grounding: We present our prototype implementation of Primrose that preprocesses annotated Rust code, selects valid container implementations and ranks them on their performance. The design of Primrose is, however, language-agnostic, and is easy to integrate into other programming languages that support container data types and traits, interfaces, or type classes. Our implementation encodes properties and library specifications into verification conditions in Rosette, an interface for SMT solvers, which determines the set of valid container implementations. We evaluate Primrose by specifying several container implementations, and measuring the time taken to select valid implementations for various combinations of properties with the solver. We automatically validate that container implementations conform to their library specifications via property-based testing. Importance: This work provides a novel approach to bring abstract modelling and specification of container types directly into the programmer's workflow. Instead of selecting concrete container implementations, application programmers can now work on the level of specification, merely stating the behaviours they require from their container types, and the best implementation can be selected automatically.

翻译：背景：容器数据类型在计算机编程中无处不在，使开发者能够通过易用的编程接口高效存储和处理数据集合。许多编程语言在其标准库中提供了多种基于不同数据结构的容器实现，这些实现具有不同的能力和性能特征。问题：为应用程序选择"最佳"容器并非易事，因为性能特征在不同场景下可能发生剧烈变化，且实际性能与理论复杂度并不总是相关。方法：我们提出Primrose，一种与语言无关的工具，能从满足应用程序开发者给定"属性"的容器数据类型集合中，选择性能最佳的合法容器实现。Primrose自动筛选出符合"库规范"的合法容器实现集合，这些库规范由容器库开发者编写，且满足指定的属性。最后，Primrose根据运行时性能对合法库实现进行排序。知识：通过Primrose，应用程序开发者可以将容器的预期行为指定为带有"语义属性"的类型精化，例如容器应仅包含唯一值（如`set`）或应满足`stack`的LIFO属性。语义属性与"句法属性"（即trait、接口或类型类）形成良好互补，共同使开发者能够指定容器的编程接口"和"行为，而无需绑定到具体实现。依据：我们展示了Primrose的原型实现，该实现预处理带注解的Rust代码，选择合法容器实现并根据性能排序。然而，Primrose的设计与语言无关，易于集成到其他支持容器数据类型及trait、接口或类型类的编程语言中。我们的实现将属性和库规范编码为Rosette（SMT求解器的接口）中的验证条件，由后者确定合法容器实现集合。我们通过指定多个容器实现，并测量求解器为各种属性组合选择合法实现所花费的时间来评估Primrose。我们通过基于属性的测试自动验证容器实现是否符合其库规范。重要性：这项工作提供了一种新颖的方法，将容器类型的抽象建模与规范直接融入程序员的工作流程。应用程序开发者不再需要选择具体的容器实现，而是可以在规范层面工作，仅需声明其对容器类型所需的行为，最佳实现即可自动选择。