论文部分内容阅读
计算机科学是研究算法的科学，而且计算机所处理的对象大部分是离散的数据。组合数学是研究离散对象的科学，正因为有了以组合数学为基础的组合算法，才使人感到计算机好像是有思维的。然而，许多组合算法程序设计教材上没有对算法程序进行形式化推导，不能给出从需要求解的组合数学问题到具体算法程序的设计过程，这严重影响了算法设计者对算法本质的理解和算法设计能力的提高。 薛锦云教授在多项国家级课题和省部级项目资助下，提出并解决了一系列关键技术，形成了支持软件形式化和半自动化的PAR方法及其支撑平台(PAR平台)。在研项目国家自然科学基金课题“基于PAR方法的算法设计形式化和自动化研究”涉及软件开发形式化和自动化、算法程序形式化推导和证明研究等内容。通过使用PAR方法对组合数学问题进行形式化推导，不但能很好地解决上述问题，而且从逻辑上保证了算法程序的正确性。由于PAR方法蕴涵了许多数学思想并拥有强大工具和良好的开发环境，用它作为组合数学问题的算法程序设计方法可避免在现有各种方法之间做出选择，可使其中相当多的创造性劳动转变成机械劳动，有效提高算法程序设计自动化、规范化的程度。 本论文主要完成了以下几项工作：分析当前形式化需求，介绍几种典型的软件形式化方法，研究Smith教授领衔的学术队伍研发的软件开发系统Specware；介绍PAR方法的关键技术、开发步骤及其语言等，将PAR方法与典型形式化方法进行比较，并将其与软件开发系统Specware进行比较；分析PAR方法的特点，研究它在组合数学问题上的有效性；用PAR方法开发多个典型组合数学问题实例的算法：字符串长度方案数，错排方案数，最大和，最长公共子序列，最小生成树，背包问题等，并对PAR方法在组合数学问题实例上的开发步骤进行了分析和总结。 在本论文研究过程中，进行了多方面创新：研究了Specware的形式化理论基础、开发步骤、开发原则等，并将其与PAR方法进行了比较；提出PAR方法是解决组合数学问题的有效方法；PAR方法的泛型机制在组合算法开发中的应用：首次在多个组合数学问题实例上运用PAR方法实现从规约到算法的推导全过程，并基于推导过程中获取的直觉经验，研究PAR方法在组合数学问题上的实用性。