Nondeterminism in Constructive Z

• Autorzy: Haghigh H. , Mirian-Hosseinabadi S-H.
• Języki publikacji: EN

Abstrakty

EN

The abstraction inherent in most specifications and the need to specify nondeterministic programs are two well-known sources of nondeterminism in formal specifications. In this paper, we present a Z-based formalism by which one can specify bounded, unbounded, erratic, angelic, demonic, loose, strict, singular, and plural nondeterminism. To interpret our specifications, we use a constructive set theory, called CZ set theory, instead of the classical set theory Z. We have chosen CZ since it allows us to investigate the notion of nondeterminism from the formal program development point of view. In this way, we formally construct functional programs from Z specifications and then probe the effects of the initially specified nondeterminism on final programs. Our investigation shows that without specifying nondeterminism explicitly, the effects of the nondeterminism involved in initial specifications will not be preserved in final programs. We prove that using the new formalism, proposed by this paper, for writing nondeterministic specifications leads to programs that preserve the initially specified modalities of nondeterminism.

Słowa kluczowe

EN

formal specifications; formal program development; constructive Z; Martin-Löf's theory of types; nondeterminism; modalities of nondeterminism

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 88, nr 1-2
• Strony: 109--134
• Opis fizyczny: bibliogr. 27 poz.

Twórcy

autor

Haghigh H.

autor

Mirian-Hosseinabadi S-H.

• Department of Computer Engineering Sharif University of Technology, USA,

Bibliografia

• [1] Aczel, P.: The Type Theoretical Interpretation of Constructive Set Theory: Inductive Definitions, Logic, Methodology and Philosophy of Science VII, Elsevier Science Publishers B.V., l986, 17-49.
• [2] Bishop, E., Bridges, D.: Constructive Analysis, Springer-Verlag, 1985.
• [3] Cavalcanti, A., Woodcock, J.: Angelic Nondeterminism and Unifying Theories of Programming (Extended Version), Department of Computer Science, University of Kent, Technical Report No. 13-04, 2004.
• [4] Cazorla, D., Cuartero, F., Valero, V., Pelayo, F. L.: Algebraic Theory of Probabilistic and Nondeterministic Processes, Technical Report DIAB-01-01-19, University of Castilla-La Mancha, Spain, 2001.
• [5] Celiku, O., von Wright, J.: Correctness and Refinement of Dually Nondeterministic Programs, TUCS Technical Reports, No. 516, 2003.
• [6] Evans, A. S.: An Imoroved Recipe for Specifying Reactive Systems in Z, in ZUM '97: Z Formal Specification Notation. Proc. 11th Internationa Conference of Z Users., Springer-Verlag, 1997, 275-294.
• [7] Haghighi, H., Mirian-Hosseinabadi, S. H.: An Approach to Nondeterminism in Translation of CZ Set Theory into Type Theory, Proc. of the IPM Inter. Workshop of Found. of Soft. Eng., ENTCS 159, 2006.
• [8] Haghighi, H., Mirian-Hosseinabadi, S. H.: Formal Development of Two Player Games: A Constructive Approach, Proc. 12th Annual CSI Computer Conference (CSICC 2007), Tehran, Iran, 2007.
• [9] Haghighi, H., Mirian-Hosseinabadi, S. H.: Nondeterminism in Constructive Z, Software Quality Research Lab., Comp. Eng. Department, Sharif Univ. of Tec., "http://ce.sharif.edu/_mirian/techreport.html", 2008.
• [10] Hesselink, W. H.: Modalities of Nondeterminacy, Springer-Verlag, 1991.
• [11] King, S.: Z and the Refinement Calculus, Proc. VDM'90, LNCS 428, Springer-Verlag, 1990, 164-188.
• [12] Kozen, D.: Semantics of Probabilistic Programs, Journal of Comp. and Sys. Sci., Vol. 22, 1981, 328-350.
• [13] Martin, C. E., Curtis, S. A.: Modelling Nondeterminism, Proc. Mathematics of Program Construction conference, Lecture Notes in Computer Science, number 3125, 2004, 228-251.
• [14] Martin-Löf, P.: An Intuitionistic Theory of Types: Predicative Part, Proc. Logic Colloquium 73 (H.E. Rose, J.C. Sheperdson, Eds.), North Holland, 1975, 73-118.
• [15] McIver, A., Morgan, C.: Demonic, Angelic and Unbounded Probabilistic Choices in Sequential Programs, Acta Informatica, 37(4/5), 2000, 329-354.
• [16] Mirian-Hosseinabadi, S. H.: Constructive Z, PhD Thesis, University of Essex, UK, 1997.
• [17] Mislovea, M., Ouaknineb, J., Worrella, J.: Axioms for Probability and Nondeterminism, Electronic Notes in Theoretical Computer Science 96 (2004), Elsevier Press, 2004, 7-28.
• [18] Morris, J. M., Bunkenburg, A.: Partiality and Nondeterminacy in Program Proofs, Formal Aspects of Computing, 3(1), 1999.
• [19] Myhill, J.: Constructive Set Theory, The Journal of Symbolic Logic, 40(3), 1975, 347-382.
• [20] Nordström, B., Petersson, K., Smith, J. M.: Programming in Martin-Löf's Type Theory: An Introduction, Oxford University Press, 1990.
• [21] Pitcher, C. S.: Functional Programming and Erratic Non-determinism, PhD Thesis, Trinity College, Oxford University Computing Laboratory, 2001.
• [22] Spiliopoulou, E.: Concurrent and Distributed Functional Systems, PhD Thesis, Department of Computer Science, University of Bristol, 1999.
• [23] Spivey, J. M.: The Z Notation: A Reference Manual, Prentice Hall, 1989.
• [24] Varacca, D.: Probability, Nondeterminism and Concurrency: Two Denotational Models for Probabilistic Computation, PhD Thesis, Department of Computer Science, University of Aarhus, Denmark, 2003.
• [25] Walicki, M., Meldal, S.: Singular and Plural Nondeterministic Parameters, SIAM J. Comput., 26(4), 1997, 991-1005.
• [26] Ward, N. T. E.: A Refinement Calculus for Nondeterministic Expressions, PhD Thesis, Department of Computer Science, University of Queensland, Australia, 1994.
• [27] Woodcock, J., Davies, J.: Using Z, Specifications, Refinement and Proof, Prentice Hall, 1996.