首页 | 本学科首页   官方微博 | 高级检索  
文章检索
  按 检索   检索词:      
出版年份:   被引次数:   他引次数: 提示:输入*表示无穷大
  收费全文   24篇
  国内免费   1篇
  完全免费   7篇
  自动化技术   32篇
  2019年   1篇
  2012年   1篇
  2011年   1篇
  2010年   2篇
  2007年   1篇
  2006年   5篇
  2005年   2篇
  2004年   2篇
  2003年   2篇
  2002年   1篇
  2001年   1篇
  2000年   2篇
  1999年   1篇
  1998年   1篇
  1997年   1篇
  1995年   4篇
  1993年   1篇
  1992年   1篇
  1991年   1篇
  1990年   1篇
排序方式: 共有32条查询结果,搜索用时 31 毫秒
1.
形式化方法B及其程序规约机理   总被引:12,自引:1,他引:11  
肖美华  薛锦云 《计算机工程》2004,30(16):16-18,50
用形式化方法开发软件是提高软件可靠性和生产效率的革命性途径,是实现软件自动化的关键。文章针对B方法,介绍了其产生的历史背景,分析了其程序规约机理,并结合实例给出了B方法中抽象机的具体运用,对该方法的特点进行了评述。  相似文献
2.
Institution中自由合并理论的初始与终结语义*   总被引:5,自引:1,他引:4       下载免费PDF全文
刘富春 《软件学报》1999,10(2):197-200
在一般性的适用框架Institution中,建立了自由合并理论与各因子理论的初始(终结)语义之间的对应关系,给出了自由理论态射的粘合态射及其相关的初始(终结)语义,并证明了在一定条件下,遗忘函子Sign:ThlSign的反射余极限.  相似文献
3.
一种基于程序正确性证明理论的程序开发方法   总被引:3,自引:0,他引:3  
程序的形式推导方法是一种基于程序正确性证明理论的程序开发方法,它使得程序的开发和证明同时进行,程序开发完成的同时其正确性亦得以保 证,以两个问题的程序开发为例说明了程序的形式推导方法的使用。  相似文献
4.
Logical Object as a Basis of Knowledge Based Systems   总被引:2,自引:0,他引:2       下载免费PDF全文
This paper presents a framework called logical knowledge object (LKO),which is taken as a basis of the dependable development of knowledge based systems(KBSs).LKO combines logic programming and object-oriented programming paradigms,where objects are viewed as abstractions with states,constraints,behaviors and inheritance.The operational semantics defined in the style of natural semantics is simple and clear.A hybrid knowledge representation amalgamating rule,frame,semantic network and blackboard is available for both most structured and flat knowledge.The management of knowledge bases has been formally specified.Accordingly,LKO is well suited for the formal representation of knowledge and requirements of KBSs.Based on the framework,verification techniques are also explored to enhance the analysis of requirement specifications and the validation of KBSs.In addition,LKO provides a methodology for the development of KBSs,applying the concepts of rapid prototyping and top-down design to deal with changing and incomplete requirements,and to provide multiple abstract models of the domain,where formal methods might be used at each abstract level.  相似文献
5.
A case-based approach to software reuse   总被引:2,自引:0,他引:2  
This software reuse system helps a user build programs by reusing modules stored in an existing library. The system, dubbed caesar (Case-basEd SoftwAre Reuse), is conceived in the case-based reasoning framework, where cases consist of program specifications and the corresponding C language code. The case base is initially seeded by decomposing relevant programs into functional slices using algorithms from dataflow analysis. caesar retrieves stored specifications from this base and specializes and/or generalizes them to match the user specification. Testing techniques are applied to the construct assembled by caesar through sequential composition to generate test data which exhibits the behavior of the code. For efficiency, inductive logic programming techniques are used to capture combinations of functions that frequently occur together in specifications. Such combinations may be stored as new functional slices.  相似文献
6.
基于XYZ/E的混成系统   总被引:2,自引:0,他引:2       下载免费PDF全文
混成系统是由计算机和物理设备组成的嵌入式实时计算系统.它允许在交互式实时系统中引入连续变化的单元.XYZ/E 是基于Manna-Pnueli的线性时序逻辑的程序设计语言.它将程序的动态语义与静态语义统一在同一框架中,支持从抽象的程序规范到可执行代码的逐步求精的全过程.该文使用XYZ/E语言描述和验证混成系统.首先介绍了计算模型,然后介绍了XYZ语言对混成系统的形式化描述,最后介绍了混成系统的验证.与同类工作相比,XYZ/E支持状态转换,从而可以方便地描述复杂的控制算法.  相似文献
7.
适用于程序规范说明的Institution范畴的完备性研究   总被引:1,自引:0,他引:1  
Institution作为一般框架下的逻辑系统,在数据库理论、程序设计语言、模块化技术和人工智能等方面有着重要的应用。论文主要研究了Institution范畴的完备性,它直观上表明如果基调类可分解,那么它们对应的Institution也可分解。这为大规模程序设计中模块化程序的安全分解和调用提供了一定的逻辑支持。首先,根据基调类范畴中的极限r:SignD',构造了一个Institution&,讨论了&中的一些性质,特别是闭包引理和表示定理;然后又建立了Institution范畴Ins中相应的极限r:&D,得到了遗忘函子U:Ins→Sig反射极限的重要结论,从而推广了Sign:Th→Sign反射余极限的关键性结果;最后给出了Ins的完备性定理。  相似文献
8.
O-表达式的性质定义与规范   总被引:1,自引:1,他引:0       下载免费PDF全文
在所提出的程序设计方法中,赋值是物理对象上的操作,而程序则是这种操作的表达式。给出了此类表达式(O-表达式)的安全性和进展性性质的形式化定义,用实例说明了基于这些性质的形式化程序规范的模式。具有明确运行目标的O-表达式称为独立O-表达式(stand-alone O-expression,saloe)。一个完整的程序可能由若干个saloe组成。给出了一个定理,指出如何从这些saloe的性质导出完整性程序的性质。用大量实例阐明了程序性质的形式定义。  相似文献
9.
本文在JACKSON程序规格说明和过程蓝图的形式化定义基础上,给出了从JACKSON程序规格说明出发,导出过程蓝图的转换映射方法。使用过程蓝图取代结构文本作为JACKSON程序规格说明和最终目标源代码的中间表示,改进了传统JACKSON结构化程序设计方法。  相似文献
10.
设为首页 | 免责声明 | 关于勤云 | 加入收藏

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