基于形式演算和不变式验证的可信算法程序构造

The paper presents a formal and practical approach to dependable algorithm development. First, starting from a formal specification based on the Eindhoven quantifier notation, a problem is regularly reduced to subproblems with less complexity by using a concise set of calculation rules, the result of which establishes a recurrence based algorithm. Second, a loop invariant is derived from the problem specification and recurrence, which certifies the transformation from the recurrence based algorithm to one or more iterative programs. We demonstrate that our approach covers a number of classical algorithm design tactics, develops algorithmic programs together with their proof of correctness, and thus contributes fundamentally to the dependability of computer software.     

基于B方法的弹道计算机程序设计技术

针对任务关键性的武器装备控制领域，选用B方法来设计通用弹道计算机程序，显著地提高了软件的质量和可靠性。在开发过程中，利用抽象机机制对基本弹道计算机进行建模，并通过逐步精化的方法扩展弹道计算机功能，从而有效地控制了弹道计算参数之间的复杂关系，依赖不变式技术形式化地保证了软件运行时的安全性，并使得生成的程序具有良好的重用性和可扩展性。     

基于DSL的装备保障领域建模

基于领域专用语言构建了装备保障领域的元模型,描述了实体、关系、行为、约束、流程等基本要素,在该模型中,二次开发人员能够方便地对该领域的各类软件系统进行建模,并通过模型精化来自动生成最终的可执行系统。实验证明,该模型是有效的。     

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

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

基于SPEC#的功能性冗余软件开发

软件的功能性冗余能够有效提高计算机系统可靠性和安全性.研究了SPEC契约机制,分析了如何通过这些机制来实现输入输出域控制,主动冗余和故障恢复等软件功能性冗余的方法和手段,并总结了软件开发过程中应用契约设计和冗余技术的若干准则和建议.这种基于契约的冗余技术能够显著地提高软件的可靠性、可维护性和可测试性,进而提高软硬件系统的整体可信性水平.     

使用SPEC#开发高可靠性的算法程序

概要介绍了SPEC#的基本特性;使用SPEC#开发了若干典型的算法程序,利用该语言中的契约机制来形式化地描述前置条件、后置条件、对象不变式等程序规约,从而显著地提高了程序的可读性、可靠性和可维护性,有助于软件自动化水平的提高。     

．NET数据库应用程序快速开发的方法与实现（上）

讲解基于．NET平台和c#语言开发数据库应用程序的过程和方法。以一个销售客户管理系统为例,详细解析如何实现从数据库模型到对象系统、再到用户界面的平滑过渡,帮助读者快速掌握三层体系结构的数据库应用开发方法。     

．NET数据库应用程序快速开发的方法与实现（下）

介绍．NET Framework中的源代码模型库CodeDOM,并讲解如何使用相关技术自动生成．NET数据库应用程序代码,包括存储过程、业务对象类、数据访问对象类,以及用户界面。这种开发方法不仅能够减少数据库应用开发中的大量重复操作,也有助于规范程序结构和代码风格。     

使用SPEC#开发高可靠性的物流信息系统

结合形式化软件开发方法和面向对象的方法学，使用SPEC#开发物流信息管理系统，利用该语言中的前置条件、后置条件、对象不变式等形式化机制显著地提高了软件的可读性，可靠性和可维护性。系统地总结了分析、设计和编码阶段的经验和问题，提出了应用SPEC#进行契约式程序设计的一组原则和建议，并分析了该语言存在的不足和改进策略。     

多Agent 主从粒子群分布式计算框架

面向大规模复杂优化问题,提出了一个基于并行粒子群优化的分布式Agent计算框架.框架中使用一个主群(master swarm)来演化问题的完整解,并使用一组从群(slave swarm)来并行优化一组子问题的解,主群和从群通过交替执行来提高问题的求解效率.采用异步组结构,主群/从群中的各类Agent共享一个解群,并通过相互协作,对解群进行构造、改进、修补、分解和合并等演化操作.该框架可用于求解复杂的约束多目标优化问题.通过一类典型运输问题上的实验,其结果表明,所提出的方法明显优于另外两种先进的演化算法.