An encapsulated datatype collects related data together with the operations used to access them. Datatype refinement then provides a clear separation between the expectations of programs that call the operations (i.e. from outside the encapsulation) and the implementation of the operations themselves (inside the encapsulation), and it enforces consistency between the two. In this paper we consider encapsulated probabilistic datatypes, i.e. those whose operations can “flip coins”; and we find as a result that the interface between calling programs’ expectations and their encapsulated probabilistic implementations must now provide consistency not only for functional properties but also for properties related to information flow. In this paper we use a quantitative information-flow model for programs to give a sound basis for refinement of probabilistic datatypes.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Probabilistic Datatypes

  • Chris Chen,
  • Annabelle McIver,
  • Carroll Morgan

摘要

An encapsulated datatype collects related data together with the operations used to access them. Datatype refinement then provides a clear separation between the expectations of programs that call the operations (i.e. from outside the encapsulation) and the implementation of the operations themselves (inside the encapsulation), and it enforces consistency between the two. In this paper we consider encapsulated probabilistic datatypes, i.e. those whose operations can “flip coins”; and we find as a result that the interface between calling programs’ expectations and their encapsulated probabilistic implementations must now provide consistency not only for functional properties but also for properties related to information flow. In this paper we use a quantitative information-flow model for programs to give a sound basis for refinement of probabilistic datatypes.