CASL:基于代数规范的几何成型

论文综合论述了代数规范方法在CAD几何成型中的应用[1,2,3]。首先阐述的是代数规范语言的概念,接下来通过引入反射函数,举例说明如何采用CASL语言在其代数性质方面的优点来描述基于n-维通用映射规范的几何成型数学模型。从而形成了高层次的几何成型操作的抽象描述。最后,简单地描述了CASL语言描述的规范到XAML描述的变换实现。

代数规范与对象行为约束

本文研究建立了代数规范和时序逻辑规范的不同语义模型之间的关联,在结构偏代数上解释时序模态词,从而可以利用时序逻辑工具讨论由代数规范所定义的抽象对象的动态行为特征.

多态性构件及其代数规范

可复用构件往往需要引入多态性支持,但是这给构件的形式化定义带来很多困难。采用代数规范系统来定义空间几何实体构件的组织结构及其行为特征,可以有效的支持构件的数据和行为多态性。在多层次的代数规范理论基础上,引入了构件的参数化多态和包含多态,建立了空间几何的实体多态性构件系统,实例表明了系统对于数据和行为多态性方面的有效性。

代数规范说明的基础

代数规范说明是软件与理论计算机科学研究中的一个活跃领域,它对于软件工程与程序设计方法学都有很好的支持,是软件形式化开发研究的一条希望之路。本文是《代数规范说明技术的理论与应用》论文的第一部分,主要介绍数据抽象的思想与抽象数据类型的规范说明。文章从泛代数的角度阐述等式规范说明、初始语义、规范说明的拓广及其一致性与完全性问题。

主动数据库系统的代数规范说明

传统的非线式化的系统描述方法已不能适应主动数据库研究的的需要。本文提出了采用代数规范说明的方法，形式化、结构化地描述规则系统的语法、语义，行为特征，并以此作为进一步分析和研究方动规则的理论基础。

非线性代数规范的直接实现技术

代数规范（ＡｌｇｅｂｒａｉｃＳｐｅｃｉｆｉｃａｔｉｏｎ）是支持软件规格说明和设计的一种有效的方法．代数规范的直接实现技术（将一个代数规范转换为一个程序设计语言的具体实现的技术）是该研究领域的一个主要分支，目前这方面的研究基本上局限于线性代数规范．本文介绍一个实现非线性代数规范的转换过程，从该过程可自然地导出针对不同程序设计语言的转换系统．我们已实现了一个基于Ｐａｓｃａｌ语言的转换系统．

代数规范说明的实现

代数规范说明的实现是代数规范说明支持快速原型枝术的关键。本文介绍了代数规范说明实现的背景,阐述了代数规范说明实现的理论与方法,给出了基于UF-变换的自动实现方法。

代数规范的可计算实现

本文给出代数规范可计算实现的定义,证明了每一个可计算实现都可用特定的三元组来形式描述.在该定理的基础上,可进一步讨论可计算实现的性质.

代数规范描述及其语义的研究

用代数规范描述来描述抽象数据类型的基本思想是用它的标记和特征性质来说明抽象数据类型,它们的性质可用多类逻辑形式来表示,通常为受限的一价逻辑。

一个含有不确定性语言的代数规范说明

本文定义了一个语言L,其允许表达式有负作用并对表达式序列的计算顺序不加规定,这样,在L中,同一表达式序列,因其计算顺序不同而可以有不同的结果,因而其语义模型就不是唯一的,传统的单一模型方法不适于定义L的语义,本文在极大语义的意义下,定义了L的代数规格说明并讨论其模型性质。

自动机及其代数规范描述

本文利用泛代数的思想和方法研究自动机理论，建立了亚群和自动机的方程规范模型，把亚群和自动机定义为这种规范模型的代数。给出了规范代数可识别语言的定义，并讨论了和规范代数的同态及同余之间的关系。

关系网的代数规范说明

将关系网看作一个抽象数据类型,给出了其代数规范说明.这个关系网是它的代数规范说明的一个代数,代数规范说明的任一代数是一个关系网;讨论了关系网在同态下的性质,以及代数规范说明的代数与关系网模式和位置/变迁网的关系。

