PZ: A Z-based Formalism for Modeling Probabilistic Behavior

Authors: Hassan Haghighi

Abstract:

Probabilistic techniques in computer programs are becoming more and more widely used. Therefore, there is a big interest in the formal specification, verification, and development of probabilistic programs. In our work-in-progress project, we are attempting to make a constructive framework for developing probabilistic programs formally. The main contribution of this paper is to introduce an intermediate artifact of our work, a Z-based formalism called PZ, by which one can build set theoretical models of probabilistic programs. We propose to use a constructive set theory, called CZ set theory, to interpret the specifications written in PZ. Since CZ has an interpretation in Martin-L¨of-s theory of types, this idea enables us to derive probabilistic programs from correctness proofs of their PZ specifications.

Keywords: formal specification, formal program development, probabilistic programs, CZ set theory, type theory.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1056098

References:

[1] Audebaud, P., Paulin-Mohring, C.: Proofs of Randomized Algorithms in Coq. In: MPC 2006, LNCS, vol. 4014, pp. 49-68 (2006)
[2] King, S.: Z and the Refinement Calculus. In: VDM-90, LNCS 428, Springer-Verlag, pp. 164-188 (1990)
[3] Kozen, D.: Semantics of Probabilistic Programs. Journal of Computer and System Sciences, pp. 328-350 (1981)
[4] Haghighi, H., Mirian-Hosseinabadi, S.H.: An Approach to Nondeterminism in Translation of CZ Set Theory into Type Theory. In: FSEN 2005, ENTCS 159 (2006)
[5] Haghighi, H., Mirian-Hosseinabadi, S.H.: Nondeterminism in Constructive Z. Fundamenta Informaticae, vol. 88 (1-2), pp. 109-134 (2008)
[6] Haghighi, H.: Nondeterminism in CZ Specification Language. Ph.D. dissertation, Sharif Univ. of Technology, Iran, (2009)
[7] Martin-L¨of, P.: An Intuitionistic Theory of Types: Predicative Part. (H.E. Rose, J.C. Sheperdson, Eds.), North Holland, pp. 73-118 (1975)
[8] McIver, A., Morgan, C.: Abstraction and Refinement in Probabilistic Systems. ACM SIGMETRICS Performance Evaluation Review, vol. 32 , no. 4, pp. 41-47 (2005)
[9] McIver, A., Morgan, C.: Developing and Reasoning About Probabilistic Programs in pGCL. LECTURE NOTES IN COMPUTER SCIENCE, pp. 123-155 (2006)
[10] Mirian-Hosseinabadi, S.H.: Constructive Z. Ph.D. dissertation, Essex Univ. (1997)
[11] Morgan, C., McIver, A.: pGCL: Formal Reasoning for Random Algorithms. Southern African Computer Journal (1999)
[12] Morgan, C., McIver, A., Hurd, J.: Probabilistic Guarded Commands Mechanised in HOL. Theoretical Computer Science, pp. 96-112 (2005)
[13] Nordstrom, B., Petersson, K., Smith, J.M.: Programming in Martin-L¨of-s Type Theory: An Introduction. Oxford University Press (1990)
[14] Park, S., Pfenning, F., Thrun, S.: A Probabilistic Language Based Upon Sampling Functions. In: ACM Symp. on Principles of Prog. Lang., pp. 171-182 (2005)
[15] Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall (1989)
[16] Thompson, S.: Haskell: The Craft of Functional Programming, 2nd ed. Addison-Wesley (1999)
[17] Woodcock, J.: An Introduction to Refinement in Z. In: VDM-91, LNCS 552, Springer-Verlag, vol. 2, pp. 96-117 (1991)
[18] Woodcock, J. and Davies, J.: Using Z, Specifications, Refinement and Proof. Prentice Hall (1996)