×

Towards proving type safety of \(\mathrm{C}^{\#}\). (English) Zbl 1387.68049

Summary: We consider a substantial subset of \(\mathrm{C}^{\#}\), named \(\mathrm{C}^{\#}_\mathcal{S}\). We develop a mathematical specification for \(\mathrm{C}^{\#}_\mathcal{S}\) by formalizing its abstract syntax, execution environment, well-typedness conditions, and operational evaluation semantics. Based on this specification, we prove that \(\mathrm{C}^{\#}_\mathcal{S}\) is type-safe by showing that the execution of \(\mathrm{C}^{\#}_\mathcal{S}\) programs preserves the types, up to a subtype relationship.

MSC:

68N15 Theory of programming languages
68N20 Theory of compilers and interpreters
68Q55 Semantics in the theory of computing

Software:

AsmL; LPTP; ML
PDFBibTeX XMLCite
Full Text: DOI

References:

[6] Fruja, N. G.; Börger, E., Modeling the .NET CLR exception handling mechanism for a mathematical analysis, Journal of Object Technology, 5, 3, 5-34 (2006)
[8] Gurevich, Y., Evolving algebras 1993: Lipari guide, (Börger, E., Specification and validation methods (1993), Oxford University Press: Oxford University Press Oxford), 9-36 · Zbl 0852.68053
[9] Börger, E.; Stärk, R. F., Abstract state machines. A method for high-level system design and analysis (2003), Springer: Springer Berlin · Zbl 1040.68042
[10] Börger, E.; Fruja, N. G.; Gervasi, V.; Stärk, R. F., A high-level modular definition of the semantics of \(C^{\#}\), Theoretical Computer Science, 336, 2-3, 235-284 (2005) · Zbl 1080.68006
[12] Stärk, R. F., Formal specification and verification of the \(C^{\#}\) thread model, Theoretical Computer Science, 343, 3, 482-508 (2005) · Zbl 1077.68054
[13] Stärk, R. F., The theoretical foundations of LPTP (a logic program theorem prover), Journal of Logic Programming, 36, 3, 241-269 (1998) · Zbl 0911.68030
[16] Fruja, N. G., The correctness of the definite assignment analysis in \(C^{\#}\)(extended version), Journal of Object Technology, 3, 9, 29-52 (2004)
[20] Jagger, J.; Perry, N.; Sestoft, P., \(C^{\#}\) annotated standard (2007), Elsevier: Elsevier Amsterdam · Zbl 1138.68347
[22] Pierce, B., Types and programming languages (2002), MIT Press: MIT Press Cambridge, MA
[23] Milner, R., A theory of type polymorphism in programming, Journal of Computer and System Sciences, 17, 348-375 (1978) · Zbl 0388.68003
[24] Cook, W. R., A proposal for making eiffel type-safe, Computer Journal, 32, 4, 305-311 (1989)
[25] Bruce, K. B., Safe type checking in a statically-typed object-oriented programming language, (POPL ’93: proceedings of the 20th symposium on principles of programming languages (1993), ACM Press: ACM Press Charleston, SC, USA), 285-298
[26] Bruce, K. B.; Crabtree, J.; Murtagh, T. P.; van Gent, R.; Dimock, A.; Muller, R., Safe and decidable type checking in an object-oriented language, (OOPSLA ’93: proceedings of the 8th conference on object-oriented programming systems, languages, and applications (1993), ACM Press: ACM Press Washington, DC, USA), 29-46
[29] Nipkow, T.; von Oheimb, D., \( \operatorname{Java}_{light}\) is type-safe—definitely, (POPL ’98: proceedings of the 25th symposium on principles of programming languages (1998), ACM Press: ACM Press San Diego, CA, USA), 161-170
[33] Stärk, R. F.; Schmid, J.; Börger, E., Java and the Java virtual machine—definition, verification, validation (2001), Springer: Springer Berlin · Zbl 0978.68033
[34] Hartel, P. H.; Moreau, L., Formalizing the safety of java, the java virtual machine, and java card, ACM Computer Surveys, 33, 4, 517-558 (2001)
[36] Gurevich, Y.; Huggins, J. K., The semantics of the C programming language, (Börger, E.; Jäger, G.; Kleine-Büning, H.; Martini, S.; Richter, M. M., CSL ’92: selected papers from the 6th workshop on computer science logic, San Miniato, Italy (1993), Springer: Springer Berlin), 274-308 · Zbl 0788.68018
[37] Wallace, C., The semantics of the \(C ++\) programming language, (Specification and validation methods (1995), Oxford University Press, Inc.: Oxford University Press, Inc. Oxford), 131-164 · Zbl 0852.68013
[41] Kutter, P. W.; Pierantonio, A., The formal specification of Oberon, Journal of Universal Computer Science, 3, 5, 443-503 (1997) · Zbl 0960.68112
[42] Börger, E.; Rosenzweig, D., A mathematical definition of full Prolog, Science of Computer Programming, 24, 3, 249-286 (1995) · Zbl 0832.68022
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.