Formal semantics of Java expressions and statements

作     者：Zamulin, AV 

作者机构：Russian Acad Sci Ershov Inst Informat Syts Siberian Div Novosibirsk 630090 Russia 

出 版 物：《PROGRAMMING AND COMPUTER SOFTWARE》 (程序设计与计算机软件)

年 卷 期：2003年第29卷第5期

页      面：259-269页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：Java programming language 

摘      要：Using Java as a study language, we have defined the formal semantics of sometypical expressions and almost all statements of an object-oriented programming language. Thesemantics is based on the formal model of a program whose state is defined as a many-sorted *** the use of update sets for results of statement executions. This made it possible to definetheir semantics in a very simple way. If the alternative classical approach to defining the programstate as a complex abstract data type (see, e.g.,) were used, one would have to define additionallymany auxiliary operators and high-level functions, which, of course, would not facilitate thesemantics definition. Moreover, as noted long time ago, the application of the classical approach toobject-oriented programming languages is not justified, since it does not have adequate means formodeling such important notions as object identity and transformation of the object state withoutchanging its identity. This problem has been solved to some extent in [7] by using monads andcoalgebras; however, such an approach resulted in a very complex form of the semantics *** important problem to be solved is how to use this form of semantics for the program verificationand for the automation of program translation and interpretation. This is a subject of our furtherresearch.