函数式逻辑语言的操作语义

函数式语言和逻辑语言在下列意义上是互补的,基于归约的函数式程序设计语言具有确定和懒惰求解等性质.但同时它又缺少诸如存在量化的变量以及部分数据结构等所希望的性质.相反,基于HORN子句逻辑和消解原理的逻辑程序设计语言允许存在量化的变量和部分数据结构但又缺少确定和懒惰求解的性质.从这个角度出发,把函数和逻辑程序设计语言结合成一种范型是很自然的,这种结合提供了一种比逻辑和函数语言表达能力更强的合一语言.提出了函数式逻辑语言的操作语义,同时表明这种操作语义在实践中是可见的.     

An Operational Semantics for Timed CSP

An operational semantics is defined for the language of timed CSP, in terms of two relations: an evolution relation, which describes when a process becomes another simply by allowing time to pass; and a timed transition relation, which describes when a process may become another by performing an action at a particular time. It is shown how the timed behaviours used as the basis for the denotational models of the language may be extracted from the operational semantics. Finally, the failures model for timed CSP is shown to be equivalent to may-testing and, thus, to trace congruence.     

UML活动图的操作语义

越来越多的系统采用UML(unified model language, 统一建模语言)作为建模语言来进行系统分析和设计. UML活动图是UML语言中描述系统动态行为的一种方法,它广泛地运用于业务建模.由于UML活动图缺乏精确的动态语义,所以不利于对其所描述的系统进行形式化的分析、验证和确认.为解决这一问题,根据UML1.5语义文档,给出UML活动图的形式化操作语义.首先给出UML活动图的形式化的语法,然后详细地定义了活动图的格局和变迁,最后基于LTS给出了活动图的演绎规则.主要工作是：引入状态包的概念,使得描述更加清楚、完善;通过LTS定义活动图的操作语义,并详细阐述演绎规则,从而获得活动图的全局状态转移图,使定义的操作语义很容易地应用到形式化验证中.该语义覆盖了UML活动图的绝大部分特征,为对UML活动图进行模型检验奠定了基础.     

An Unboxed Operational Semantics for ML Polymorphism

We present an unboxed operational semantics for an ML-style polymorphic language. Different from the conventional formalisms, the proposed semantics accounts for actual representations of run-time objects of various types, and supports a refined notion of polymorphism that allows polymorphic functions to be applied directly to values of various different representations. In particular, polymorphic functions can receive multi-word constants such as floating-point numbers without requiring them to be boxed (i.e., heap allocated.) This semantics will serve as an alternative basis for implementing polymorphic languages. The development of the semantics is based on the technique of the type-inference-based compilation for polymorphic record operations [20]. We first develop a lower-level calculus, called a polymorphic unboxed calculus, that accounts for direct manipulation of unboxed values in a polymorphic language. This unboxed calculus supports efficient value binding through integer representation of variables. Different from de Bruijn indexes, our integer representation of a variable corresponds to the actual offset to the value in a run-time environment consisting of objects of various sizes. Polymorphism is supported through an abstraction mechanism over argument sizes. We then develop an algorithm that translates ML into the polymorphic unboxed calculus by using type information obtained through type inference. At the time of polymorphic let binding, the necessary size abstractions are inserted so that a polymorphic function is translated into a function that is polymorphic not only in the type of the argument but also in its size. The ML type system is shown to be sound with respect to the operational semantics realized by the translation.     

UML Statechart图的操作语义

面向对象标准建模语言UML(unified modeling language)缺乏精确的动态语义.根据UML1.1语义文档,提出描述对象状态机的UML Statechart图的形式化操作语义.该语义覆盖了UML Statechart图的绝大部分特征,为UML Statechart图的代码产生、模拟和测试用例生成奠定了基础.根据上述语义,基于Rose98完成了UML Statechart图的测试用例生成和测试过程的模拟.     

An Operational Semantics for Shared Messaging Communication

Shared Messaging Communication (SMC) has been introduced in [Satya Kiran M.N.V., Jayram M.N., Pradeep Rao, and S.K. Nandy. A complexity effective communication model for behavioral modeling of signal processing applications. In Proceedings of 40th Design Automation Conference, 2003] as a model of communication which reduces communication costs (both in terms of communication latency and memory usage) by allowing tasks to communicate data through special shared memory regions. Sending a reference to an otherwise inaccessible memory regions rather than the data itself, the model combines the advantages of message passing and shared memories. Experimental results have shown that SMC in case of large data payloads clearly outperforms the classical message passing.In this paper we give a formal operational semantics to SMC exhibiting unambiguously the effect of executing an SMC command on local and shared memories. Based on this semantics we show that any program using message passing can be proved to be weakly bisimilar to one based on SMC and that with respect to communication costs the latter is amortised cheaper, [A. Kiehn and S. Arun-Kumar. Amortised bisimulations. In Proceedings of FORTE 2005, number 3731 in Lecture Notes in Computer Science, pages 320–334. Springer-Verlag, 2005].     

Paraconsistent Declarative Semantics for Extended Logic Programs

We introduce a fixpoint semantics for logic programs with two kinds of negation: an explicit negation and a negation-by-failure. The programs may also be prioritized, that is, their clauses may be arranged in a partial order that reflects preferences among the corresponding rules. This yields a robust framework for representing knowledge in logic programs with a considerable expressive power. The declarative semantics for such programs is particularly suitable for reasoning with uncertainty, in the sense that it pinpoints the incomplete and inconsistent parts of the data, and regards the remaining information as classically consistent. As such, this semantics allows to draw conclusions in a non-trivial way, even in cases that the logic programs under consideration are not consistent. Finally, we show that this formalism may be regarded as a simple and flexible process for belief revision.     

