一类递归函数的多态类型

以上下文无关语言上的递归函数为基础的语言LFC(1anguage for context free recursive function)是一种形式规约语言,适于处理短语结构.LFC也是函数式语言,具有函数式语言的许多特点.LFC已经在形式规约获取系统SAQ(specification acquisition system)中实现,为其最初设计的类型系统不支持多态类型.引入类型变量和相应的类型检查方法,就可以将其类型系统扩充为多态类型系统.对多态类型系统实现中的一些问题也进行了讨论.在实现多态之后,LFC     

一种特殊的上下文无关文法及其语法分析

SAQ系统是一个进行软件规约获取、检验和复用的实验系统，其中以上下文无关文法表示的概念是规约的一部分.SAQ要求将概念的词法和句法定义结合在一个上下文无关文法中.如果用常规的上下文无关文法描述诸如程序设计语言和自然语言等一些复杂概念的语法，则需要把诸如空格和回车等没有实质意义的分隔符包含到语法中去(这种描述方法称为朴素表示法),使得语法描述很累赘.为此，作者设计了一种特殊的上下文无关文法,它把通常上下文无关文法定义中的非终极符集合和终极符集合进行细化.用这种文法可以相对简洁地描述程序语言和自然语言等复杂概     

一个支持规约获取的形式规约语言

该文介绍了形式规约语言LFC设计的一些主要方面，并通过例子说明了LFC的一些特色。形式规约语言LFC是为支持软件形式规约的获取工作而开发的。该语言以一种新的递归函数，即定义在上下文无关语言上的递归函数为基础，以上下文无关语言为数据类型，在语言级支持规约获取。LFC语言已被用作形式规约获取系统SAQ的一部分。使用表明，LFC是一个能力强、易使用的语言，适合软件形式规约获取之用，并且适合其它一些用途。     

模糊安全性和活性

形式规约使用形式语言构建所开发的软硬件系统的规约,刻画系统的模型和性质.其中,性质规约中的分支时间规约对于系统验证有着非常重要的作用.在经典情形下,系统性质规约是基于二值逻辑的,不能描述不一致或不确定的信息.因此,将其推广到模糊逻辑背景下,有助于对模糊系统进行形式验证.文中首先给出了性质规约中分支时间属性在模糊背景下的...     

基于ICE分布式用电信息采集系统的规约服务

Ice中间件集成了分布式运算环境,利用Ice提供的load balancing功能,把M个规约处理请求合理的分配到N个规约服务上,并在不影响用电信息采集系统运行的情况下实现规约服务实例及规约处理应用的动态增减。基于Ice的分布式规约服务,具备负载均衡能力、很好的可伸缩性及灾难冗余能力。     

智能电量采集终端便携式校验仪设计与研究

设计开发一套智能电量采集终端测试校验系统,既能满足电量采集终端装置(简称TMR采集终端)的到货验收测试需要,又能满足对TMR采集终端的现场调试要求.校验系统实现了主站与终端通讯测试、规约测试,终端上行通讯检测,上行规约数据对比,下行规约检测.分析判断TMR采集终端的网络、上、下行规约的异常.系统的设计与研发即减少了TM...     

循环式远动规约在高速公路交通监控上的移植

在解析了循环式远动规约(即CDT规约)的基础上,分别探讨了变电站系统与高速公路监控系统的系统体系结构与数据信息,提出了电力远动通信协议在高速公路监控系统上的移植,并拟定了高速公路监控系统通信协议的报文格式.     

基于IEC60870-5-104远动规约的通信技术在电厂SIS系统中的应用

介绍了国际电工委员会(IEC)制定的IEC60870-5-104远动规约.详细阐述了该规约的网络参考模型和通信实施过程.根据工程实践,介绍了基于IEC104规约的网络通信技术在远动终端和SIS系统之间的应用.最后展望了该通信技术在火电厂SIS系统中的广泛应用前景.     

FC和iSCSI协议的分析比较

FC和iSCSI是目前存储区域网络SAN(StorageAreaNetwork)的两个主流协议。该文介绍FC(FibreChannel:光纤通道)和iSCSI(InternetSCSI)协议的协议结构以及流量控制和发现机制,在零复制和流量控制等方面对FC和iSCSI的协议功能进行了分析比较。     

一种典型FC和CAN偶发通信故障分析与验证

从机载系统传感器图像到综合处理机的数据传输通信过程中,会偶发短消息指令,经机载光线通道(FC)转控制器局域网(CAN)后无响应,故障复现难度大。为了有效解决这一问题,根据产品工作原理和系统组成,对仿真验证测试系统和整机联试系统的测试覆盖性、特征参数及系统通信过程进行分析和排查,并通过加载测试工具对通信过程进行测量和验证,确定系统在初始化过程中,因上位机FC仿真卡没有严格按照光线通道航空环境匿名用户消息协议(FC-AE-ASM)与产品建立可靠的交联通信而导致短消息无响应的偶发故障。实践表明,改进升级后的FC仿真卡在工程应用中有效解决了此类偶发的通信故障,提高了整机联试系统通信的可靠性。     

The convergence of functions to fixedpoints of recursive definitions

The classical method for constructing the least fixedpoint of a recursive definition is to generate a sequence of functions whose initial element is the totally undefined function and which converges to the desired least fixedpoint. This method, due to Kleene, cannot be generalized to allow the construction of other fixedpoints. In this paper we present an alternate definition of convergence and a new fixedpoint access method of generating sequences of functions for a given recursive definition. The initial function of the sequence can be an arbitrary function, and the sequence will always converge to a fixedpoint that is “close” to the initial function. This defines a monotonic mapping from the set of partial functions onto the set of all fixedpoints of the given recursive definition.     

