Probabilistic Datatypes
摘要
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.