首页 | 本学科首页   官方微博 | 高级检索  
相似文献
 共查询到18条相似文献,搜索用时 93 毫秒
1.
代数规范是支持软件规格说明和设计的一种有效的方法,代数规范的直接实现技术是该研究领域的一个主要分支,目前这方面的研究基本上局限于线性代数规范,本文介绍一个实现非线性代数规范的转换过程,从该过程可自然是导出针对不同程序设计语言的转换系统,我们已实现了一个基于Pascal语言的转换系统。  相似文献   

2.
MFS是一个基于重写技术的程序开发系统.它提供的程序设计语言MFSL是扩展的函数式语言与代数规约语言相结合的混合语言.在这种混合语言中引入了能够提高效率和满足用户特殊需求的优化规则定义机制.语言的类型系统以及在语言和系统中引入的证明和测试机制能够使人们在开发过程中较早地发现问题,提高所开发系统的正确性.在系统的实现中采用的必要平行最外归约策略、图归约、证据测试集等技术能够使所开发的系统具有很高的实现效率.应用这一程序开发系统,能够较快地开发出正确且效率较高的程序.  相似文献   

3.
程序变换的一种规范说明方法   总被引:1,自引:0,他引:1  
文中给出了一种对程序变换进行分类的方法,提出了适合于更广义程序变换描述的四元组表示,程序变换的一种规范说明方法和规范说明语言的元语言SMOPT。介绍了这一规范说明方法SMOPT在反编译系统OECLER的AB变换器的设计与实现中的应用。  相似文献   

4.
冯速 《计算机科学》2005,32(2):150-152
本文考虑如何设计高效率(即重写步数较少的)重写型程序。文中以计算Fibonacci数列的程序为例.比较具有相同功能的重写型程序,展示编写高效率重写型程序的可能性。介绍利用动态项重写计算编写高效率重写型程序的直观、简洁的方法。其中.动态项重写计算是项重写系统的元计算模型,其计算同样基于项重写。  相似文献   

5.
XQuery语言的高性能实现需要利用XML查询代数提供的查询优化方法,也需要采取高效的树模式整体匹配算法。为了将这两种XML查询处理技术有效地结合在XQuery语言处理系统中,提出了一种通用系统框架来支持XQuery语言的高性能实现。在这个框架内,提供开放式XML数据源连接,并且通过作为中间语言的一种函数式查询计划描述语言FXQL来支持各种查询代数算子和树查询模式的表示,既允许采用各种XML查询代数,又允许采用各种树模式查询算法;进而,通过这种中间层的程序变换可以实现基于各种查询代数的查询重写,并从查询计划中分离出独立的树模式查询计算,使两种查询处理技术适当地统一在同一系统框架中,有效地支持了多种环境下XQuery语言的实现。  相似文献   

6.
基于重写技术的程序开发与验证   总被引:2,自引:0,他引:2  
孙永强  陆朝俊  邵志清 《软件学报》2000,11(8):1066-1070
完整地介绍了一个基于重写技术的程序开发和验证系统,重点展示验证子系统的理论、方法 和技术.验证子系统使得系统能自动证明程序和规范中的优化规则及测试等式,从而进一步保 证程序开发过程的正确性.验证子系统所采用的主要技术是以成批证明方法和证据测试集为 特色的重写归纳方法.  相似文献   

7.
陈意云  郭青 《计算机学报》1990,13(8):631-636
程序设计语言的形式规格说明是程序设计语言标准化、编译器自动生成和程序正确性证明的基础。良好的形式规格说明对语言的设计者、实现者和使用者都是有益的。 1.程序设计语言的代数规格说明方法 代数规格说明方法起源于ADJ小组,他们把语言的语法作为初始代数T,语义论域则是同样基调(signature)上的代数A,使得语言的语义由唯一同态f:T→A自动给  相似文献   

8.
JMX是一种资源管理的实现规范,它基于Java语言,并随着Java应用系统的增多将会有广泛的应用。文章介绍了JMX的体系结构及特点,并以Sun公司的实现为基础,分析了一个具体的程序实例。  相似文献   

9.
在面向对象程序设计语言的应用中,Java中的方法重写与方法重载在应用中会存在很多问题,这些概念很容易混淆,本文就这些概念给出了一些详细的论述,在理论和应用中来介绍方法重写与方法重栽的区别.  相似文献   

10.
Web应用服务器中Web Service引擎的设计与实现   总被引:2,自引:2,他引:2  
Web Service为程序之间的交互提供了基础,实现了独立于程序设计语言的一致化编程模型,并以通用的方法进行应用程序集成。分析了Web应用服务器实现Web Service的关键需求,阐述了在应用服务器中基于SOAP的Web Service引擎的设计与实现,介绍了实现Web Service引擎的若干关键技术和解决办法。Web Service引擎已在自主研发的OnceAS应用服务器中实现。  相似文献   

11.
In this paper the theoretical basis is presented and the implementation of a term rewriting system based on algebraic specifications is described. The input to this system is represented by an algebraic specification language, which forms not only the set of axioms but also the sorts, variables, operators and terms of a specific simulated theory or application. Rewriting and matching mechanisms provide the formal methodology for evaluating terms and proving assertions in an algebraic theory. Specifications are evaluated by interpreting terms by means of rewrite rules. The rules are described by the axioms of the specifications where the finite termination and congruence properties are assumed. A term rewriting system to recognize handwritten Hindu numerals is introduced as a case study. Besides rewriting, a robust algorithm is proposed to segment the numeral's image into strokes based on feature points and to identify cavity features. A syntactic representation (term) of the input image is matched and rewritten against a set of rules. Experimental results proved that the proposed system is tolerant to recognize a variety of numeral shapes with 96% successful recognition rate.  相似文献   

