通过抽象程序证明复杂具体程序

本文描述了证明抽象程序和具体程序满足一致性关系的方法.抽象程序使用抽象数据结构（ADTs）如set、list、map及其上的操作.具体程序使用类C语言中的类型.抽象程序和具体程序一致性证明需要用户给出抽象变量和具体变量的关系,抽象程序程序点和具体程序程序点的对应关系.基于对应关系,抽象程序和具体程序一致性证明可以分解,从而容易并可能自动证明.     

抽象类型在程序开发中的应用

本文邓开发中的抽象类，并给出了类型更改方法和类型实经的方法。本文还用例子说明了具体计算结构实现的方法。     

综合网管中的抽象代理技术

提出异网管理的抽象代理及其相关的虚拟网络，抽象管理信息模型等概念，并对抽象代理体系结构，抽象管理信息模型的实现方案作了研究。     

Agent插件在PowerBuilder程序开发中的应用

使用过office xp、金山毒霸和瑞星杀毒软件的朋友,一定会对程序中的人性化的动画角色留下深刻印象,这完全归功于微软推出的Agent("代理")技术,Agent采用COM技术,使用ActiveX控件方式,支持现在流行的各种开发工具,不仅可以实现文本的朗读,而且可识别用户的语音命令,在应用程序和HTML文件中得到广泛的使用.     

软件模型检测中的抽象

软件模型检测对保证软件的正确性和可靠性具有十分重要的意义，而抽象是减轻模型检测中状态爆炸问题最重要的技术之一。本文综述当前广泛应用于软件模型检测中的抽象技术，介绍了该领域的进展及研究方向。     

电脑装帧设计的程序与操作方法

一、电脑装帧设计的程序电脑装帧设计的程序分为:创意构思——手工草图——电脑操作三个阶段.1.创意构思如儿童读物的装帧设计,首先要考虑此装帧设计必须要有强烈的装饰风味,,其次要考虑盒封的整体规范以及产品的市场认读性和名牌正品效应,这是至关重要的环节.设计定位明确才能对每一个产品进行具体的想象构思.下面,我们就《英语情景剧场》、《狐狸吃葡萄》、《作文开心豆》和《唱歌学英语》四个光碟的封面装帧的构思作一介绍.题材确定后,怎样去表现这四个主题,在画面上用什么形象去表现主题,这就是构思过程.难点是要充分理解可视读物的内涵、题材,风格设计既要构思新颖,具有时代性,又不落俗套,同时还要切题,有较强的吸引力.     

谓词抽象技术研究

随着软、硬件系统规模和功能的不断扩充,状态空间爆炸问题严重影响了模型检验的进一步发展与应用,成为验证大规模系统的瓶颈.谓词抽象是解决状态空间爆炸的最有效方法之一,近年来得到迅速发展.介绍了谓词抽象的基本算法并比较了不同的求解支持工具;重点分析了反例指导的抽象求精和基于插值的抽象求精原理;分析了产生新谓词的各种方法的优、缺点;最后指出了谓词抽象技术进一步发展所面临的挑战和发展方向.     

智能神经网络程序设计语言的研究与实现

将神经网络与逻辑推理统一到面向对象理论中,建立了同时具备神经网络和专家系统特性、融合连接机制和符号机制的智能神经元模型。提出了一种新的程序设计语言——智能神经网络程序语言(NIPL),实现了神经计算、逻辑推理和数值计算的统一。定义了NIPL的语法,设计并实现了智能神经网络程序设计语言NIPL编译器,从而为开发智能神经网络应用系统提供了有效的手段。     

程序菜单设计与实现

一、菜单的可视化设计及其命令映射 在这里我们先来打开11期中《文档数据的读取和显示》中的单文档应用程序项目Viewer,然后对其菜单和工具栏进行设计。     

基于抽象解释理论的程序验证技术

抽象解释(abstract interpretation)理论是Cousot.P和Cousot.R于1977年提出的程序静态分析时构造和逼近(approxiamation)程序不动点语义的理论.描述了程序语义基于Galois连接的抽象解释理论框架,讨论了基于抽象解释理论的程序变换、程序安全性验证和活性性质验证这3种典型的应用,并指出了基于抽象解释理论的程序验证的主要研究方向.     

Uniform Closures: Order-Theoretically Reconstructing Logic Program Semantics and Abstract Domain Refinements

