【摘 要】
：
终结共代数上的互模拟是等价关系,这一性质为对象的行为等价提供了一种基于共归纳原理的证明方法。首先,利用共代数给出面向对象方法中的抽象类、类和对象的形式化描述,其中
【机 构】
：
中山大学信息科学与技术学院,华南理工大学计算机科学与工程学院
【基金项目】
：
国家自然科学基金项目（60673122）, 广东省自然科学基金项目（8151030007000002）资助
论文部分内容阅读
终结共代数上的互模拟是等价关系,这一性质为对象的行为等价提供了一种基于共归纳原理的证明方法。首先,利用共代数给出面向对象方法中的抽象类、类和对象的形式化描述,其中抽象类被定义为一个包含方法和断言声明的类规范,类被定义为满足类规范的共代数,类的各个对象看成是共代数状态空间上的元素,而对象中方法的各种行为结构则通过强Monads进行参数化描述;接着,利用类规范的终结共代数给出对象行为等价关系的证明方法以及在各种不同Monads结构下的终结共代数语义;最后,通过实例说明如何利用PVS工具对研究结果进行验证。
其他文献
机载航空电子系统设计采用综合化系统体系结构,可实现计算系统及其计算资源和计算设施的＂物理集成＂;以及机载嵌入式软件系统的＂功能集成＂;提供对系统计算功能的动态配置管理和实
访问控制模型定义了安全系统访问控制的整体框架。现有的访问控制模型大多是静态授权模型,尽管可以通过扩展来实现局部动态性（比如可以通过定义条件来实现角色的临时激活等）,但
给出了广义随机着色Petri网（GSCPN）和基于GSCPN的Web服务模型,实现了Web服务QoS和数据的表示,并给出了基于GSCPN的服务组合运算方法。用模型的层次化方法来降低模型的复杂性,一
针对车牌识别系统中由于低质车牌首字符特征提取困难而导致车牌首字符识别率不高的问题,提出了一种新的车牌汉字特征提取方法。该方法首先对车牌首字符的二值图像进行网格化处理,并对每一块网格区域提取字符笔画所在像素的占空比、散度和质心3个特征分量,接着将提取到的所有的特征向量用支持向量机分类器进行训练,最终可以得到一组鲁棒性很强的分类器。实验结果表明,该特征提取方法与支持向量机分类器结合可以较大地提高车牌首
针对目前复杂系统多路径覆盖测试用例生成方法较少的问题,提出一种新的基于复杂系统的多路径覆盖测试用例生成方法。首先改进遗传算法,在种群进化中对父代选择、个体进化的学
可编程逻辑器件（PLD）在电子设备中广泛应用,其安全缺陷检测已成为信息安全领域中一个富有挑战性的课题。通过分析PLD安全缺陷的存在形式,提出了基于状态转移图的安全缺陷检测方
在分析多处理机调度问题的基础上,提出了α-平坦的概念,并将其引入到多处理机调度问题中;基于此,提出了一种新的基于α-平坦的求解多处理机调度问题的算法。算法首先对作业集
标准的近似支持向量机（PSVM）用求解正则化最小二乘问题代替了求解二次规划问题,它可以得到一个解析解,从而减少训练时间。但是标准的PSVM没有考虑数据集中正、负样本的分布情况
介绍了几种常用的网络数据安全传输的技术，在此基础之上，提出了信息安全传输系统的设计思想。在此系统中，通过使用开源的EJBCA系统完成对数字证书的管理。客户端采用CAPICOM技术
频繁模式挖掘可以发现数据中频繁出现的模式，是关联规则挖掘的重要步骤。并行频繁模式算法将其应用到并行环境中，以对海量数据进行挖掘。在Apache软件基金会的Mahout项目实现的