框架时序逻辑语言MSVL中面向对象机制的实现

针对目前时序逻辑语言存在框架问题、缺少面向对象机制、形式化程度过高等不足,提出了框架时序逻辑语言MSVL,包含新的框架操作符、等待语句和非确定的选择语句等技术,并且能够支持面向对象的程序设计．基于正则形和正则图,给出了MSVL解释器的实现方案．并发访问共享资源的实例表明,MSVL比其他时序逻辑语言更接近高级语言,并且解释器的实现方案是切实可行的．     

面向对象系统的时序逻辑描述

针对面向对象系统,定义了一种基于时序逻辑的形式化规约语言.它不仅支持对面向对象思想中重要概念,如类、对象、继承等的描述,而且支持对面向对象系统的时序属性的描述,如类的状态之间的转换,类中某些属性必须一直满足的约束条件等.能够实现对系统属性的推理也是用这种语言描述的系统的动机之一.通过对一个局域网用户访问控制实例的描述来实现对这种形式化规约语言的直观阐述与理解.     

面向对象的逻辑程序设计

逻辑程序设计是通过使用逻辑规则来解决问题，面向对象的程序设计是通过定义与使用对象的方法来解决问题。逻辑程序设计使开发者集中精力于问题而面向对象的方法提倡代码重用。面向对象的逻辑程序设计可结合这两种设计的优点。先简单介绍prolog程序设计，然后重点论述面向对象的Prolog程序设计方法。     

框架投影时序逻辑程序设计语言中的指针

针对框架投影时序逻辑程序设计语言Framed Tempura,提出了一种形式化指针及其实现的新方法.该方法扩展了投影时序逻辑,基于名字常量给出了指针引用和反引用的形式化定义,再使用框架操作符和极小模型,给出了指针在投影时序逻辑的可执行子集Framed Tempura中的实现方法．原地逆置单链表的实例说明该方法是切实可行的．     

区间时序逻辑的模型检查

为了检验标注有限状态自动机描述的系统是否满足某个区间时序逻辑公式刻画的性质,定义了一套转换规则．利用这些规则,可以构造一个chop-自动机,该自动机接受的语言恰是所有满足这个区间时序逻辑公式的模型的集合．同时,定义了一套转换规则把一个chop-自动机转换为一个标注有限状态自动机,使得它们接受相同的原子命题序列集．这样,区间时序逻辑的模型检查问题就等价地转换成了很容易解决的两个标注有限状态自动机的语言包含问题．     

进位保留加法器的命题投影时序逻辑组合验证

为保证硬件设计的正确性,提出了对硬件设计组合验证的新方法．该方法在命题投影时序逻辑的统一框架下,实现对硬件系统行为的建模,对所期望性质的形式化描述,并利用命题投影时序逻辑合理且完备的公理系统对系统性质进行验证,从而证明硬件系统满足期望的性质,保证设计的正确性．进位保留加法器的验证实例说明了该方法的可行性．     

支持Stutter-不变性的命题区间时序逻辑

为了将命题区间时序逻辑(PITL)应用于组合验证,并降低组合产生的状态爆炸风险,提出了支持Stutter-不变性的命题区间时序逻辑PITLst.PITLst继承了PITL的结构相关性,可表达所有PITL能够表达的Stutter-不变性质,支持模块抽象约简系统规模,降低了状态爆炸风险.自动加油站模型的组合验证实例表明,PITLst可有效应用于组合验证技术.     

在扩展PROLOG中函数和面向对象的程序设计

论述了逻辑、函数和面向对象程序设计语言的差别和联系,提出了PROLOG语言的元级扩展,讨论了在此系统中函数和面向对象程序设计的实现方法.从程序设计方法学的观点看,此系统展现了多种程序设计风格,是逻辑、函数和面向对象程序设计模式的结合.     

面向对象工程数据库的自然语言查询

通过面向对象的分析，将面向对象的查询转换成关系语义的查询，针对自然语言查询的特点，采用Ｍｏｎｔａｎｇｕｅ语义法进行语义分析，提出了描述自然语言查询语义的类关系代数表达式以及类关系代数表达式的确定化方法，该自然语言查询接口具有容易修改，通用性好的优点。     

