A high-level modular definition of the semantics of C\(_{\sharp}\). (English) Zbl 1080.68006
Summary: We propose a structured mathematical definition of the semantics of C\(_{\sharp}\) programs to provide a platform-independent interpreter view of the language for the C\(_{\sharp}\) programmer, which can also be used for a precise analysis of the ECMA standard of the language and as a reference model for teaching. The definition takes care to reflect directly and faithfully – as much as possible without becoming inconsistent or incomplete – the descriptions in the C\(_{\sharp}\) standard to become comparable with the corresponding models for Java in R. F. Stärk, J. Schmid and E. Börger’s book [Java and the Java virtual machine. Definition, verification, validation (2001; Zbl 0978.68033)] and to provide for implementors the possibility to check their basic design decisions against an accurate high-level model. The model sheds light on some of the dark corners of C\(_{\sharp}\) and on some critical differences between the ECMA standard and the implementations of the language.
Citations:
Zbl 0978.68033References:
| [1] | J.-R. Abrial, E. Börger, H. Langmaack, The steam boiler case study: competition of formal program specification and development methods, in: J.-R. Abrial, E. Börger, H. Langmaack (Eds.), Formal Methods for Industrial Applications. Specifying and Programming the Steam-Boiler Control, Lecture Notes in Computer Science, Vol. 1165, Springer, Berlin, 1996, pp. 1-12.; J.-R. Abrial, E. Börger, H. Langmaack, The steam boiler case study: competition of formal program specification and development methods, in: J.-R. Abrial, E. Börger, H. Langmaack (Eds.), Formal Methods for Industrial Applications. Specifying and Programming the Steam-Boiler Control, Lecture Notes in Computer Science, Vol. 1165, Springer, Berlin, 1996, pp. 1-12. · Zbl 1060.68501 |
| [2] | J. Alves-Foss, Formal Syntax and Semantics of Java, Lecture Notes in Computer Science, Vol. 1523, Springer, Berlin, 1998.; J. Alves-Foss, Formal Syntax and Semantics of Java, Lecture Notes in Computer Science, Vol. 1523, Springer, Berlin, 1998. |
| [3] | Archer, T.; Whitechapel, A., Inside \(C \sharp (2002)\), Microsoft Press |
| [4] | C. Beierle, E. Börger, I. Durdanović, U. Glässer, E. Riccobene, Refining abstract machine specifications of the steam boiler control to well documented executable code, in: J.-R. Abrial, E. Börger, H. Langmaack (Eds.), Formal Methods for Industrial Applications. Specifying and Programming the Steam-Boiler Control, Lecture Notes in Computer Science, Vol. 1165, Springer, Berlin, 1996, pp. 62-78.; C. Beierle, E. Börger, I. Durdanović, U. Glässer, E. Riccobene, Refining abstract machine specifications of the steam boiler control to well documented executable code, in: J.-R. Abrial, E. Börger, H. Langmaack (Eds.), Formal Methods for Industrial Applications. Specifying and Programming the Steam-Boiler Control, Lecture Notes in Computer Science, Vol. 1165, Springer, Berlin, 1996, pp. 62-78. |
| [5] | E. Börger, Abstract state machines: a unifying view of models of computation and of system design frameworks, Ann. Pure Appl. Logic (2005).; E. Börger, Abstract state machines: a unifying view of models of computation and of system design frameworks, Ann. Pure Appl. Logic (2005). · Zbl 1066.68047 |
| [6] | E. Börger, A logical operational semantics for full Prolog. Part I: selection core and control, in: E. Börger, H. Kleine Büning, M.M. Richter, W. Schönfeld (Eds.), CSL’89. 3rd Workshop on Computer Science Logic, Lecture Notes in Computer Science, Vol. 440, Springer, Berlin, 1990, pp. 36-64.; E. Börger, A logical operational semantics for full Prolog. Part I: selection core and control, in: E. Börger, H. Kleine Büning, M.M. Richter, W. Schönfeld (Eds.), CSL’89. 3rd Workshop on Computer Science Logic, Lecture Notes in Computer Science, Vol. 440, Springer, Berlin, 1990, pp. 36-64. · Zbl 0925.68301 |
| [7] | E. Börger, High-level system design and analysis using abstract state machines, in: D. Hutter, W. Stephan, P. Traverso, M. Ullmann (Eds.), Current Trends in Applied Formal Methods (FM-Trends 98), Lecture Notes in Computer Science, Vol. 1641, Springer, Berlin, 1999, pp. 1-43.; E. Börger, High-level system design and analysis using abstract state machines, in: D. Hutter, W. Stephan, P. Traverso, M. Ullmann (Eds.), Current Trends in Applied Formal Methods (FM-Trends 98), Lecture Notes in Computer Science, Vol. 1641, Springer, Berlin, 1999, pp. 1-43. |
| [8] | E. Börger, The ASM ground model method as a foundation of requirements engineering, in: N. Dershowitz (Ed.), Manna-Sympo., Lecture Notes in Computer Science, Vol. 2772, Springer, Berlin, 2003.; E. Börger, The ASM ground model method as a foundation of requirements engineering, in: N. Dershowitz (Ed.), Manna-Sympo., Lecture Notes in Computer Science, Vol. 2772, Springer, Berlin, 2003. |
| [9] | Börger, E., The ASM refinement method, Formal Aspects Comput., 15, 237-257 (2003) · Zbl 1093.68601 |
| [10] | E. Börger, T. Bolognesi, Remarks on turbo ASMs for computing functional equations and recursion schemes, in: E. Börger, A. Gargantini, E. Riccobene (Eds.), Abstract State Machines 2003—Advances in Theory and Applications, Lecture Notes in Computer Science, Vol. 2589, Springer, Berlin, 2003, pp. 218-228.; E. Börger, T. Bolognesi, Remarks on turbo ASMs for computing functional equations and recursion schemes, in: E. Börger, A. Gargantini, E. Riccobene (Eds.), Abstract State Machines 2003—Advances in Theory and Applications, Lecture Notes in Computer Science, Vol. 2589, Springer, Berlin, 2003, pp. 218-228. · Zbl 1021.68035 |
| [11] | E. Börger, K. Dässler, Prolog: DIN papers for discussion, ISO/IEC JTCI SC22 WG17 Prolog Standardization Document 58, National Physical Laboratory, Middlesex, England, 1990.; E. Börger, K. Dässler, Prolog: DIN papers for discussion, ISO/IEC JTCI SC22 WG17 Prolog Standardization Document 58, National Physical Laboratory, Middlesex, England, 1990. |
| [12] | E. Börger, N.G. Fruja, V. Gervasi, R. Stärk, A complete formal definition of the semantics of \(\operatorname{C} \sharp \); E. Börger, N.G. Fruja, V. Gervasi, R. Stärk, A complete formal definition of the semantics of \(\operatorname{C} \sharp \) |
| [13] | Börger, E.; Mearelli, L., Integrating ASMs into the software development life cycle, J. Univ. Comput. Sci., 3, 5, 603-665 (1997) · Zbl 0971.68051 |
| [14] | E. Börger, J. Schmid, Composition and submachine concepts for sequential ASMs, in: P. Clote, H. Schwichtenberg (Eds.), Computer Science Logic (Proc. CSL, 2000), Lecture Notes in Computer Science, Vol. 1862, Springer, Berlin, 2000, pp. 41-60.; E. Börger, J. Schmid, Composition and submachine concepts for sequential ASMs, in: P. Clote, H. Schwichtenberg (Eds.), Computer Science Logic (Proc. CSL, 2000), Lecture Notes in Computer Science, Vol. 1862, Springer, Berlin, 2000, pp. 41-60. · Zbl 0973.68066 |
| [15] | E. Börger, R.F. Stärk, Exploiting abstraction for specification reuse. The \(\operatorname{Java} / \operatorname{C} \sharp \); E. Börger, R.F. Stärk, Exploiting abstraction for specification reuse. The \(\operatorname{Java} / \operatorname{C} \sharp \) |
| [16] | 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 |
| [17] | M. Broy, S. Merz, K. Spies, Formal Systems Specification—The RPC-Memory Specification Case Study, Lecture Notes in Computer Science, Vol. 1169, Springer, Berlin, 1996.; M. Broy, S. Merz, K. Spies, Formal Systems Specification—The RPC-Memory Specification Case Study, Lecture Notes in Computer Science, Vol. 1169, Springer, Berlin, 1996. · Zbl 1060.68504 |
| [18] | Common Language Infrastructure, Standard ECMA-335, 2003,; Common Language Infrastructure, Standard ECMA-335, 2003, |
| [19] | Foundations of Software Engineering Group, Microsoft Research, AsmL, 2001, web pages at; Foundations of Software Engineering Group, Microsoft Research, AsmL, 2001, web pages at |
| [20] | N.G. Fruja, Specification and implementation problems for \(\operatorname{C} \sharp \); N.G. Fruja, Specification and implementation problems for \(\operatorname{C} \sharp \) |
| [21] | N.G. Fruja, The correctness of the definite assignment analysis in \(\operatorname{C} \sharp \); N.G. Fruja, The correctness of the definite assignment analysis in \(\operatorname{C} \sharp \) |
| [22] | N.G. Fruja, R.F. Stärk, The hidden computation steps of turbo abstract state machines, in: E. Börger, A. Gargantini, E. Riccobene (Eds.), Abstract State Machines 2003—Advances in Theory and Applications, Lecture Notes in Computer Science, Vol. 2589, Springer, Berlin, 2003, pp. 244-262.; N.G. Fruja, R.F. Stärk, The hidden computation steps of turbo abstract state machines, in: E. Börger, A. Gargantini, E. Riccobene (Eds.), Abstract State Machines 2003—Advances in Theory and Applications, Lecture Notes in Computer Science, Vol. 2589, Springer, Berlin, 2003, pp. 244-262. · Zbl 1021.68036 |
| [23] | A.D. Gordon, D. Syme, Typing a multi-language intermediate code, in: Proc. 28th Ann. ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, London, 2001, pp. 248-260.; A.D. Gordon, D. Syme, Typing a multi-language intermediate code, in: Proc. 28th Ann. ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, London, 2001, pp. 248-260. · Zbl 1323.68209 |
| [24] | Hartel, P.; Moreau, L., Formalizing the safety of Java, the Java Virtual Machine and Java Card, ACM Comput. Surv., 33, 4, 517-558 (2001) |
| [25] | Hejlsberg, A.; Wiltamuth, S.; Golde, P., \(C \sharp\) Language Specification (2003), Addison-Wesley: Addison-Wesley Reading, MA |
| [26] | J. Huggins, Broy-Lamport specification problem: a Gurevich abstract state machine solution, Tech. Report CSE-TR-320-96, EECS Department, University of Michigan, 1996.; J. Huggins, Broy-Lamport specification problem: a Gurevich abstract state machine solution, Tech. Report CSE-TR-320-96, EECS Department, University of Michigan, 1996. |
| [27] | \( \operatorname{C} \sharp \); \( \operatorname{C} \sharp \) |
| [28] | C. Lewerentz, T. Lindner, Formal development of reactive systems, Case Study “Production Cell”, Lecture Notes in Computer Science, Vol. 891, Springer, Berlin, 1995.; C. Lewerentz, T. Lindner, Formal development of reactive systems, Case Study “Production Cell”, Lecture Notes in Computer Science, Vol. 891, Springer, Berlin, 1995. · Zbl 0825.00053 |
| [29] | Mono compiler for \(\operatorname{C} \sharp \); Mono compiler for \(\operatorname{C} \sharp \) |
| [30] | Prosise, J., Programming Microsoft .NET (2002), Microsoft Press |
| [31] | Richter, J., Applied Microsoft .NET Framework Programming (2002), Microsoft Press |
| [32] | J. Schmid, Refinement and implementation techniques for abstract state machines, Ph.D. Thesis, University of Ulm, Germany, 2002.; J. Schmid, Refinement and implementation techniques for abstract state machines, Ph.D. Thesis, University of Ulm, Germany, 2002. |
| [33] | J. Schmid, Executing ASM specifications with AsmGofer, web pages at; J. Schmid, Executing ASM specifications with AsmGofer, web pages at |
| [34] | SSCLI (Rotor) web site,; SSCLI (Rotor) web site, |
| [35] | R.F. Stärk, E. Börger, An ASM specification of \(\operatorname{C} \sharp \); R.F. Stärk, E. Börger, An ASM specification of \(\operatorname{C} \sharp \) |
| [36] | 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 |
| [37] | Stutz, D.; Neward, T.; Shilling, G., Shared Source CLI Essentials (2003), O’Reilly: O’Reilly Sebastopol |
| [38] | D. Syme, Declarative theorem proving for operational semantics, Ph.D. Thesis, University of Cambridge, 1998.; D. Syme, Declarative theorem proving for operational semantics, Ph.D. Thesis, University of Cambridge, 1998. |
| [39] | Visual Studio .NET 2003,; Visual Studio .NET 2003, |
| [40] | W. Zimmermann, A. Dold, A framework for modeling the semantics of expression evaluation with abstract state machines, in: E. Börger, A. Gargantini, E. Riccobene (Eds.), Abstract State Machines 2003—Advances in Theory and Applications, Lecture Notes in Computer Science, Vol. 2589, Springer, Berlin, 2003, pp. 391-406.; W. Zimmermann, A. Dold, A framework for modeling the semantics of expression evaluation with abstract state machines, in: E. Börger, A. Gargantini, E. Riccobene (Eds.), Abstract State Machines 2003—Advances in Theory and Applications, Lecture Notes in Computer Science, Vol. 2589, Springer, Berlin, 2003, pp. 391-406. · Zbl 1021.68508 |
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.
