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. |