函数－规约混合语言的设计与实现

在函数式语言中引入约束类型和优化规则定义机制，并将扩展的函数式语言与代数规约说明语言相结合，支持从规约到程序的设计，并提高编程的效率及灵活性．混合语言系统将代数规约转换为合流的重写系统，将函数定义、计算约束和优化规则视为重写规则，基于重写模型，以平行最外方法辅以必要归约进行计算．     

函数—规约混合语言的设计与实现

在函数式语言中引入约束类型和优化规则定义机制，并将扩展的函数式语言与代数规约说明语言相结合，支持从规约到程序的设计，并提高编程的效率及灵活性，混合语言系统将代数规约转换为合流的重写系统，将函数定义，计算约束和优化规则视重为规则，基于重写模型，以平行最外方法辅以必要归约进行计算。     

COQ定理证明器辅助PLC 程序验证和分析

使用定理证明器COQ 验证和分析PLC 抢答器程序的一些性质, 证明了原程序的所有可能状态中只有半数是可达状态, 揭示了系统在可达状态之间的转移关系。基于这些性质, 引入了逻辑自动机的概念作为对PLC程序行为完整抽象的描述。此外, 在证明过程中, 发现该程序中存在着一个很难通过现场测试发现的问题。     

Lebesgue积分在PVS中的证明分析

为了有效解决函数系统建模、信号实时分析等数理支持领域验证与测试的定理证明形式化问题,设计并实现了利用Lebesgue积分的运算特征在PVS定理证明器中进行形式化证明与分析.主要对其分裂定理、不等式计算、闭区间子集可积分性、多重分部、线性运算、Cauchy可积分准则和极限定理等多个方面进行了形式化,且依据数学定理与推论形式化,说明Lebesgue积分在PVS中的形式化是可行的、有效的.以标准反相积分器为应用模型,对其通用电路原理与机制进行了形式化证明,通过数理分析测试了本文Lebesgue积分形式化定理库的正确性.     

一种精化演算支撑工具的分析与设计

利用精化演算的方法开发软件，其过程由巨大数量的小步骤构成，由手工完成极其烦琐，也极容易出错，因此利用机器辅助工具的支持是必要的，在分析现有的精化工具的基础上，提出了一个用于软件形式化开发的精化工具，并对其进行了需求分析和功能分析，在精化工具的设计中，讨论了作为定理证明器和精化引擎基础的窗口推理系统和用于程序精化推理的程序窗口推理系统，同时分析了设计中的设计目标，总体结构，精化与证明的表示方法，用户     

一个定理证明检查器

介绍了一种新型的形式说明语言ＰＤ－Ｃａｌ,该语言具有良好的表达能力以及丰富的类型。通过对由该语言描述的定理证明过程进行类型检查,可判断该证明是否是给定定理的正确的证明。在该思想的基础上,设计并实现了ＰＤ－Ｃａｌ定理证明检查器。     

用构造基证明归纳定理

在测试集方法的基础，引入一个新的概念－构造基，用于产生完全的但非冗余的不可归的约基项；提出构造基归纳原理，将显式归纳证明和隐式归纳证明有机地结合在一起。对测试集方法做出了改进，实验表明：这种方法提高了归纳定理的证明效率。     

结构化面向对象形式规格说明语言OOZS——设计原理

形式方法与面向对象方法的综合使用可以使它们各自的优点得到充分体现：形式方法使目标软件系统的需求规格说明简明、精确,面向对象方法使目标软件系统的组织和分解工作更加系统、自然．本文讨论了Ｚ规格说明语言的应用限制,并在Ｚ语言的基础上介绍了结构化面向对象形式规格说明语言——ＯＯＺＳ的设计方法．该语言吸收了面向对象程序设计语言ＳｍａｌＴａｌｋ、Ｃ＋＋以及形式规格说明语言ＶＤＭ、Ｚｃ、Ｚ．Ｓ等的优点,引入了类、继承、入口、出口、Ｐｒｅ谓词、Ｐｏｓｔ谓词等机制,并对Ｚ语言的符号进行结构化处理,提高了形式规格说明的层次性和模块化能力,可用于大型面向对象软件系统需求规格说明的编写     

基于PVS的数据库安全策略形式化分析方法

基于安全策略模型的形式化分析对于数据库管理系统达到高安全保障等级的重要性,提出了新的基于PVS的数据库安全策略模型分析方法,该方法结合了PVS函数式语言的特点,通过一系列算法和流程展示了模块化的系统状态、安全属性、操作规则的定义过程.借助PVS定理证明器对BeyonDB数据库管理系统进行安全性分析,结果表明,该方法不但能够提高形式化建模效率,而且可以有效地发现系统设计中存在的漏洞.     

Carleman不等式的加强及加强式的自动发现

运用最值单调定理及maple数学软件,对有限项Carleman不等式进行非严格化,建立了无限项Carleman不等式一个新的加强式,根据其证明规律,编写程序cdiscover,实现了此类Carleman不等式加强式的自动发现.     

基于关系数据模型代码生成器的设计与实现

在以多层架构实现的数据库应用系统中,大量程序代码与其关系数据模型直接相关,采用一种以关系数据模型为输入的自动代码生成工具,可以大幅度地降低编程工作量,提高软件质量.现有基于模板的代码生成工具具有良好的设计框架,但其脚本语言由于与关系数据模型关联不紧密,导致代码模板编写和维护比较困难,难以快速应用.文中设计一种与关系数据模型紧密结合的迭代式代码脚本语言RDM CodeMark,保留基于模板的代码生成技术通用性的同时,简化代码模板编写难度.结果表明:基于RDM CodeMark语言的代码生成工具在针对J2EE平台和.Net平台的软件项目开发实践中能取得较为理想的效果.     

