排序方式: 共有15条查询结果,搜索用时 0 毫秒
1.
本文从Ideal的基本概念出发,研究了Ideal作为类型的语义模型所具有的性质.在类型的Ideal模型下,讨论了Garment中参数化多态类型和约束多态类型的语义.并在此基础上,证明了Garment中类型规则的语义可靠性. 相似文献
2.
知识结构的三叉树表示和逻辑推理的实现 总被引:1,自引:0,他引:1
本文根据逻辑程序的要求,设计了知识结构的三叉树表示法,并给出了基于这种表示的推理过程的框架。 相似文献
3.
Hardware and software co-design is a design technique which delivers computer systems comprising hardware and software components.A critical phase of the co-design process is to decompose a program into hardware and software .This paper proposes an algebraic partitioning algorithm whose correctness is verified in program algebra.The authors inroduce a program analysis phase before program partitioning and deveop a collection of syntax-based splitting rules.The former provides the information for moving operations from software to hardware and reducing the interaction between compoents,and th latter supports a compositional approach to program partitioning. 相似文献
4.
基于描述逻辑的特征模型 总被引:1,自引:0,他引:1
由于特征模型缺乏严格语义基础,难以对模型进行一致性推理,无法保证模型的一致性,进而影响最终软件产品的质量。本文讨论了如何使用描述逻辑对特征模型进行形式化,给出了将特征模型转化为描述逻辑ALCQI知识库的算法,通过验证转化后的知识库的一致性得到所对应特征模型的一致性。并利用描述逻辑的推理机RACER对转换得到的知识库进行推理,自动完成特征模型的一致性检查,为特征模型的一致性检验提供一种方法,实践证明这种方法具有可靠性和高效性。 相似文献
5.
本文对C语言语法形式化问题作了初步探讨,给出了一个较为完整的语法图,并对表达式、说明符和函数的定义作了重点分析,对有关问题提出了意见。 相似文献
6.
一种带约束的多态类型系统 总被引:1,自引:0,他引:1
本文讨论了一种带约束的多态类型系统,引入了约束类型,约束与全称量化的结合使得参数化多态函数的应用更安全,同时也为重工的表示和实现提供了一个新的途径,提高了类型表示的抽象度。本文讨论的类型系统具有两个不同层次的类型结构,约束的引入与肖去是不同层次上的操作,最后,本文人出了类型检查算法Wr,并证明了此算法中约束的可满足性是可判定的。 相似文献
7.
程序变换在程序语言中的一种表示——兼论变换型语言 总被引:3,自引:1,他引:2
本文首先引入了“变换型语言”的概念,给出了代表这种语言特征的机制:“变换模块”和“变换控制命令”的具体定义;举例说明了如何使用“变换模块”描述一个抽象数据类型的部分实现,并通过“变换控制命令”来完成程序中抽象变量及有关操作的变换过程;最后,讨论了变换型语言表示的抽象性,一般性和控制的灵活性,以及变换型程序的正确性等问题。 相似文献
8.
基于交易中件的客户/服务器系统是一种典型的分布式事务处理系统,深入研究这种系统的一般模型,有助于深刻理解这种软件的特征与性质,有助于提高系统的正确性和可靠性。文章根据该系统的同象模型对它的主要“构件”和“操作”的功能进行抽象的分析;并用规范语言Z对这种体系结构的模型进行了系统的形式化描述。 相似文献
9.
程序变换过程的分析与设计 总被引:2,自引:0,他引:2
程序变换过程的分析与设计张乃孝(北京大学计算机科学与技术系北京100871)ANALYSISANDDESIGNOFTHEPROGRAMTRANSFORMATIONPROCESS¥ZhangNaixiao(DepartmentofcomputerSci... 相似文献
10.