12.
An algebraic specification of a new rewriting machine for fast rewriting of terms is considered. Theorems on the correctness of this specification are proved. A method for optimization of a strategy of iterative rewriting is proposed.  相似文献   

13.
This paper presents a shallow and efficient embedding of the security protocol specification language MSR into an extension of rewriting logic with dependent types. The latter is an instance of the open calculus of constructions which integrates key concepts from equational logic, rewriting logic, and type theory. MSR is based on a form of first-order multiset rewriting extended with existential name generation and a flexible type infrastructure centered on dependent types with subsorting. The encoding presented in this paper has served as the basis for the implementation of an MSR specification and analysis environment using the first-order rewriting engine Maude.  相似文献   

14.
现有的服务组合描述途径不能有效地验证和测试组合正确性,针对这一问题,提出了一个代数规约方法,引入规约包机制扩展面向服务代数规约语言SOFIA以支持该方法。用代数规约单元描述服务系统中的各种实体,其中基调部分定义实体的语法和结构,公理部分定义其功能和行为特性。与一个服务相关的规约单元封装在一个包中或拆分在几个相互引用的包中,每个包形成一个命名空间。当多个服务组合在一起时,以这些服务的代数规约包为基础,一方面抽象地定义组合服务的交互过程和语义,形成描述服务组合实现方式的实现规约包;另一方面抽象地定义组合服务对外接口及其功能语义,形成描述组合服务需求的抽象规约包。在实现规约和抽象规约的双元结构基础上,进一步定义了实现规约和抽象规约之间必须满足的“实现”关系,证明了满足实现关系可以保证实现的正确性,从而为服务组合的可验证性和可测试性奠定了理论基础。最后结合实例分析阐述了用代数规约描述服务组合的抽象性、可表达性和可验证性。  相似文献   

15.
We propose checking the execution of an abstract data type's imperative implementation against its algebraic specification. An explicit mapping from implementation states to abstract values is added to the imperative code. The form of specification allows mechanical checking of desirable properties such as consistency and completeness, particularly when operations are added incrementally to the data type. During unit testing, the specification serves as a test oracle. Any variance between computed and specified values is automatically detected. When the module is made part of some application, the checking can he removed, or may remain in place for further validating the implementation. The specification, executed by rewriting, can be thought of as itself an implementation with maximum design diversity, and the validation as a form of multiversion-programming comparison  相似文献   

16.
Stratego is a domain-specific language for the specification of program transformation systems. The design of Stratego is based on the paradigm of rewriting strategies: user-definable programs in a little language of strategy operators determine where and in what order transformation rules are (automatically) applied to a program. The separation of rules and strategies supports modularity of specifications. Stratego also provides generic features for specification of program traversals. In this paper we present a case study of Stratego as applied to a non-trivial problem in program transformation. We demonstrate the use of Stratego in eliminating intermediate data structures from (also known as deforesting) functional programs via the warm fusion algorithm of Launchbury and Sheard. This algorithm has been specified in Stratego and embedded in a fully automatic transformation system for kernel Haskell. The entire system consists of about 2600 lines of specification code, which breaks down into 1850 lines for a general framework for Haskell transformation and 750 lines devoted to a highly modular, easily extensible specification of the warm fusion transformer itself. Its successful design and construction provides further evidence that programs generated from Stratego specifications are suitable for integration into real systems, and that rewriting strategies are a good paradigm for the implementation of such systems. This revised version was published online in June 2006 with corrections to the Cover Date.  相似文献   

17.
为了解决安全协议验证中攻击者模等式理论推理的可操作性问题,提出并设计了一种基于模重写系统的攻击者推理方法。该方法建立在一个反映两种密码原语代数特性的联合理论实例之上,由一组定向的重写规则和非定向的等式构成,前者进一步转化为项重写系统TRS(Term Rewriting System),而后者则转化为有限等价类理论,通过定义项间的模重写关系,使二者构成一个可以反映攻击者针对联合理论代数项操作能力的模重写系统。实例分析表明,该模型为攻击者模等式推理规则赋予了明确的操作语义,可以使攻击者达到对安全协议代数项规约、推理的目的。  相似文献   

18.
In this paper, we propose the notion of reducibility of symbols in term rewriting systems (TRSs). For a given algebraic specification, operation symbols can be classified on the basis of their denotations: the operation symbols for functions and those for constructors. In a model, each term constructed by using only constructors should denote an element, and functions are defined on sets formed by these elements. A term rewriting system provides operational semantics to an algebraic specification. Given a TRS, a term is called reducible if some rewrite rule can be applied to it. An irreducible term can be regarded as an answer in a sense. In this paper, we define the reducibility of operation symbols as follows: an operation symbol is reducible if any term containing the operation symbol is reducible. Non-trivial properties of context-sensitive rewriting, which is a simple restriction of rewriting, can be obtained by restricting the terms on the basis of variable occurrences, its sort, etc. We confirm the usefulness of the reducibility of operation symbols by applying them to behavioral specifications for proving the behavioral coherence property.  相似文献   

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号