面向对象的并发程序设计语言

将并发机构引入Ｃ＋＋，本文提出了面向对象的并发程序设计语言ＣｏｎｃｕｒｒｅｎｔＣ＋＋，揭示了类、对象及进程之间的关系。     

论逻辑语言的现代化转向

传统的逻辑语言具有缺乏一致性、准确性和全面性的特点,因而在应用中受到较大的局限。而现代化的逻辑语言不仅对语言内容与语言形式作出区分,还对对象语言与元语言,以及语法学、语义学、语用学等语言层次上作出区分。因此,对逻辑语言的现代化转向的重新追溯和审视,将使人们更易于理解现代逻辑语言与传统逻辑语言的差异,并且对于逻辑学的发展和应用具有深远的理论意义和实践意义。     

一种OODBMS的直观对象查询语言的研究与实现

论述了一种面向对象的数据库管理系统的直观对象查询语言。这种基于图形的查询语言可支持图表式查询语言的定义和说明,因此这种语言既有基于本的结构查询语言的表达能力,也具有基于图形查询语言的直观性。     

一种网络消息逻辑描述语言

在分布式网络程序的运行过程中,网络消息的传递具有一定的规律和逻辑性.这种逻辑如果与设计者的预期行为不相符合,则说明系统在运行过程中出现了异常模型.文中重点分析了消息的传播模式,提出一种消息逻辑描述语言LT来描述这种消息之间的逻辑关系.此语言为脚本语言,不需要编译,直接解释为二进制模块运行.此逻辑语言具有简明,实用,可扩展的特征.     

扩展命题区间时序逻辑公式可满足性判定算法

针对扩展命题区间时序逻辑由于缺少验证算法因而不能用于模型检测问题,提出该逻辑的可满足性判定算法.首先,正则形子算法把带星算子或不带星算子的扩展命题区间时序逻辑公式翻译为其正则形公式;然后,正则图子算法根据正则形公式构造公式的正则图模型;最后,判定子算法在正则图上判定公式的可满足性.如果在正则图上直接加上接受条件,即可得...     

从语言到逻辑——范畴类型逻辑序列

范畴类型逻辑序列是近30年来语言和逻辑交叉研究的重要学派,是对自然语言的计算机处理影响很大的形式语义理论。该理论把自然语言的生成毗连看作是范畴的运算和推演,据此构造自然语言的语句系统,并确立直接或间接的语义解释。另一方面构造范畴推演的逻辑系统,并配备可能世界的模态语义解释。范畴类型逻辑的研究成果可以直接应用于自然语言的计算机信息处理,也可以应用于汉语的形式语义理论研究。     

逻辑程序设计语言HPROLOG1的控制策略

逻辑程序设计语言HPROLOG是一种类prolog语言,它将主要作为一种推理数据库的查询语言.HPROLOG1是HPROLOG的一个基本子集,它具有逻辑程序设计语言prolog的基本功能和特点.本文将主要介绍在实现逻辑程序设计语言HPROLOG1中所采用的一种合一算法,目标栈的回溯控制方式以及循环检测的有关理论及其算法.     

用于描述和验证数字电路的一阶间隔时态逻辑

提出一种新的时态逻辑——一阶间隔时态逻辑（ＦＯＩＴＬ）,它是扩充了间隔时间算子的一阶时态逻辑。它能精确地描述数字电路的时间特性,支持连续和离散的时间结构并能对时间信息进行推理。本文给出了ＦＯＩＴＬ的基本框架,并对其进行了验证。     

一种基于时态逻辑的有限状态系统验证方法

ＬＰＴＬ与自动机之间有着紧密的联系,结合ＬＰＴＬ语义和语法,提出一种从ＬＰＴＬ公式导出Ｂｕｃｈｉ自动机的方法。导出的Ｂｕｃｈｉ自动机所接受的语言准确地表达了ＬＰＴＬ公式所描述的特性。从而把由ＬＰＴＬ公式描述的系统设计规范的验证问题转换成检验Ｂｕｃｈｉ自动机的包含问题。