• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Verification, model checking, and abstract interpretation >Deciding Extensions of the Theories of Vectors and Bags
【24h】

Deciding Extensions of the Theories of Vectors and Bags

机译：确定向量和袋理论的扩展

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Vectors and bags are basic collection data structures, which are used frequently in programs and specifications. Reasoning about these data structures is supported by established algorithms for deciding ground satisfiability in the theories of arrays (for vectors) and multisets (for bags), respectively. Yet, these decision procedures are only able to reason about vectors and bags in isolation, not about their combination.rnThis paper presents a decision procedure for the combination of the theories of vectors and bags, even when extended with a function bagof bridging between vectors and bags. The function bagof converts vectors into the bags of their elements, thus admitting vector/bag comparisons. Moreover, for certain syntactically restricted classes of ground formulae decidability is retained if the theory of vectors is extended further with a map function which applies uninterpreted functions to all elements of a vector.
机译：向量和包装袋是基本的收集数据结构，在程序和规范中经常使用。这些数据结构的推理得到了既定算法的支持，这些算法分别在数组（对于矢量）和多集（对于包）的理论中确定地面可满足性。然而，这些决策程序仅能够孤立地推理向量和包，而不是它们的组合。rn本文提出了向量和包理论的组合的决策程序，即使在向量和包之间架桥的功能扩展时也是如此。袋。 bagof函数将向量转换为其元素的袋，从而允许进行向量/袋比较。此外，对于某些语法上受限制的地面公式类别，如果使用映射函数进一步扩展向量的理论，则可保留可判定性，该映射函数将未解释的函数应用于向量的所有元素。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号