Effect of curing time on the mesoscopic parameters of cemented paste backfill simulated using the particle flow code technique

Several special mechanical properties, such as dilatancy and compressibility, of cemented paste backfill(CPB) are controlled by its internal microstructure and evolution.The mesoscopic structure changes of CPB during the development process were investigated.On the basis of the scanning electron microscopy(SEM) and mechanical test results of CPB, the particle size information of CPB was extracted, and a two-dimensional particle flow code(PFC) model of CPB was established to analyze the evolution rule of mesoscopic parameters during CPB development.The embedded FISH language in PFC was used to develop a program for establishing a PFC model on the basis of the SEM results.The mesoscopic parameters of CPB samples at different curing times, such as coordination number(C_n), contact force chain, and rose diagram, were obtained by recording and loading and used to analyze the intrinsic relationship between mesoscopic parameter variations and macroscopic mechanical response during CPB development.It is of considerable significance to establish the physical model of CPB using the PFC to reveal the mesoscopic structure of CPB.     

用颗粒流模拟技术模拟固化时间对胶结膏体细观参数的影响

Several special mechanical properties, such as dilatancy and compressibility, of cemented paste backfill (CPB) are controlled by its internal microstructure and evolution. The mesoscopic structure changes of CPB during the development process were investigated. On the basis of the scanning electron microscopy (SEM) and mechanical test results of CPB, the particle size information of CPB was extracted, and a two-dimensional particle flow code (PFC) model of CPB was established to analyze the evolution rule of mesoscopic parameters during CPB development. The embedded FISH language in PFC was used to develop a program for establishing a PFC model on the basis of the SEM results. The mesoscopic parameters of CPB samples at different curing times, such as coordination number (C_n), contact force chain, and rose diagram, were obtained by recording and loading and used to analyze the intrinsic relationship between mesoscopic parameter variations and macroscopic mechanical response during CPB development. It is of considerable significance to establish the physical model of CPB using the PFC to reveal the mesoscopic structure of CPB.     

基于通用接口母线的自动测试方法

论述基于GPIB智能化测试系统的原理和设计开发方法。通过高级语言封装，统一发送命令、接收执行结果和执行结果提取函数，系统建立了逻辑规则库，在测试过程中根据测试结果与设置的报警阈值等参数进行比较，根据设定的判断规则，对测试流程进行动态调整。     

Model-based embedded compiled software fault positioning

Software fault positioning is one of the most effective activities in program debugging. In this paper, we propose a model-based fault positioning method to detect the faults of embedded program without source code. The system takes the machine code of embedded software as input and translates the code into high-level language C with the software reverse engineering program. Then, the static analysis on the high-level program is taken to obtain a control flow graph (CFG), which is denoted as a node-tree and each node is a basic block. According to the faults found by the field testing, we construct a fault model by extracting the features of the faulty code obtained by ranking the Ochiai coefficient of basic blocks. The model can be effectively used to locate the faults of the embedded program. Our method is evaluated on ST chips of the smart meter with the corresponding source code. The experiment shows that the proposed method has an effectiveness about 87% on the fault detection.     

采用C语言实现CNC系统的输入控制

提出采用C语言实现CNC系统的输入控制,为CNC系统控制软件的开发建立了良好的开发平台.并重点分析了采用C语言实现零件加工程序的存储和程序段逐段解释译码过程以及它们各自的特殊处理技术——压缩存储技术和特征字代码表的建立和应用.     

C++函数重载实现方法剖析

目的剖析C 中重要语法函数重载的实现机制,应用获得的结果,分析C 和C语言中的相关语法特征。方法采用Visual C 为实验工具,利用编译器生成的COD文件,对源代码和相应的汇编代码进行比对、归纳,得出结论。结果获得了C 函数重载的实现方法的关键策略,获得了关键策略中的部分编码规则,解释了相关语法现象。结论改名策略是C 函数重载实现机制的关键,也是实现C 中类型安全的链接的特征的基础,可以利用该实现策略对C语言中函数的相关语法进行解释。     

COC++ 编译器面向对象技术的实现

ＣＯＣ＋＋编译器的功能是将Ｃ＋＋源程序转换为等价的Ｃ程序。ＣＯＣ＋＋编译器不是使用传统的构造方法而是采用面向对象的设计技术，将相应成分如符号表，语法分析等模块封装为类，并以Ｃ＋＋语言实现。符号表类封装符号表及其建立、登录、查找等操作。基于Ｃ＋＋的作用域规则，ＣＯＣ＋＋编译器为每个作用域中的符号建立一个符合表，利用指针链指明嵌套关系和继承关系。语法分析的模块设计为一个抽象类，定义所有语法成分类的公共特性和公共接口。实际的分析工作和语义处理工作通过Ｃ＋＋语言的多态机制由相应的派生类各自的成员函数实现。这样类化的编译结构不会因为增加某些语言成分而做很大的改动。阐述了面向对象的技术用于编译系统的设计和开发的特点。     

PHP中实现APPLICATION级别的多用户数据共享

PHP网站开发语言中不支持APPLICATION应用,本文对比ASP网站开发中APPLICATION的应用,分析了如何在PHP网站开发中实现类似功能,详细阐述了两种方法来实现PHP中不同用户间数据共享,分析了它们的优缺点,通过模块化开发,为PHP网站开发语言编写一个可行的APPLICATION类模块程序代码,通过调用该模块,方便实现多用户数据共享。