Abstract

Continuous randomvariables are widely used to mathematically describe random phenomena in engineering and the physical sciences. In this paper, we present a higher-order logic formalization of the StandardUniformrandomvariable as the limit value of the sequence of its discrete approximations. We then show the correctness of this specification by proving the corresponding probability distribution properties within the HOL theorem prover, summarizing the proof steps. The formalized StandardUniformrandomvariable can be transformed to formalize other continuous randomvariables, such as Uniform, Exponential, Normal, etc., by using various non-uniformrandom number generation techniques. The formalization of these continuous randomvariables will enable us to perform an error free probabilistic analysis of systems within the framework of a higher-order-logic (HOL) theorem prover. For illustration purposes, we present the formalization of the Continuous Uniformrandomvariable based on the formalized StandardUniformrandomvariable, and then utilize it to perform a simple probabilistic analysis of roundoff error in HOL.