Institution中自由合并理论的初始与终结语义*

在一般性的适用框架Institution中,建立了自由合并理论与各因子理论的初始(终结)语义之间的对应关系,给出了自由理论态射的粘合态射及其相关的初始(终结)语义,并证明了在一定条件下,遗忘函子Sign:Th^l→Sign的反射余极限.     

正则序类逻辑Institution的Lawvere定理及其初始与终结语义

主要考虑了以下3个问题:(1) 通过将正则序类理论态射(延拓为多类型理论态射,得到了模型函子( )·和( )#都与(可交换的结论;(2) 获得了正则序类逻辑Institution的Lawvere定理;(3) 讨论了正则序类逻辑Institution中合并理论与各因子理论的初始和终结语义.     

关于三值逻辑程序中否定和蕴涵完备化程序的不动点语义

逻辑程序具有丰富的表达能力和非确定性等特点，在定理机器证明、关系数据库系统、程序验证、模块化程序设计和非单调推理等方面都有了广泛的应用。本文是继续文[8]的工作。首先通过两个反例，指出了文[7]中关于否定完备化程序Comp（→，Pr）和蕴涵完备化程序Comp（→，Pr）的两个重要定理都存在一定程度的错误。然后对这两个定理进行了修改，用后继算予Tpt和Fitting算予FPr的不动点语义，分别给出了否定完备化程序（Somp（→，Pr）和蕴涵完备化程序Comp（→，Pr）的Herbrand模型的充分条件和必要条件，这将在逻辑程序的最优不动点和最小不动点的语义研究中有着重要的应用价值。     

程序设计语言的代数规格说明方法

程序设计语言的形式规格说明是程序设计语言标准化、编译器自动生成和程序正确性证明的基础。良好的形式规格说明对语言的设计者、实现者和使用者都是有益的。 1.程序设计语言的代数规格说明方法 代数规格说明方法起源于ADJ小组,他们把语言的语法作为初始代数T,语义论域则是同样基调(signature)上的代数A,使得语言的语义由唯一同态f:T→A自动给     

光学图层分解方法综述

光学图层分解能够为物体识别提供有用信息,是图像内容理解和分析的基础。按照输入信息的不同可以将光学图层分解方法分为基于单幅图像和基于图集2类。对典型的光学图层分解方法进行论述和分析,包括交互式图层先验法、相对光滑度分解法、多重反射信息法、交互层叠法、反射变换法和稀疏性运动盲源法,阐述这些方法的原理和特点。结合软件测试平台验证和分析上述光学图层分解方法的优缺点及适用范围,并对光学图层分解方法的时效性、完备性和实用性进行展望。     

并发面向对象语言的继承异常问题研究

1·引言随着面向对象技术的发展,面向对象程序设计语言在软件设计、模块化、可扩充性、可复用性等方面给软件开发人员带来了很大的方便[lj。继承是顺序面向对象语言的一个基本特点,继承机制是面向对象语言的重要机制之一,是实现软件复用和可扩充的有效语言机制。Bertrand Meyer曾指出纯00语言的七个特性川:①模块化结构;②数据抽象(对象是抽象数据类型的实现);③自动     

基于范畴计算的多目标语言程序生成架构

提出了一种基于范畴论的多目标语言程序生成架构,程序元素的元类型在程序元模型范畴中定义,常用的软件开发模式由元模型实例组成并带有可配置的参数,模式到可执行语言的表达式、函数、类型等映射由范畴函子统一定义。在实际应用开发时,通过函子计算将抽象模式精化到不同的目标语言程序范畴。各种语言的精化计算方式具有统一的契约规范,从而支持高度的灵活性和重用度水平。     

基于并行处理环境的多类命题动态逻辑系统

本文提出了一个描述并行处理环境下程序动态特性的多类命题动态逻辑和多类结构，并使用ＭＰＤＬ描述一个实际问题。本文使用了新算子Ｇ＾ｉｊ来描述并行程序间的关系，最后，本文简单地讨论了ＭＰＤＬ的一致性和完备性。     

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

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

可靠性与完备性定理中描述形式等价性证明以及应用的讨论

本文首先分别讨论了可靠性定理和完备性定理中不同描述形式的等价性,然后讨论了对于可靠性和完备性定理应用的理解。     

Categorical ML — Category-theoretic modular programming

We consider an extension of the functional programming language Standard ML with a modular structure based upon concepts in category theory such as categories, functors, natural transformations and adjunctions. In essence, we are following the categorical imperative of considering arrows as well as objects. This is intended to enforce a certain mathematical rigour on the programmer, so that the only programs that can be expressed are those with a categorical significance. The essentially algebraic nature of category theory means that we may generate equational correctness conditions for the modular structure of programs, thus separating the correctness of individual functions from that of modules. We describe this programming language, give examples of its use, and explain how it is implemented in a type system.     

无需随机预言的无证书聚合签名方案

现有的聚合签名方案大多数是在传统公钥密码体制或者基于身份的密码体制提出的,都存在证书的管理问题和密钥托管问题。最近Gong等人提出聚合签名是在无证书密码体制下的。然而,他们的方案是在随机预言模型下可证安全的。在无证书公钥密码体制的基础上提出了一个无需随机预言模型下的聚合签名方案。新方案不但具有不需要数字证书同时也不存在密钥托管问题的特点,并且还满足无证书聚合签名安全需求。此外与现存的无证书聚合签名方案相比,新方案在性能上具有明显的改进。     

基于辫群的代理签名方案的分析与改进

对两个基于辫群的代理签名方案进行了分析,发现它们并不满足不可伪造性。第一个方案中不能抵抗原始签名人改变攻击,在第二个方案中任何攻击者可以伪造一个有效的代理签名,在该签名中,代理签名者以及消息可以任意指定。根据上述缺陷,提出一个改进的强代理签名方案, 新方案在不增加计算复杂性的前提下,保证了签名的安全性,同时代理授权过程中还增加了不需要安全通道的性质。     

一种基于格理论的数字签名方案

本文介绍了一种建立在解决NTRU格（NTRU Lattice）中近似最近向量问题（Appr-CVP）基础上的数字签名方案.与现有的基于解决Appr-CVP问题的数字签名方案相比，这种新的数字签名方案通过构造完整的短格基进行签名，在签名与近似最近向量问题之间建立了直接而清晰的关系，因此不需引入任何附加结构，具有更高的安全性.同时，该签名方案引入了适当的扰动，有效地限制了攻击者通过分析大量签名副本所获取的有用信息，具有副本分析免疫性.实验结果表明：该方案不仅安全可靠，而且易于实现.     

具有时效的Chameleon签名方案的设计与分析

基于Chameleon签名理论，提出具有时效的Chameleon签名方案，为需要指定签名接收者，且对签名时效有一定要求的签名问题提供了解决途径。该方案保证在时效期限内，只有指定的接收者能够验证签名的有效性；超过时效期限后，签名转换为普通签名，并且签名转换的决定权不再限于签名者，任何人都可以核实监督甚至强制要求签名者按时转换签名。该方案设计简单、易于实现，而且在签名效率与安全性等方面都优于现有的可转换Chameleon签名方案。     

免疫原理在计算机病毒检测中的应用

主要探讨免疫原理在计算机病毒检测中的应用,并实现了一种将否定选择、克隆选择等生物免疫机制应用于传统的基于特征码的计算机病毒检测法.实验表明,该方法具有检测已知病毒和识别病毒的一些未知变种的能力,能够自动提取特征码,并且生成的病毒特征码具有很低的误别率,是一种实用的计算机病毒检测的方法.     

Pose-oblivious shape signature

A 3D shape signature is a compact representation for some essence of a shape. Shape signatures are commonly utilized as a fast indexing mechanism for shape retrieval. Effective shape signatures capture some global geometric properties which are scale, translation, and rotation invariant. In this paper, we introduce an effective shape signature which is also pose-oblivious. This means that the signature is also insensitive to transformations which change the pose of a 3D shape such as skeletal articulations. Although some topology-based matching methods can be considered pose-oblivious as well, our new signature retains the simplicity and speed of signature indexing. Moreover, contrary to topology-based methods, the new signature is also insensitive to the topology change of the shape, allowing us to match similar shapes with different genus. Our shape signature is a 2D histogram which is a combination of the distribution of two scalar functions defined on the boundary surface of the 3D shape. The first is a definition of a novel function called the local-diameter function. This function measures the diameter of the 3D shape in the neighborhood of each vertex. The histogram of this function is an informative measure of the shape which is insensitive to pose changes. The second is the centricity function that measures the average geodesic distance from one vertex to all other vertices on the mesh. We evaluate and compare a number of methods for measuring the similarity between two signatures, and demonstrate the effectiveness of our pose-oblivious shape signature within a 3D search engine application for different databases containing hundreds of models     

一种RSA算法之数字签名系统的快速实现方案

不同于常规的二进制幂模算法，该文采用一种更快速有效的滑动窗口法来实现幂模运算，同时结合Montgomery算法和中国剩余定理相结合来实现RSA签名，并给出了签名和验证的流程图。实验结果表明，以1024bit签名为例，采用滑动窗口算法比采用二进制算法要快22．3％；而综合采用滑动窗口和montgomery算法结合中国剩余定理，一次1024bit签名仅需28ms。     

姓名字在线签名与非签名书写的可区分性研究

对姓名字在线签名与非签名书写的区别进行了研究.采集了多位实验者姓名字的在线签名的书写数据和混于文本中的书写数据,将这两组数据看成是两个类,采用动态时间规整(DTW)算法,以位移信号作为特征向量,计算了两个类的类内距离和类间距离,得到姓名字在线签名写法的差别小于非签名写法的差别小于签名字与非签名字之间写法的差别.实验结果表明,该方法具有较强的稳定性和识别性能好的优点.