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

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

C程序不变量动态发现编配工具的设计

程序不变量是用于描述程序运行过程中某些保持不变的性质的逻辑断言.程序编配的任务是通过对程序改造,暴露程序的运行轨迹,然后在通过对轨迹分析完成程序不变量的发现.程序编配是程序不变量过程中的关键步骤.本文介绍了C程序编配的工作原理和主要方法,并详细说明了采用内嵌法的编配工具的设计过程.     

基于不变量的程序运行保护方法

程序不变量反映了程序在特定点上的安全属性,可以作为运行保护时的监控对象.提出了一种程序运行保护方法,通过动态监控程序不变量,保护程序安全运行.该方法根据检测出的程序不变量,配置程序保护策略.运行环境支持对程序插装保护代码,执行保护策略.实验表明方法是有效的且使用方便,保护带来的性能损失不大.     

用VB4为Windows95编制屏幕保护程序

Windows屏幕保护程序一般以.SCR的形式存放在SYSTEM目录中,比如在安装Windows 3.x之后将存在以下屏幕保护程序:SSFLYWIN.SCR、SCRNSAVE.SCR、SSMARQUE.SCR等。这些屏幕保护程序在结构上与Windows的可执行程序*.EXE文件非常相似,从实质上说它本身就是一个Windows的应用程序。但在Windows 3.x下的屏幕保护程序与一般的Windows程序稍有差别,在屏幕保护程序内部存在特殊标志供Windows识别,只有具有此标志的程序才能被Windows的桌面设置程序承认并使用。当你进行屏幕保护程序设置时会发现,在可选框内列出的不是屏幕保护程序的程序名,而是代表相应屏幕保护程序内容的名字,这些内容就是从屏幕保护程序内部的固定位置读出的。所以在Windows 3.x下你可以把任一个屏幕保护程序.SCR文件改名为.EXE文件,然后即可在程序管理器或文件管理器中正常运     

用Z形式化描述程序切片

程序切片是一种重要技术,已广泛地应用于软件工程的各个领域,如程序理解、维护、调试、测试、复用、度量等.虽然,越来越多的研究者致力于程序切片工作,然而由于缺少形式化方面的工作导致程序切片可能存在不一致性和模糊性.本文尝试着用Z语言来形式化描述程序切片,考虑了程序切片中诸如程序依赖图和程序切片算法等常用的方面.该形式化描述不仅能帮助人们正确地理解程序切片的含义,而且还能够从比较严格的意义上明确程序切片的应用领域.     

Linux聊天室开发

在Linux下开发了一个聊天室程序,可实现Linux下文字、文件的实时交互功能.程序分为服务端和客户端两个程序,采用流式套接字进行通信.客户端程序使用GTK开发用户界面介绍了程序的开发思路和技巧,对于在Linux下开发类似程序有参考价值.     

程序插装在软件测试中的应用研究

程序插装是软件测试中一种重要的白盒测试技术.介绍了程序插装的基本原理,分析了程序插装的关键要素,研究了插装测试设计的主要内容.针对常用的程序结构,如线性程序、结构化程序、面向对象程序的不同特点,提出了相应的程序插装策略和测试实现方法.在插装测试实践中,根据程序测试的规模、要求等,需要综合考虑程序插装对被测程序性能、执行...     

基于合约的程序不变量动态检测模型研究

讨论了程序不变量的内涵,研究并建立了程序不变量动态生成系统的理论模型.主要描述基于合约的似然程序不变量发现的基本理论模型,以及程序不变量发现的主体过程,并结合Java程序设计语言进一步阐明函数依赖程序不变量动态发现的一种方法.通过程序不变量动态生成技术,可以分析程序内部的关联属性,从而有助于设计高质量的程序代码以及规范化的程序架构.     

用Delphi实现动态时钟程序

所谓动态时钟程序,在这里是指能够准确地显示当前时钟的程序.诸如此类的程序到处可见,像Windows操作系统中任务栏的右下角的时钟程序.     

基于线程的Java程序自动并行转换技术

Java程序的并行化研究是一个重要课题.提出一种Java程序的自动并行转换技术,并充分利用Java语言本身提供的多线程机制,通过操作冲突性检测等方法将串行化的Java程序自动转化成并行化程序.使得转化后的并行化程序在多处理机操作系统的支持下,能在共享内存的多处理机系统上运行,从而提高了程序的运行效率.     

一种面向对象程序的分层切片方法

程序切片是一种程序分析技术,广泛应用于程序的调试、测试、理解和维护等软件开发的各个阶段.在研究静态类型面向对象的程序切片时发现,利用系统依赖图计算程序切片虽然是一种有效的方法,但构造OO程序的系统依赖图是一件非常复杂的工作,而且构造过程中容易出错,这会导致切片的结果不正确,造成前功尽弃.为此,从程序逻辑分层的角度提出一种OO程序的层次模型,然后在OO程序的层次模型基础上采用逐步求精算法来分层计算OO程序的切片.     

