脉动阵列算法自动综合的优化策略

对于脉动阵列算法的自动综合方法，本文揭示了参数确定法和相关性变换法的本质联系，给出了相关性变换法适用问题类的一个新的高效寻优策略。     

A prolog technology theorem prover: Implementation by an extended prolog compiler

A Prolog technology theorem prover (PTTP) is an extension of Prolog that is complete for the full first-order predicate calculus. It differs from Prolog in its use of unification with the occurs check for soundness, the model-elimination reduction rule that is added to Prolog inferences to make the inference system complete, and depth-first iterative-deepening search instead of unbounded depthfirst search to make the search strategy complete. A Prolog technology theorem prover has been implemented by an extended Prolog-to-LISP compiler that supports these additional features. It is capable of proving theorems in the full first-order predicate calculus at a rate of thousands of inferences per second.This is a revised and expanded version of a paper presented at the 8th International Conference on Automated Deduction, Oxford, England, July 1986.This research was supported by the Defense Advanced Research Projects Agency under Contract N00039-84-K-0078 with the Naval Electronic Systems Command and by the National Science Foundation under Grant CCR-8611116. The views and conclusions contained herein are those of the author and should not be interpreted as necessarily representing the official policies, either expressed or implied, of the Defense Advanced Research Projects Agency, the National Science Foundation, or the United States government. Approved for public release. Distribution unlimited.     

在线性处理机阵列上求MCST的并行算法

本文给出一种在P个处理机线性阵列上求MCST(最小代价生成树)的并行算法,记为OLA-MCST.证明了在整个1≤P≤n范围内其时间复杂性均为O(n~2/P);特别地,当P=n时,为O(n).这是在本模型下使用n个处理机时的最优性能.     

An approach to systems verification

The term systems verification refers to the specification and verification of the components of a computing system, including compilers, assemblers, operating systems and hardware. We outline our approach to systems verification, and summarize the application of this approach to several systems components. These components consist of a code generator for a simple high-level language, an assembler and linking loader, a simple operating system kernel, and a microprocessor design.     

分块同步磁盘阵列数据存取时间近似计算

本文提出了一种有效的计算分块同步磁盘阵列数据存取时间的近似方法。分析表明，要获得较好的近似效果，应将分块度限制在２０以内。     

网孔处理机阵列上最小生成树算法

已知一加权无向图G(V,E),|V|=n.本文基于网孔处理机阵列,运用分而治之策略和数据归约技术给出了一种新的最小生成树算法.此算法需O(n~2/p)时间,使用了O(p)个处理机(1≤p≤n).当p=n时,此算法仅需O(n)时间和O(n)处理机.而目前基于同一计算模型上此问题的最好算法需O(n)时间和O(n~2)个处理机,因而这里给出的算法在使用处理机数目方面改进了O(n)因子.     

一维Walsh变换的阵列协处理器的设计

本文给出了一种用短序列Walsh变换芯片构成长序列Walsh变换阵列协处理器的方法.按此法,易用2~t片2~t长芯片构成2~(2t)长的Walsh变换的阵列协处理器,并且易用2~(t+1)片2~t长芯片及2~(2t)个蝶形运算器构成2~(2t+1)长的Walsh变换的阵列协处理器.     

应用稀疏数组存储病案首页数据研究

病历数据性质特殊,一般数据模型用于其管理比较困难,因此需要研究寻找适合的特殊数据模型。病案首页是病历的一种摘要,病历数据的许多特性均反映到病案首页中。本文将介绍一种应用稀疏数组存储病案首页的存储结构设计,以及基于稀疏数组的病案首页系统如何利用稀疏数组的特性,使存储结构既能保证长久数据的应用连续性,又能不断适应结构变化,同时介绍其独特的数据存储体系和数据备份方案。     

Web应用中数据库交互行为验证

采用定理证明和逆向工程的方法,对Web应用中的数据库交互行为进行验证。使用Z规格说明描述需求模型,根据数据库交互的源代码和转换规则得到实现模型。从实现模型中获取Web应用的相关性质,通过Z/EVES定理证明器验证这些性质是否在需求模型的 Z规格说明中得到满足。在此基础上,设计该方法的验证框架,并开发相应的原型系统。通过图书馆数据库管理系统实例证明该方法的有 效性。     

一种归并排序算法的阵列映射

本文介绍一种归并排序算法－－插入归并算法的基本原理，并通过该算法的Ｓｙｓｔｏｌｉｃ阵列映射，重点阐述了正则映射生成ＶＬＳＩ阵列的理论和方法，最后，还指出了改进脉动阵列通用性和灵活性的途径。     

LINEAR ARRAY FOR A CLASS OF NON UNIFORM RECURRENCE EQUATIONS

In this paper we present a new scheduling algorithm to solve the class of non uniform recurrence equations on the linear systolic array. The main idea is to use the fact that data dependency graph of the dynamic programming function of the problem is an irregular mesh. We propose a scheduling algorithm for irregular meshes on the linear array by an allocation function and an initial time for each node.     

软件需求定义语言NDRDL的设计

本文概述了软件需求定义语言ＮＤＲＤＬ的设计目标及设计原则，并讨论了一些语言基本成分，如数据流图，控制流图，实体关系图等的设计，文中采用个人帐目管理系统作为示例。     

A Complete Mechanization of Correctness of a String-Preprocessing Algorithm

We report on mechanization of a correctness proof of a string-preprocessing algorithm. This preprocessing algorithm is employed in Boyer-Moore’s pattern matching algorithm. The mechanization is carried out using the PVS system. The correctness proof being mechanized has been formulated in Linear Time Temporal Logic. It consists of fourteen lemmata which are related to safety properties and two additional lemmata dealing with liveness properties. The entire mechanization of the safety and liveness parts has been completed. Several small errors and omissions were found in the handwritten proof and corrected. Yet, the manual correctness proof of the string-preprocessing algorithm was found to satisfy the usual mathematical validity. We conclude that the string-preprocessing algorithm in Boyer-Moore’s pattern matching algorithm, corrected a number of times because of flaws, does not contain any more undiscovered errors. An extended abstract of this work appears in the Proceedings of the 8^th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS ‘02).     

一种新型智能机器人敏感皮肤的触觉传感器阵列

本文提出了一种眼精密，高位置分辩率，快速响应的，可任意分布的，便于大规模集成的智能化机器人的多参量融合的的阵列触觉传感器，介绍了石英晶振精密分布测量压力，形变，温度，生物量和化学量的原理。该系统传感及信号传输方法独特，精度，分辩率和响应速度等指标优于其他机器人敏感皮肤系统。     

集成式磁盘阵列及主机接口设备驱动程序的设计

本文介绍了我们研制的一种集成式磁盘阵列系统的结构，重点介绍了其主机接口的硬件结构和设备驱动程序的设计方法。     

证明开发环境中的元语言设计

本文通过对数型赋予操作解释，将ＬＦ的逻辑定义风格的λＰｒｏｌｏｇ的逻辑程序设计风格融于一体，提出了旨在对定理证明过程进行元级编程的元语言ＴＭＬ及其抽象解释器，然后，利用项推理过程给出了ＴＭＬ元程序的正确性检查算法。     

水下声纳基阵姿态鲁棒控制频域设计

对水下声纳基阵运行姿态伺服系统进行了建模和鲁棒控制器的设计，在计算机上对所设计的系统进行了数字仿真。讨论了在随机海浪作用下船的艏摇角姿态随机运动的数字仿真问题，结果表明，当系统参数在允许范围变化时，所设计的鲁棒控制伺服系统具有满意的性能指标。