The notion of uniform closure operator is introduced, and it is shown how this concept surfaces in two different areas of application of abstract interpretation, notably in semantics design for logic programs and in the theory of abstract domain refinements. In logic programming, uniform closures permit generalization, from an order-theoretic perspective, of the standard hierarchy of declarative semantics. In particular, we show how to reconstruct the model-theoretic characterization of the well-known s-semantics using pure order-theoretic concepts only. As far as the systematic refinement operators on abstract domains are concerned, we show that uniform closures capture precisely the property of a refinement of being invertible, namely of admitting a related operator that simplifies as much as possible a given abstract domain of input for that refinement. Exploiting the same argument used to reconstruct the s-semantics of logic programming, we yield a precise relationship between refinements and their inverse operators: we demonstrate that they form an adjunction with respect to a conveniently modified complete order among abstract domains.     

师范院校计算机专业程序类课程群设置

针对目前社会中存在岗位与学生供求不平衡的状况,在分析目前师范类院校计算机专业的程序类课程群设置不足的基础上,结合某校在计算机专业程序类课程群建设方面取得的部分成果,提出师范院校计算机专业程序类课程群建设的几个观点。     

基于抽象解释的C程序信息保密性研究

在分析程序具体语义的基础上,提出一种信息保密性检测方法。构造具体语义和抽象语义的对应关系,根据待测程序性质构建抽象语义,同时在抽象基础上,采用限界思想来优化检测的效率。通过该方法降低程序检测的复杂性,减少时间和空间的浪费,提高了检测的效率和准确度。     

加强程序设计课程群建设,培养计算机应用型人才

在计算机专业应用型人才的培养过程中,程序设计能力是衡量学生专业水平的一个关键因素,是影响计算机专业学生就业率的一个重要因素。通过对课程群建设的理论分析,结合我校的实际情况,针对计算机专业的程序设计课程群建设进行规划．切实培养学生程序设计的学习兴趣,促进计算机专业应用型人才的培养。     

Lightweight Reasoning about Program Correctness

Automated verification tools vary widely in the types of properties they are able to analyze, the complexity of their algorithms, and the amount of necessary user involvement. In this paper we propose a framework for step-wise automatic verification and describe a lightweight scalable program analysis tool that combines abstraction and model checking. The tool guarantees that its True and False answers are sound with respect to the original system. We also check the effectiveness of the tool on an implementation of the Safety-Injection System.     

基于抽象符号表的内存模型

符号执行技术在软件测试和程序验证中发挥着重要作用。如何抽象和处理程序中各种数据类型和语法成分是符号执行必须解决的问题。本文提出抽象符号表的概念,以及基于抽象符号表建模内存的方法。抽象符号表记录可寻址对象的名称、类型、抽象地址和符号值,是一种简单、精确的内存抽象机制。内存模型是所有使用符号执行的技术的前提,本文系统给出了一个面向符号执行的内存模型。基于抽象符号表的内存模型能够统一处理各种数据类型和语法成分,包括函数和类,能够直接处理指针别名问题,不需要额外的别名分析算法。经过一些性能优化处理,基于抽象符号表的内存模型具有较好的性能。     

VisualBasic程序设计课程中计算思维能力的培养

Visual Basic程序设计是非计算机专业学生必修的一门计算机基础课程,在计算机能力培养方面发挥着重要的作用。而计算思维能力培养是计算机基础课程教学的核心任务,为此,探究了如何在Visual Basic程序设计课程的教学过程中培养学生计算思维的能力。首先介绍了计算思维的基本概念,然后从师生角色定位、教学模式、教学内容方面阐述了为了培养Visual Basic程序设计课程中的计算思维能力而采取的方法和措施,最终取得了较好的实施效果。     

一种混合模式两级抽象服务粒度划分法

该文首先介绍了当前服务粒度划分研究现状,并对几种主流服务粒度划分方法进行分析,指出了它们的不足之处,进而提出了一种基于业务、组件、类的混合模式两级抽象粒度划分方法——TAMM,该方法利用混合模式并结合java设计模式思想对服务粒度划分过程进行两级优化组合抽象,以适中的粗细粒度优化组合抽象服务,从而提高服务的稳定性、灵活性及性能。最后,结合实际案例对该划分方法的特性进行了分析说明。     

VFP程序设计中应避免的几个问题

Visual FoxPro是一个功能强大的数据库管理系统,它以其独到的特点和优势赢得了开发者的青睐。本文指出了Visual FoxPro程序设计中应避免的几个问题,并对此给出了具体的处理方法。