1995, 6(12):705-711.
摘要:本文提出一种面向对象软件的形式描述语言JOOSL,用它可描述面向对象软件需求规格、概要设计和详细设计。从描述方法角度看,需求规格和概要设计的描述在很大程度上相同,这就反映了OO开发模型中需求和设计之间的重叠。在这些描述中用抽象方法描述数据和操作;详细设计中确定算法细节和数据的表示。JOOSL 认为对象是一种抽象的状态机,继承是行为特性的共享。
1995, 6(12):712-718.
摘要:本文介绍了一种以圆头体字形特征为基础,使用覆盖规则自动生成一种琥珀体曲线轮廓汉字字形的方法.
1995, 6(12):719-727.
摘要:XYZ/E的好处之一在于高级和低级的说明能够在同一框架下表示,因而使得软件的说明和实现变得容易一些.在这同时,开发验证工具以验证不同层次的说明是否满足所期望的关系是很重要的.谢洪亮等同志曾研究过XYZ/SE程序的验证规则.本篇文章增加了有关使用数组、过程说明和过程调用的规则.同时着重说明XYZ/SE程序验证的自动化方面的问题,且实现了一些化简验证条件的规则.
1995, 6(12):728-733.
摘要:随着远程通信需求的不断增长和我国公用分组交换数据网的扩容,实现微机UNIX环境下的分组交换网访问协议软件,使我国成千上万的微机用户实现远程通信已迫在眉睫。本文在简单介绍了基于STREAMS机制的通信软件开发的一般思路之后,着重叙述了基于STREAMS机制的X.25分组交换网协议访问软件的设计与实现.并对基于STREAMS机制的通信软件开发方法作了简单评价.
1995, 6(12):734-741.
摘要:本文给出了HOS方法学中基本控制结构JOIN、INCLUDE、OR和复合控制结构COJOIN、COINCLUDE及COOR的语义构造规则.以此为基础,提出了一种层次武功能理解方法,并讨论了其在HOS规格说明的语义验证和复用方面的应用.
1995, 6(12):742-750.
摘要:本文将P.Enjalbert和L.FarinasdelCerro提出的模态归结推理方法推广到命题模态逻辑K4和D4系统,建立了K4逻辑的归结推理RK4;D4逻辑的归结推理R D4,分别证明了RK4和RD4关于K
缪淮扣 , John McDermid , Lan Toyn
1995, 6(12):751-760.
摘要:Z规格说明中的初始化定理的证明是对基于状态的规格说明的一个标准的检查.本文给出了一个证明初始化定理的过程,该过程可自动地构成证明的证据.作为实例,我们用该过程证明了两个初始化定理.