用于Hadoop2.x的MapReduce性能评估模型

基于MapReduce的程序被越来越多地应用于大型数据分析的应用中.Apache Hadoop是最常用的开源MapReduce模型之一.程序运行时间的缩短对于MapReduce程序以及所有数据处理应用而言至关重要,而能够准确估算MapReduce程序的执行时间是优化程序的重要环节.本文定义了一个在Hadoop2.x版本...     

怎样在程序中与命令行程序交互

?命令行程序存在的意义是什么? ! 当前绝大部分应用程序都是GUI的,即图形界面交互程序,CUI(命令行程序)程序已经不是主流了,但是在某些情况下还必须使用命令行程序,比如服务器上的脚本程序等等.另外,许多图形界面程序往往同时伴有一个命令行程序版本,这说明至少在当前,命令行程序还有其存在的必要性.以调用Winrar程序的命令行版本为例子,来介绍一下.net程序如何与命令行版本交互.     

一类线性循环程序的终止性判定

提出一种判定这类线性循环程序是否终止的新方法,该方法通过分析循环变量每次迭代后的状态.最后得到循环条件的满足与否只是与变量的初始值和迭代的次数有关.从而判断该循环程序是否终止.根据该方法,不但能判断这一类程序是否终止.对于不是对所有输入都终止的程序,还能够给出程序终止的输入条件.     

面向语句分值的C程序静态评分方法

针对现有评测方法结果过于粗糙的问题,提出面向语句分值的C程序静态评分方法.定义答案程序中语句分值的表示形式,引入程序语句依赖图准确表示待判定程序的语法结构;基于语句分值及依赖关系将程序语句依赖图划分为路径片段集合,通过匹配待判定程序和答案程序的路径片段集合相似度获得程序分值.实验结果表明,相比现有评测方法,该方法能够明显提升程序评分的准确度.     

程序重构预处理在提高软件模型检测效率中的应用

针对软件模型检测目前很难处理大型程序的问题,提出用程序重构技术对待检的源代码进行预处理,以提高模型检测算法的效率.程序重构将大型程序分解成语义一致的小型过程的集合,由于模型检测算法中过程总结边可单独计算,而且在程序中对某过程的调用可能有多次,这种预处理可以避免状态空间的重复搜索,从而降低模型检测算法在空间和时间上的开销.根据表达程序性质的线性时序逻辑LTL公式的构成,给出了程序重构预处理前后程序语义相等的充分条件;并给定程序和性质公式,用blast作为程序模型检测实验工具,比较程序重构预处理前后blast的运行结果.理论分析和部分程序上的实验表明:程序重构预处理能降低大型程序的模型检测开销,并满足软件模型检测的安全性要求.     

基于机器学习的源程序自动标注方法

程序注释是软件开发过程中不可缺少的工作.大量的Java程序需要准确的注释来提高程序的可维护性.对自动标注方法进行研究,分析现存方法存在的问题,为了改善注释的效率,提出一种基于机器学习的程序注释自动标注方法用于Java程序的自动标注.方法 主要分为两个部分:数据的预处理和机器学习模型.数据预处理采用双编码器对程序进行处理,通过已训练的GRU神经网络模型对未注释的Java程序进行自动标注.实验表明该自动标注方法在准确率、时间等性能方面都有显著的提升,提高了源代码的可读性.     

程序缺陷分析与安全保护技术研究

程序安全是信息安全研究的一个重要方向,主要研究程序缺陷分析和安全保护技术等.介绍程序缺陷分析研究及其分类方法,然后将程序安全保护研究分为三类主要途径进行重点阐述和分析,最后讨论程序安全研究的发展趋势.     

基于断言的程序正确性检测工具

文章提出了程序断言检测工具设计方案和基于断言的程序正确性检测步骤.该工具的基本原理是Floyd提出的"用断言式方法"证明程序的正确性的方法,通过一个断言发现工兵从程序中发现该程序断言,然后与程序要求满足的断言条件比较,判明其正确性.该工具在复杂条件下对程序正确性判断和大量重复程序检测上能发挥重要的作用.     

基于微课的《ASP.NET程序设计》课程教学模式改革与创新

“微课”教学作为当下教育行业中一种新兴的教育方式,尽管微课视频在教学中的广泛应用在一定程度上促进了教学任务的完成,但仍存在一定程度上的局限性,为此,开展了基于微课的《ASP.NET程序设计》课程教学模式改革与创新的研究。通过明确《ASP.NET程序设计》课程教学目标,构建《ASP.NET程序设计》课程教学资源共享平台,根据“三个课堂”教学方法,改革《ASP.NET程序设计》课程教学评价机制,创新《ASP.NET程序设计》课程教学模式,获得《ASP.NET程序设计》课程教学理念、教学内容的创新以及个性化《ASP.NET程序设计》实践训练,实现基于微课的《ASP.NET程序设计》课程教学模式的改革与创新。