直觉模糊集和区间值模糊集的截集、分解定理和表现定理

该文给出了直觉模糊集和区间值模糊集的截集定义,建立了直觉模糊集和区间值模糊集的分解定理和表现定理.首先,将直觉模糊集的截集视为三值模糊集,给出了直觉模糊集的四类截集定义,指出这些截集是模糊集截集概念的推广且与模糊集的截集有完全一样的性质.其次,利用本文给出的截集概念,建立了直觉模糊集的分解定理和表现定理.指出直觉模糊集的每种截集都对应两种分解定理和表现定理,从而建立了直觉模糊集的八种分解定理和八种表现定理.最后,利用直觉模糊集的截集理论,给出了区间值模糊集的截集定义,并建立了区间值模糊集的八种分解定理和表现定理.这些工作为研究直觉模糊集和区间值模糊集建立了理论基础.     

定理证明辅助工具Isabelle剖析与应用

Isabelle是一个通用的定理证明器,应用领域广泛.介绍Isabelle逻辑系统的功能和构成,分析了Isabelle的规格说明语言、验证系统的特点,并给出了用Isabelle逻辑系统来构造Z规格说明的定理证明的方法.     

DEDS双子模型的等价变换及其应用

提出了ＤＥＤＳ双子模型的等价变换与等价系统,给出了其定义,研究了其主要特性和计算方法,探讨了其在ＤＥＤＳ双子模型的简化、规范化及性能分析方面的应用,文中还给出了等价变换在建模、传函矩阵计算和有关定理证明方面应用的实例。     

Vague集的模糊熵*

首先,在给出了反例证实现有方法在某些情况得出的结果与实际结论不一致情况下,提出了一个真正考虑了两种因素的改进的vague集模糊熵公理化定义;然后给出一种vague集模糊熵的新计算公式;最后通过定理证明和实例分析,指出它确实同时考虑到vague集的未知性和不确定性,从而证明所给出vague集模糊熵的定义是更加合理的.     

从概念程序表示到C++过程蓝图的映射

文章给出了与程序实现语言无关的概念层抽象逻辑结构图程序表示到C＋＋过程蓝图的平滑过渡方法和映射规则,给出了概念层和逻辑层抽象逻辑结构图的有效性定义、导出C＋＋逻辑层抽象逻辑结构图的有效性定理及其证明。     

交互式进化计算的适应值噪声及收敛鲁棒性

噪声是影响进化计算(evolutionary computation,简称EC)算法性能的一个重要因素.对于传统EC中的噪声,已有许多研究成果,但交互式进化计算(interactive evolutionary computation,简称IEC)的噪声研究成果却较少.首先回顾了传统EC中噪声的定义、来源、类型及各种处理噪声的方法;其次,从IEC的理性用户观点出发,研究了IEC的适应值噪声及收敛鲁棒性.其中,空间的映射关系、个体间的占优关系以及IEC的收敛等是研究收敛鲁棒性的两个定理(强条件定理和弱条件定理)的基础.这两个定理表明,理性用户条件下的噪声不会影响算法全局收敛性.在这两个定理的基础上进一步得出了如下结论:有效的适应度尺度变换是弱条件定理的一部分,IEC中"真"适应值是用户偏好等.并以不满足弱条件定理,即破坏算法收敛性为依据,给出了IEC中适应值噪声的狭义定义.实验进一步验证了这两个定理.上述结论为进一步研究IEC作了必要的铺垫.     

支持契约式设计的Java静态验证器的研究

基于对Java编译器的扩展和静态验证技术提出了VeriJava项目,与相关工作相比,它的优点在于从语言层面扩展了Java,并且全面支持动态和静态的契约检查.首先介绍了VeriJava项目的整体架构,及其对Java进行的语言层面的扩展,进而重点讨论了方案的核心部分基于定理证明器的静态验证器的理论和设计,并给出了相关示例.     

连续傅里叶变换基础理论的高阶逻辑形式化

连续傅里叶变换(CFT)在数学和工程技术领域都有着广泛应用.利用高阶逻辑定理证明器HOL4,实现了对连续傅里叶变换定义及其常用运算性质的形式化,包括线性、频移、反转性、积分、时域一阶微分及高阶微分运算性质,为采用形式化方法分析相关系统奠定了基础.最后利用定理证明的方法对电阻电感电容(RLC)串联谐振电路的频率响应特性进行了验证,说明了CFT形式化的初步应用.     

