...
首页> 外文期刊>Programming and Computer Software >An ASM-based Formal Model of a Java Program
【24h】

An ASM-based Formal Model of a Java Program

机译:Java程序的基于ASM的形式模型

获取原文
获取原文并翻译 | 示例
           

摘要

We have introduced a formal model (high-level operational machine) of a sequential Java-like program in the style of abstract state machines. An algebraic model of an object class of an object-oriented programming language has been elaborated with this aim. As a result, the denotational semantics of the basic class components (fields, constructors, and methods) has been defined for the subsequent use for interpreting expressions and statements. This is the denotational part of the approach suggested. The transition of our machine from one state to another is the operational part of the approach. The use of the formal operational machine made it possible to get a high level of abstraction, which cannot be obtained in a pure operational approach, and simplicity of mapping, which cannot be obtained in a pure denotational approach based on the use of some universal mathematical structures as denotations. Each object in our machine possesses a state and a unique identity. An object identity is represented by a reference that is an element of a special reference sort. The state is represented by a number of instance variables, whose values can be updated. These variables are naturally defined in the model as functions on the sets of references undefined on the value null. The object state can be observed or updated by a method that is a state-dependent function. The result of an updating method is an update set, which is a well-defined mathematical structure. Therefore, the semantics of such a method is given by a set of functions producing update sets. The state is an implicit parameter for all method declarations and an implicit result for state updating methods, like in Java and other object-oriented pro- gramming languages. This also allowed us to make the declaration methods similar to their declarations in Java-like languages. We have shown that our model supports all important aspects of Java-like languages, namely, inheritance, overloading, overriding, and late binding. Because of lack of space, several interesting aspects of the model have not been presented in this paper. Primarily, this concerns expressions, statements, and exceptions, which will be considered in a following paper. Local class definitions, multipackage programs, dynamic class loading also need further study which is underway.
机译:我们以抽象状态机的形式介绍了类似Java的顺序程序的形式化模型(高级操作机)。为此目的,已经详细阐述了一种面向对象编程语言的对象类的代数模型。结果,已经定义了基本类组件(字段,构造函数和方法)的指称语义,供以后用于解释表达式和语句的使用。这是建议方法的重要组成部分。我们的机器从一种状态过渡到另一种状态是该方法的操作部分。形式化运算机器的使用使获得高层次的抽象成为可能,这是无法通过纯运算方法获得的,而映射的简单性是无法通过基于纯粹通用方法基于某些通用数学方法获得的。结构作为符号。我们机器中的每个对象都具有一个状态和一个唯一标识。对象标识由作为特殊引用类别的元素的引用表示。状态由许多实例变量表示,它们的值可以更新。这些变量在模型中自然定义为未定义值null的一组引用上的函数。对象状态可以通过状态相关函数的方法进行观察或更新。更新方法的结果是更新集,它是定义明确的数学结构。因此,这种方法的语义由产生更新集的一组函数给出。状态是所有方法声明的隐式参数,是状态更新方法的隐式结果,例如在Java和其他面向对象的编程语言中。这也使我们可以使声明方法类似于类Java语言中的声明方法。我们已经证明,我们的模型支持类Java语言的所有重要方面,即继承,重载,覆盖和后期绑定。由于篇幅所限,本文未介绍该模型的几个有趣方面。首先,这涉及表达式,语句和异常,将在后续论文中进行讨论。本地类定义,多包程序,动态类加载也需要进一步研究。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号