A Formalization of the Common Type System and CLS Rules of ECMA Standard 335: 'Common Language Infrastructure'

ECMA Standard 335, “Common Language Infrastructure (CLI)”, was published in December 2001. According to Partition I, Section 1, it defines the Common Language Infrastructure (CLI) in which applications written in multiple high level languages may be executed in different system environments without the need to rewrite the application to take into consideration the unique characteristics of those environments. The standard is specified in natural language. Given the limitations of natural language, it is difficult to write a specification free of ambiguity and potential contradiction. Therefore, a formal model has been constructed in Z Notation of a subset of the Standard: the Common Type System (CTS) and many of the Common Language Specification (CLS) Rules. The model provides a framework for reasoning about the CTS and the CLS Rules, and establishes a base on which further areas of the Standard can be formalized. In the process of writing the formalisms, possible contradictions and ambiguities have been identified, which are discussed either in the body of the text or in the Appendices. In many cases the authors are confident that they have correctly interpreted the intention of the Standard;where they are not confident, the problems are described in Appendix E, Unresolved Questions.