GJK算法的一种特殊情形的形式化验证和应用

计算几何算法经常用于机器人避碰运动规划等安全攸关领域,对这些算法进行正确性证明非常重要.用形式化方法对算法进行验证是一种十分有效的手段,尤其是定理证明的方法用严格的数学公理和定理推理证明逻辑模型的性质,对所验证的性质而言是完备的.基于GJK算法设计了计算空间两条线段间距离的算法,用定理证明器HOL4对其相关的定义和定理进行形式化定义和证明,进而基于霍尔逻辑完成形式化表示和证明,对该算法的正确性实现了形式化验证.最后,给出了这一经过验证的算法在双臂机器人无碰撞运动规划中的应用.     

抽象逻辑结构图到VFP过程蓝图的过渡与映射

给出独立于程序实现语言的抽象逻辑结构图到VFP过程蓝图的平滑过渡方法及概念结点到逻辑结点的映射规则;给出了抽象逻辑结构图程序表示的有效性定义、导出VFP抽象逻辑结构图的有效性定理及其证明。     

基于SHML的CPS行为建模及仿真

信息物理融合系统（cyber-physical systems，简称CPS）是深度融合了计算进程和物理进程的统一体，是集计算、通信与控制于一体的下一代智能系统，具有广阔的应用前景.CPS的行为具有混成性、随机性等特征，建模及仿真CPS的动态行为对于开发高质量的CPS系统至关重要.但是目前缺乏面向CPS的领域建模方法及建模CPS的领域建模语言，也迫切需要支持仿真CPS领域模型的仿真工具.针对以上问题，提出一种面向CPS领域的随机混成建模语言（stochastic hybrid modeling language，简称SHML）以支持建模CPS系统的行为.首先，根据CPS的领域特征定义了SHML的元模型作为其抽象语法，并定义了SHML的具体语法和操作语义；其次，基于GEMOC框架实现了SHML的可视化建模工具.此外，集成GEMOC的序列化执行引擎和Scilab的连续行为仿真引擎，实现仿真CPS的混成行为.提出了一种面向CPS领域的建模及仿真方法，设计并实现了一个集成的面向CPS行为的建模与仿真平台，为CPS的建模及仿真提供了一种有效的方法及工具支撑.     

Towards Verification of C Programs. C-Light Language and Its Formal Semantics

The C-light language is described, which is a representative subset of C. C-light permits deterministic expressions, limited use of switch and goto statements, and, instead of library functions for work with dynamic memory, includes C++ statements new and delete. A survey of structured operational semantics of the C-light language in Plotkin's style is given.     

CPS transformation of beta-redexes

The extra compaction of the most compacting CPS transformation in existence, which is due to Sabry and Felleisen, is generally attributed to (1) making continuations occur first in CPS terms and (2) classifying more redexes as administrative. We show that this extra compaction is actually independent of the relative positions of values and continuations and furthermore that it is solely due to a context-sensitive transformation of beta-redexes. We stage the more compact CPS transformation into a first-order uncurrying phase and a context-insensitive CPS transformation. We also define a context-insensitive CPS transformation that provides the extra compaction. This CPS transformation operates in one pass and is dependently typed.     

On the computational power of BlenX

We present some decidability and undecidability results for subsets of the BlenX Language, a process-calculi-based programming language developed for modelling biological processes. We show that for a core subset of the language (which considers only communication primitives) termination is decidable. Moreover, we prove that by adding either global priorities or events to this core language, we obtain Turing equivalent languages. The proof is through encodings of Random Access Machines (RAMs), a well-known Turing equivalent formalism, into our subsets of BlenX. All the encodings are shown to be correct.     

Call-by-need and continuation-passing style