关系规范代数范畴(Ω,R,E)-alg中自由对象的存在性(英文)

本文给出（Ω，R）－代数直积的概念，证明范畴（Ω，R，E）－alg关于子代数、直积和同态像运算封闭。从而得到该范畴中自由对象的存在性定理。最后讨论关系规范代数约化的概念及其性质。

基于代数式规范的变异测试方法的设计与实现

软件测试是软件工程中保证软件产品质量的重要组成部分。变异测试是一种衡量测试用例集完备性的测试策略,也被用于生成完备的测试用例集。为了提出一种基于代数式规范的新的变异测试方法,为此设计了12类针对代数式规范的变异操作符,对5个代数式规范进行了实验,并进行了结果分析。结果表明基于代数式规范的变异测试方法相比基于代码的传统变异测试方法,生成更少的变异体,也大幅度提升了变异测试的效率。

基于代数-时态逻辑的象形对象语义模型探讨

本文在 "基于代数 -时态逻辑的象形对象研究 "一文的基础上 ,进一步讨论了“基于代数 -时态逻辑的象形对象语义模型”问题 .主要是将基于代数模型和基于时态逻辑模型这两种方法结合 ,通过 OOCPN描述形式 ,对象形对象语义模型进行了探索式研究 .具体包括象形对象标记、象形对象语义解释结构、象形对象语义结构模型结构 ,定义了状态运算符、操作运算符并给出其语义域上的解释 ;提出了可继承属性和可继承操作、完全继承和部分继承等概念 ,并用来刻画象形对象系统中的类结构及继承性 ;在分类结构、组装结构的基础上提出了聚合类结构及分类 -聚合类结构 ;给出了象形对象类类型的代数规范描述 ;给出了有关象形对象系统的公理和定理 ,并用 OOCPN(Object- Oriented ColorPetri Net)对象形对象的继承性、类结构及类变化、重码语义的可能性和有害性等进行了描述 .

基于代数-时态逻辑的象形对象研究

本文首先讨论了国内外有关面向对象方法学、代数规范、时态逻辑的研究现状 ,分析了对象形式化语义研究的不足 .其次 ,分析了几种主要的系统形式化模型和方法 .然后 ,在我们已研究的“计算机甲骨文象形码输入法”的基础上 ,从时态逻辑的角度定义了象形对象及其约束条件 ,定义了面向对象的有色 Petri网 (OOPEN) ,并应用 OOPEN描述了象形对象的层次结构 .最后 ,我们将代数规范与时态逻辑相结合 ,对象形对象的语义基础进行了一些研究 .

基型代数族的积代数

在本文中作者对有关一族ＳＩＧ一代数的积代数的几个问题作了一些讨论，得到了一些重要的结果：指出ＳＩＧ─Ａｌｇ是一个可积范畴，引入了积代数的合同关系和由同态映射及合同关系诱导的合同关系，相应地得到了一些结果，并指出了这些结果适用于ＳＰＥＣ一代数．

一类等式模型类的代数性质

讨论了具有使等式e 有效的子代数的规范代数构成的类的代数性质。

一种通信协议测试序列生成的新方法

本文讨论了一种协议测试的新方法 ,它使用构造类别代数描述通信协议规范 ,然后根据规范中的公理部分生成测试序列。本文以栈规范为例介绍这种方法的应用。并通过与基于有限状态机的测试序列生成方法相比较 ,得出两种方法在一些方面是等效的 ,但在处理状态较多的协议时 ,这种方法有一定的优点。

基于重写技术的程序开发与验证

完整地介绍了一个基于重写技术的程序开发和验证系统 ,重点展示验证子系统的理论、方法和技术 .验证子系统使得系统能自动证明程序和规范中的优化规则及测试等式 ,从而进一步保证程序开发过程的正确性 .验证子系统所采用的主要技术是以成批证明方法和证据测试集为特色的重写归纳方法 .