Abstract
One of the efficient approaches to creating trusted software consists in the construction of a formal model that reflects its semantics and subsequent code verification with the use of this model. This work presents results of studies aimed at constructing a general model for description of static formal semantics of programs represented as a high-level intermediate code conforming to the ECMA-335 standard.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Benton, N., Kennedy, A., and Varming, C., Some Domain Theory and Denotational Semantics in Coq, TPHOLs, Berghofer, S., Nipkow, T., Urban, C., and Wenzel, M., Eds., LNCS, 2009, vol. 5674, pp. 115–130.
Balzy, S., Dargaye, Z., and Leroy, X., Formal Verification of a C Compiler Front-End, FM2006: Formal Methods, 2006, pp. 460–475.
ECMA-335: Common Language Infrastructure (CLI), Geneva, Switzerland: ECMA (European Association for Standardizing Information and Communication Systems), 2006, 4th edition.
Feldman, J.A., A Formal Semantics for Computer Languages and its Application in a Compiler-Compiler, Commun. ACM, 1966, vol. 9, no. 1, pp. 3–9.
Universal Multiple-Octet Coded Character Set (UCS), Geneva, Switzerland: ISO, 2003.
Binary Floating-Point Arithmetic for Microprocessor Systems, Geneva, Switzerland: International Electrotechnical Commission, 1989.
Codes for the Representation of Names of Countries, Geneva, Switzerland: ISO, 1988.
Codes for the Representation of Names of Languages, Geneva, Switzerland: ISO, 1988.
Schmidt, D.A., Denotational Semantics: a Methodology for Language Development, Dubuque, IA, USA: William C. Brown Publishers, 1986.
Kriticheski vazhnye ob’ekty i kiberterrorizm. Chast’ I. Sistemnyi podkhod k organizatsii protivodeistviya (Critically Important Objects and Cyberterrorism. Part 1: System Approach to Organization of Counteraction), Vasenin, V.A., Ed., Moscow: MTsNMO, 2008.
Kriticheski vazhnye ob’ekty i kiberterrorizm. Chast’ 2. Aspekty programmnoi realizatsii sredstv protivodeistviya (Critically Important Objects and Cyberterrorism. Part 2. Aspects of the Program Implementation of Counteraction Facilities), Vasenin, V.A., Ed., Moscow: MTsNMO, 2008.
Author information
Authors and Affiliations
Corresponding author
Additional information
Original Russian Text © V.A. Vasenin, M.A. Krivchikov, 2012, published in Programmirovanie, 2012, Vol. 38, No. 4.
Rights and permissions
About this article
Cite this article
Vasenin, V.A., Krivchikov, M.A. ECMA-335 static formal semantics. Program Comput Soft 38, 183–188 (2012). https://doi.org/10.1134/S0361768812040056
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1134/S0361768812040056