{"title":"PZ: A Z-based Formalism for Modeling Probabilistic Behavior","authors":"Hassan Haghighi","volume":37,"journal":"International Journal of Computer and Information Engineering","pagesStart":29,"pagesEnd":38,"ISSN":"1307-6892","URL":"https:\/\/publications.waset.org\/pdf\/1920","abstract":"Probabilistic techniques in computer programs are becoming\r\nmore and more widely used. Therefore, there is a big\r\ninterest in the formal specification, verification, and development\r\nof probabilistic programs. In our work-in-progress project, we are\r\nattempting to make a constructive framework for developing probabilistic\r\nprograms formally. The main contribution of this paper\r\nis to introduce an intermediate artifact of our work, a Z-based\r\nformalism called PZ, by which one can build set theoretical models of\r\nprobabilistic programs. We propose to use a constructive set theory,\r\ncalled CZ set theory, to interpret the specifications written in PZ.\r\nSince CZ has an interpretation in Martin-L\u252c\u00bfof-s theory of types, this\r\nidea enables us to derive probabilistic programs from correctness\r\nproofs of their PZ specifications.","references":"[1] Audebaud, P., Paulin-Mohring, C.: Proofs of Randomized Algorithms in\r\nCoq. In: MPC 2006, LNCS, vol. 4014, pp. 49-68 (2006)\r\n[2] King, S.: Z and the Refinement Calculus. In: VDM-90, LNCS 428,\r\nSpringer-Verlag, pp. 164-188 (1990)\r\n[3] Kozen, D.: Semantics of Probabilistic Programs. Journal of Computer and\r\nSystem Sciences, pp. 328-350 (1981)\r\n[4] Haghighi, H., Mirian-Hosseinabadi, S.H.: An Approach to Nondeterminism\r\nin Translation of CZ Set Theory into Type Theory. In: FSEN 2005,\r\nENTCS 159 (2006)\r\n[5] Haghighi, H., Mirian-Hosseinabadi, S.H.: Nondeterminism in Constructive\r\nZ. Fundamenta Informaticae, vol. 88 (1-2), pp. 109-134 (2008)\r\n[6] Haghighi, H.: Nondeterminism in CZ Specification Language. Ph.D.\r\ndissertation, Sharif Univ. of Technology, Iran, (2009)\r\n[7] Martin-L\u252c\u00bfof, P.: An Intuitionistic Theory of Types: Predicative Part. (H.E.\r\nRose, J.C. Sheperdson, Eds.), North Holland, pp. 73-118 (1975)\r\n[8] McIver, A., Morgan, C.: Abstraction and Refinement in Probabilistic\r\nSystems. ACM SIGMETRICS Performance Evaluation Review, vol. 32 ,\r\nno. 4, pp. 41-47 (2005)\r\n[9] McIver, A., Morgan, C.: Developing and Reasoning About Probabilistic\r\nPrograms in pGCL. LECTURE NOTES IN COMPUTER SCIENCE, pp.\r\n123-155 (2006)\r\n[10] Mirian-Hosseinabadi, S.H.: Constructive Z. Ph.D. dissertation, Essex\r\nUniv. (1997)\r\n[11] Morgan, C., McIver, A.: pGCL: Formal Reasoning for Random Algorithms.\r\nSouthern African Computer Journal (1999)\r\n[12] Morgan, C., McIver, A., Hurd, J.: Probabilistic Guarded Commands\r\nMechanised in HOL. Theoretical Computer Science, pp. 96-112 (2005)\r\n[13] Nordstrom, B., Petersson, K., Smith, J.M.: Programming in Martin-L\u252c\u00bfof-s\r\nType Theory: An Introduction. Oxford University Press (1990)\r\n[14] Park, S., Pfenning, F., Thrun, S.: A Probabilistic Language Based Upon\r\nSampling Functions. In: ACM Symp. on Principles of Prog. Lang., pp.\r\n171-182 (2005)\r\n[15] Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall (1989)\r\n[16] Thompson, S.: Haskell: The Craft of Functional Programming, 2nd ed.\r\nAddison-Wesley (1999)\r\n[17] Woodcock, J.: An Introduction to Refinement in Z. In: VDM-91, LNCS\r\n552, Springer-Verlag, vol. 2, pp. 96-117 (1991)\r\n[18] Woodcock, J. and Davies, J.: Using Z, Specifications, Refinement and\r\nProof. Prentice Hall (1996)","publisher":"World Academy of Science, Engineering and Technology","index":"Open Science Index 37, 2010"}