Recursive functions of context free languages (I)--The definitions of CFPRF and CFRF

It is intended to establish the recursive function theory on context free languages (CFLs). In this paper, the function class CFRF and its proper subclass CFPRF were defined on CFLs; it is quite straightforward to use them for describing non_numerical algorithms. In fact, they are respectively the partial recursive functions and primitive recursive functions of context free languages. The structure induction method for proving CFPRF function properties was presented. A method for CFL sentence enumeration was given, the minimization operator was defined. Based on CFL sentence enumeration, the minimization operator evaluation method was given. Finally, the design and implementation principles of executable specification languages with the CFRF as theoretical basis were discussed.     

Recursive functions of context free languages (Ⅰ)——The definitions of CFPRF and CFRF

It is intended to establish the recursive function theory on context free languages (CFLs). In this paper, the function class CFRF and its proper subclass CFPRF were defined on CFLs; it is quite straightforward to use them for describing non-numerical algorithms. In fact, they are respectively the partial recursive functions and primitive recursive functions of context free languages. The structure induction method for proving CFPRF function properties was presented. A method for CFL sentence enumeration was given, the minimization operator was defined. Based on CFL sentence enumeration, the minimization operator evaluation method was given. Finally, the design and implementation principles of executable specification languages with the CFRF as theoretical basis were discussed.     

Recursive functions of context free languages (I)

It is intended to establish the recursive function theory on context free languages (CFLs). In this paper, the function class CFRF and its proper subclass CFPRF were defined on CFLs; it is quite straightforward to use them for describing non-numerical algorithms. In fact, they are respectively the partial recursive functions and primitive recursive functions of context free languages. The structure induction method for proving CFPRF function properties was presented. A method for CFL sentence enumeration was given, the minimization operator was defined. Based on CFL sentence enumeration, the minimization operator evaluation method was given. Finally, the design and implementation principles of executable specification languages with the CFRF as theoretical basis were discussed. This paper is based on the Technical Report ISCAS-LCS-2k-03 (SAQ Report No. 30): Recursive Functions Defined on Context Free Languages (I), August 2000, with minor revisions.     

Parallelization of divide-and-conquer in the Bird-Meertens formalism

An SPMD parallel implementation schema for divide-and-conquer specifications is proposed and derived by formal refinement (transformation) of the specification schema. The specification is in the form of a mutually recursive functional definition. In a first phase, a parallel functional program schema is constructed which consists of a communication tree and a functional program that is shared by all nodes of the tree. The fact that this phase proceeds by semantics-preserving transformations in the Bird-Meertens formalism of higher-order functions guarantees the correctness of the resulting functional implementation. A second phase yields an imperative distributed message-passing implementation of this schema. The derivation process is illustrated with an example: a two-dimensional numerical integration algorithm.Parts of this paper were presented at the International Parallel Processing Symposium, Mexico, 1994 [GoL94] and at the World Transputer Congress, Italy, 1994 [Gor94]     

Using Computer Algebra techniques for the specification,verification and synthesis of recursive programs

We describe an innovative method for proving total correctness of tail recursive programs having a specific structure, namely programs in which an auxiliary tail recursive function is driven by a main nonrecursive function, and only the specification of the main function is provided. The specification of the auxiliary function is obtained almost fully automatically by solving coupled linear recursive sequences with constant coefficients. The process is carried out by means of CA (Computer Algebra) and AC (Algorithmic Combinatorics) and is implemented in the Theorema system (using Mathematica). We demonstrate this method on an example involving polynomial expressions. Furthermore, we develop a method for synthesis of recursive programs for computing polynomial expressions of a fixed degree by means of “cheap” operations, e.g., additions, subtractions and multiplications. For a given polynomial expression, we define its recursive program in a schemewise manner. The correctness of the synthesized programs follows from the general correctness of the synthesis method, which is proven once for all, using the verification method presented in the first part of this paper.     

Recursive functions of context free languages (Ⅱ)——Validity of CFPRF and CFRF definitions

In this paper we proved that the function class CFRF and its proper subclass CFPRF are respectively the partial recursive functions and primitive recursive functions of context free languages (CFLs). Also we discussed the relation between them and recursive functions defined on other domains . It is indicated that the functions of natural numbers and/or symbol strings (words) are functions of CFLs. Several frequently used primitive recursive functions on words were given, including logical connectives, conditional expressions. Also the powerful operators (bounded maximization and minimization operators) for constructing primitive recursive functions were defined. Two important nontrivial algorithms, the characteristic function of arbitrary CFL and the parse function of CFL sentences were constructed. Based on them, the method for extending or restricting function domain was described.     

Facilitating formal specification acquisition by using recursive functions on context-free languages

Although formal specification techniques are very useful in software development, the acquisition of formal specifications is a difficult task. This paper presents the formal specification language LFC, which is designed to facilitate the acquisition and validation of formal specifications. LFC uses context-free languages for syntactic aspect and relies on a new kind of recursive functions, i.e. recursive functions on context-free languages, for semantic aspect of specifications. Construction and validation of LFC specifications are machine-aided. The basic ideas behind LFC, the main aspects of LFC, and the use of LFC and illustrative examples are described.