A Formal Description of an Incremental Type-Checker for Z

• Alexandre M. L. de Vasconcelos UFPE

DOI: https://doi.org/10.5753/sbes.1994.24464

Resumo

In this paper, we describe some of the difficulties that must be tackled when type-checking Z [1] specifications on an incremental basis. We formalise, in Z itself, the possible dependency relationships for each kind of Z definition. Then, we present an extensive list of issues that an incremental type-checking algorithm for Z must deal with, as well as an outline specification of an incremental type-checking algorithm which deals with these issues.

Palavras-chave: Incremental Type-Checking, Formal Specification, Z Notation

Referências

Spivey, J.M., The Z Notation: A Reference Manual - 1st edition, Prentice-Hall Intl. (1989).

Toyn, I., "Exploratory Environments for Functional Programming", D. Phil. Thesis. Department of Computer Science. University of York (Apr. 1987).

Spivey, J. M., Understanding Z: A Specification Language and its Formal Semantics. Cambridge University Press (Jan. 1988).

Atkins, M. C., "Implementation Techniques for Object-Oriented Systems", D.Phil. Thesis, Department of Computer Science, University of York (Jun. 1989).

Milner, R., "A Theory of Type Polymorphism in Programming", Journal of Computer and System Sciences 17(3), pp. 348-375 (Dec. 1978).

Sennet, C., "Review of Type Checking and Scope Rules of the Specification Language Z", Report No. 87017, Royal Signals and Radar Establishment, Malvern, UK (Nov. 1987).

Reed, J. N. and Sinclair, J. E., "An Algorithm for Type-Checking Z: A Z Specification", PRG-81, Programming Research Group, University of Oxford (Mar. 1990).

Hayes. I. (editor), Specification Case Studies, Prentice-Hall Intl. (1987).

de Vasconcelos, A. M. L., "Incremental Processing of Z Specifications", D.Phil. Thesis, Department of Computer Science, University of York (Oct. 1993).

Z Standards Review Commitee. "Z Base Standard (Version 1.0)", BSI Panel IST/5-/52 (1993).

Nikhil, R. S.. "Practical Polymorphism", Lecture Notes in Computer Science. Nancy. France 201. pp. 319-333, Springer-Verlag, Functional Programming Languages and Computer Architecture (Sep. 1985).

Toyn, I. and Runciman, C., "Performance Polymorphism". Lecture Notes in Computer Science, Proceedings of the Third International Conference on Functional Programming Languages and Computer Architecture (Sep. 1987).

R. Medina-Mora and P. H. Feiler, "An Incremental ing Environment", IEEE Transaction on Software Engineering SE-7(5), pp. 471-481 (Sep. 1981).

Nicol, C.. Crowe. M. K., Com. M. E., Oram, J. W. and Jenkins. D. G., "IDEA - An Incremental Development Environment for ADA", Software Engineering Journal (6), pp. 194-198 (Nov. 1987).

Schwarz, M. D., Delisle. N. M. and Begwani. V. S., "Incremental Compilation in Magpie", SIGPLAN Notices 19(6). pp. 122-131. Proceedings of the SIGPLAN Symposium on Compiler Construction (Jun. 1984).