This paper examines the transformation of call-by-need terms into continuation-passing style (CPS). It begins by presenting a simple transformation of call-by-need terms into program graphs and a reducer for such graphs. From this, an informal derivation is carried out, resulting in a translation from terms into self-reducing program graphs, where the graphs are represented as CPS terms involving storage operations. Though informal, the derivation proceeds in simple steps, and the resulting translation is taken to be our canonical CPS transformation for call-by-need terms.In order to define the CPS transformation more formally, two alternative presentations are given. The first takes the form of a continuation semantics for the call-by-need language. The second presentation follows Danvy and Hatcliff's two-stage decomposition of the call-by-name CPS transformation, resulting in a similar two-stage CPS transformation for call-by-need.Finally, a number of practical matters are considered, including an improvement to eliminate the so-called administrative redexes, as well as to avoid unnecessary memoization and take advantage of strictness information. These improvements make it feasible to consider potential applications in compilers for call-by-need programming languages.Supported in part by the National Science Foundation under PYI grant #CCR-9057567, with matching funds from Bell Northern Research.Supported by an AT&T Ph.D. scholarship.     

PCF的信息系统模型

带类型的λ－演算是一个逻辑系统，它可以作为程序语言的基础．Ｐｌｏｔｋｉｎ所引进的ＰＣＦ就是这样一类程序语言．Ｐｌｏｔｋｉｎ构造了ＰＣＦ的一个模型，然后讨论与这个模型相关的指称语义和操作语义之间的配合问题──简单配合和完全配合．本文利用Ｓｃｏｔｔ引进的信息系统概念构造ＰＣＦ的另一种模型，并证明与这个模型对应的指称语义与操作语义是完全配合的．     

Reasoning about programs in continuation-passing style

Plotkin's _v -calculus for call-by-value programs is weaker than the -calculus for the same programs in continuation-passing style (CPS). To identify the call-by-value axioms that correspond to on CPS terms, we define a new CPS transformation and an inverse mapping, both of which are interesting in their own right. Using the new CPS transformation, we determine the precise language of CPS terms closed under -transformations, as well as the call-by-value axioms that correspond to the so-called administrative -reductions on CPS terms. Using the inverse mapping, we map the remaining and equalities on CPS terms to axioms on call-by-value terms. On the pure (constant free) set of -terms, the resulting set of axioms is equivalent to Moggi's computational -calculus. If the call-by-value language includes the control operatorsabort andcall-with-current-continuation, the axioms are equivalent to an extension of Felleisenet al.'s _v -C-calculus and to the equational subtheory of Talcott's logic IOCC.This article is a revised and extended version of the conference paper with the same title [42]. The technical report of the same title contains additional material.The authors were supported in part by NSF grant CCR 89-17022 and by Texas ATP grant 91-003604014.     

Toward a theory of encoded data structures and data translation

Several models of data base systems have distinguished levels of abstraction ranging from the high-level entity set model down to the low-level physical device level. This paper presents a model for describing data encodings, an intermediate level which focuses on the relationship among data items as demonstrated by contiguity or by pointer connections. Multiple data encodings for a file are shown and transformation functions that describe the translation between data encodings are discussed.     

A static simulation of dynamic delimited control

We present a continuation-passing-style (CPS) transformation for some dynamic delimited-control operators, including Felleisen’s and , that extends a standard call-by-value CPS transformation. Based on this new transformation, we show how Danvy and Filinski’s static delimited-control operators and simulate dynamic operators, allaying in passing some skepticism in the literature about the existence of such a simulation. The new CPS transformation and simulation use recursive delimited continuations to avoid undelimited control and the overhead it incurs in implementation and reasoning.     

AADL+: a simulation-based methodology for cyber-physical systems

AADL (architecture analysis and design language) concentrates on the modeling and analysis of application system architectures. It is quite popular for its simple syntax, powerful functionality and extensibility and has been widely applied in embedded systems for its advantage. However, it is not enough for AADL to model cyber-physical systems (CPS) mainly because it cannot be used to model the continuous dynamic behaviors. This paper proposes an approach to construct a new sublanguage of AADL called AADL+, to facilitate the modeling of not only the discrete and continuous behavior of CPS, but also interaction between cyber components and physical components. The syntax and semantics of the sublanguage are provided to describe the behaviors of the systems. What’s more, we develop a plug-in to OSATE (open-source AADL tool environment) for the modeling of CPS. And the plug-in supports syntax checking and simulation of the system model through linking with modelica. Finally, the AADL+ annex is successfully applied to model a lunar rover control system.