描述性语言与知识库系统

1．引言 在数据库领域,由于描述性语言SQL的成功使用,描述性更加受到重视[1,2,3,4]。描述性语言Data-log的提出,使得一些学者认为知识库语言应该是描述性的程序设计语言[4]。然而多年来的研究,不但没有开发出一个描述性的知识库程序设计语言,而且还阻碍了知识库的实用化[5]。本文研究了描述性与逻辑语言、知识库语言之间的关系,提出了三个观点：1)描述性语言是计算不完备的,因此不能作为独立的程序设计语言；2)逻辑语言是描述性语言的合适形式；3)追求语言的描述性是知识库系统实用化的障碍之一。     

一种命令式风格的面向对象语言语义框架

面向对象语言在软件工程实践中有着广泛的应用。为面向对象语言定义严格的语义有助于理解面向对象语言的本质特征,对验证软件、提高软件系统可靠性等也具有重要意义。给出了一种新的面向对象语言的语义框架,该框架基于命令式的风格,具有操作语义和类型规则;证明了该语义框架的类型安全定理。     

Operational Semantics for MSC'96

Recently, the ITU-standardised specification language Message Sequence Chart has been extended with constructs for more complete and structured specifications. The new version of the language is called MSC'96. Currently, research is performed on the extension of the formal semantics towards a semantics for MSC'96. In this article, we aim at explaining the basic ideas behind the formal semantics. We give formal definitions of parts of the language, but most features are explained by informal examples and drawings. It takes several steps in order to follow the path from an MSC drawing to its formal meaning. First, the drawing must be converted to a concrete textual representation. This conversion is already defined implicitly in Z.120. Next, this syntax is transformed into a formal expression over some process algebra signature. MSC constructs are replaced by appropriate process algebra operators. This transformation is compositional. The operational behaviour of the process algebraic expression can be studied, or the expression can be interpreted into some mathematical model and compared to the interpretation of some other MSC.     

An Eclipse-based Integrated Environment for Developing Executable Structural Operational Semantics Specifications

The Structural Operational Semantics Development Tooling (SOSDT) Eclipse Plugin integrates the Relational Meta-Language (RML) compiler and debugger with the Eclipse Integrated Development Environment Framework. SOSDT, together with the RML compiler and debugger, provides an environment for developing and maintaining executable Structural Operational Semantics specifications, including the Natural Semantics big step variant of SOS specifications. The RML language is successfully used at our department for writing large specifications for a range of languages like Java, Modelica, Pascal, MiniML etc. The SOSDT environment includes support for browsing, code completion through menus or popups, code checking, automatic indentation, and debugging of specifications.     

An Observation Approach to the Semantics of Agent Communication Languages

We show how a formal framework for the observation issue in computer systems can be used for the specification of an agent behavior, abstracting away from agent inner details while focusing on its interactive behavior. This model can also be used as a specification of agent communication languages (ACLs), providing the proper abstraction level to represent the conditions causing an agent to send a message, as well as its effect on the receiving agent. In particular, this approach generalizes upon existing ACL semantics, such as FIPA ACL, that relate agent communicative acts to the agent mental state. Since the observation framework induces a more abstract architecture than other known approaches, our semantics are likely to be applicable to a wider set of agent architectures, thus better supporting standardization aims. Some application examples are shown, describing how various aspects of ACL semantics can be specified within our framework.     

命令式语言的化学语义

化学计算模型是基于化学反应和计算之间比喻的并行计算模型,其内在的并行性及不确定性可以有效的消除与计算逻辑本身无关的人为顺序性,但是难于描述特定的控制机制.高阶化学编程语言是对传统化学计算模型的扩展和泛化,可以描述传统的控制机制和定义新的控制机制.通过从简单命令式语言到高阶化学语言的转换,给出了命令式语言的一种化学语义描述,为结合命令式编程和化学编程提供了一种可能.     

面向对象语言的化学语义

提出了一种基于程序分析的代码查询技术,它能有效地应用于代码审查、程序自动插桩等常用的软件工程的研究场景。它通过代码静态分析获得程序元素信息,并将其保存为中间结构,作为代码查询过程的目标集合;查询过程以程序元素为目标,查询语言以谓词逻辑表达式的形式描述查询条件。基于此技术,实现了一个面向C/C++语言的代码查询工具。     

Formal Foundations of Operational Semantics

In this paper we report on the results of a sophisticated and substantial use of PVS to establish a recent result in operational semantics. The result we establish is a context lemma for operational equivalence for very wide class of programming languages, known as the CIU theorem. The proof uses the annotated holes technique to represent contexts and compute with them. Thus this paper demonstrates that that it is possible to use PVS as a tool in the development of modern operational techniques, and a productive tool at that. The process of formalizing the CIU theorem revealed several gaps in published proof. The proof of the CIU theorem in PVS took approximately six months to develop. The actual machine checked proof involves the proving of around one thousand facts, and takes PVS slightly less than three hours of CPU time running on a Linux machine configured with 2 GBytes of main memory and four 550 MHz Xeon PIII processors.     

基于逻辑的软件演化操作语言及结构化操作语义

由于使用环境和新技术的不断变化,软件演化的控制变得日趋复杂.为了提高软件演化活动的可视化和形式化支持程度,结合谓词逻辑和软件演化,提出了一种软件演化操作语言SEOL(Software Evolution Operational Language)描述软件演化,给出了SEOL的语法和结构化操作语义描述,并指出了软件演化操作语义等价分析方法.结合软件代码演化和软件模型演化实例,说明了SEOL的应用.与已有的软件演化操作描述相比,SEOL在易用性、可重用性和形式化分析方面有明显的改善,为软件演化的管理、分析和实施奠定了基础.