Measurement of refinement and correctness

Abstract

The purpose of this paper is to introduce a measurement approach of refinement and correctness of probabilistic programs. That is, we define the refinement degree and the correctness degree by the weakest precondition transformers. This kind of measurement indicates the degree that a program is refined by another and the degree that a program is correct with respect to a pair of precondition and postcondition. Some properties of this measurement, for example continuity, are discussed.

Keywords

deterministic probabilistic program / nondeterministic probabilistic program / refinement degree / correctness degree