理性控制下的形式推导与生成——特拉尼法西斯宫的形式解读

该文以特拉尼理性主义设计为出发点,结合特拉尼的人生经历、建筑思潮及时代背景,追溯法西斯宫创作的构思来源,并根据最终方案确定整个修改历程,运用形式推导与生成的方法结合透明性对法西斯宫进行解读。探寻理性控制下空间与流线、建筑与环境、统一与差异背后蕴藏的几何关系,推敲建筑形体及建筑内外每一细节的生成依据,剖析古典主义与现代主义设计手法的完美结合,以期完整还原法西斯宫的设计过程,探索特拉尼用传统和现代构筑的世界。

若干算法程序的形式化推导与生成技术研究

PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于形式化证明的求解算法问题的递推关系;并在此基础上,自然地导出循环不变式.在得到简短、易于理解、高可靠性的Apla算法程序之后,通过转换工具自动生成Java,C++等可执行程序.

最小生成树算法的PAR方法形式化推导

采用PAR方法通过功能归约变换,形式化推导出可读性好、效率高的递推的最小生成树算法,简化了算法程序设计和正确性证明的过程,有效提高了算法程序设计自动化、规范化的程度及其正确性。该文给出的相关算法在PAR平台通过自动转换系统转换成可执行语言程序并运行通过。

Huffman算法程序的形式化推导

使用PAR方法形式化推导了解决最优编码问题的Huffman算法。推导过程充分利用最优编码树的特性,在对原问题进行分划归约为子问题时,引入一个新元素来取代原来的2个或多个元素,使用一套接近数学语言的抽象记号表示集合、二叉树等,推导过程简洁且能生成正确的算法。该Huffman算法能在PAR平台上通过自动生成系统转换成可执行语言程序,并正常运行。

算法及其时间复杂度可同步形式化推导的方法

对在长期的算法研究中提出的PAR方法和PAR平台引入时间谓词加以扩展,不仅可以形式化推导出顺序查找和二分查找问题的算法程序,而且这两个问题关于时间复杂度的递归方程式也可同步且自然地推导得到。这为开发并验证高效率的算法开辟了一条新途径。

序列折半划分问题的形式化推导

形式化推导是在程序正确性证明理论下所进行的程序开发,最终得到完全正确的算法程序。针对序列折半划分问题,现有的形式化推导方法将推导与证明交替进行,推导过程繁琐且大多无法直接获得可执行程序。为解决上述问题,提出了一种新的序列折半划分问题的形式化推导方法。该方法基于分划递推的核心思想,应用规约变换技术对问题规约进行变换并严格保证一致性,使得在推导过程中无需交替证明,进而导出递推关系式并得到高可靠性抽象算法程序Apla,最终通过转换工具自动生成可执行程序。实现了从程序规约到具体可执行程序的完整程序求精过程。以2个序列算法为例,验证了该方法的有效性和可行性,对相关问题的形式化推导具有指导意义。

算法的形式化推导与基于Isabelle的自动化验证

可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化验证,避免了手工验证过程繁琐和易出错等问题.研究表明:基于递推关系的算法形式化方法不仅可以提高开发算法的效率,而且通过数学变换保证推导过程的正确性,从而有效保证了算法和程序的正确性.

3个变形背包问题的形式化推导

在对0-1背包问题的若干变形问题进行深入研究的基础上,使用二进制数组的方式形式化描述了几种背包问题的程序规约,通过程序规约变换技术获取问题求解的递推关系,给出了3个变形背包问题的算法推导过程,有效保证了算法程序的可靠性,并可将采用的推导方法在子集和问题、船装载等问题中加以推广应用.

研究汉语韵母拼合顺序的形式化推导方法

本文依照陆丙甫先生提出的形式化推导方法,对汉语普通话的韵母拼合顺序进行了探索,研究发现了韵母拼合顺序的优势序列和劣势序列,并用"音响顺序原则"进行了的解释。

PAR平台从规约出发的算法推导与自动生成

简要介绍PAR方法及其支撑平台,使用PAR方法及其平台从规约出发形式化推导并生成了两个典型的算法程序。PAR方法及其平台使用一阶谓词逻辑表示功能规约,分划与递推来进行算法形式推导,各种转换系统来自动生成算法程序。这显著地提高了算法程序的正确性和开发效率,也有助于深刻地理解算法设计思想。

在工科数学教学中贯彻形式逻辑分析思想的实例

逻辑思维能力是按照严谨的形式逻辑分析问题的能力,即所谓的逻辑分析。本文对在工科数学教学过程中贯彻逻辑分析、对如何分析问题以及简化问题,使工科数学中的难点重点变得易于理解进行了具体的探讨,也贯彻了高等数学是分析数学的思想。

形式化开发若干组合数学问题的算法

计算机科学的核心内容是使用算法处理离散数据,组合数学的重要性日渐凸显.使用形式化方法PAR开发了两个组合数学问题的算法,形式化推导过程为问题求解提供了思路,自然地引进了算法程序中用到的变量,清晰地展示了算法程序的设计过程,最终可得到简洁、易理解、可靠性高的算法程序.对形式化方法开发组合算法做了积极的探索,有利于促进组合算法设计自动化的研究及形式化开发方法的推广应用.

三个经典数学问题的形式化开发

计算机科学最高奖图灵奖获得者Knuth指出,算法是计算机科学的核心。算法的设计和理解对开发高效、正确的软件至关重要。本文选取平方数问题、几何级数求和问题和多项式求值这3个经典数学问题,使用支持算法程序形式化的PAR方法和PAR平台,从待求解问题的精确功能描述出发,使用PAR方法和PAR平台的推理和变换规则,经过一系列等价变换,最后得到正确的算法程序。这一系列形式化推演的过程揭示了这3个经典数学问题的奥妙,事实说明PAR方法和PAR平台在算法程序设计过程中可以发挥更大的作用。

英汉语SOV结构的推导研究

受特征核查的驱动,英汉语中的SVO是在SOV基础上的推导。英语中核查是受语义无解特征所驱动;汉语中动词的提升是受时态功能词T的驱使,T的强弱分别推导出SVO和SOV两种句法结构。

一种基于程序正确性证明理论的程序开发方法

程序的形式推导方法是一种基于程序正确性证明理论的程序开发方法，它使得程序的开发和证明同时进行，程序开发完成的同时其正确性亦得以保证。以两个问题的程序开发为例说明了程序的形式推导方法的使用。

一类0-1背包问题算法程序的形式化推导

0-1背包问题是经典的组合优化问题与NP完全问题,具有重要的应用价值与理论意义.本文使用PAR(Partition and Recurrence)方法形式化推导了0-1背包问题的高效动态规划算法程序.通过类比分析,该问题的若干变形问题的算法也可推导得到,算法通过PAR平台的自动生成系统转换成可执行语言程序并运行通过,保证了该类0-1背包问题算法的正确性和可靠性.本文主要的贡献是将PAR方法推广到能处理带约束条件的组合优化类问题,大大扩展了PAR方法的应用范围,为形式化开发高效高可信组合优化类算法开辟了一条新途径.

分划递推法在Hanoi塔问题上的应用

采用分划递推法通过功能归约变换,形式化推导和证明H ano i塔问题中圆盘的移动规律,从而推导出结构清晰、可读性好、效率高、占用存储空间与圆盘个数无关的非递归算法,算法比较分析地显示出形式化推导在获得高效和正确性的算法程序中的作用.相关算法在UN IX平台下用C语言进行实现.

PAR在数学算法中的应用

针对算法走进高中课堂的现状,提出使用PAR作为高中学习算法开发的主要平台,通过PAR形式化推导实现多项式和素数两个经典数学问题,表明PAR具有良好的数学和程序设计语言透明性,得到算法简短易于理解的同时也可以同时保证算法的正确性,理论分析和试验表明,PAR是学习算法开发的一个有效平台。

管理过程中的理解问题

当代，处在信息文明的条件下，管理过程越来越取决于接受信息的适应性。由于管理是一个目标明确的，按计划进行的过程，是一个不断进行协调并自觉加以组织的过程，通过这一过程，可以在花费最少的人力、资源和时间的情况下取得最大的效益。因此可以这样推论．对任何过程所进行的管理都是对所获取的信息做出的回答。不严格地说，也可以把管理过程想像为主体与客体的信息反馈过程。问题在于管理是认识活动循一个组成部分，但它不能仅仅局限于对出现问题的情况、对管理的任务，手段和客体进行记录，它还应当包括主体立场的“主观现实”。对事件做出的相应反应取决于主体对所发生的事件的理解。因此，对某一过程进行管理又是理解的一个组成部分。当代对“理解”这一概念的定义又可划分为两个流派。第一种流派的主论依据就是那种普通的，习惯的看法，即认为理解某一客体，也就是掌握了客体的涵义。根据这一思想得出合乎规律的结论，即只能够理解那种在接受理解过程之前就已经具有某种涵义，因而也就具有某种标识性特征的事物。这里重要的不是它的自身，而是别的什么事物的表现。一个明显的例子就是语言表述。第二种流派则把理解视为一种诠释，也就是说用形式推导的原始符号来确定它的含义，由此，这种推导的?

有关PAR在数学算法之中的应用探析

目前在高中课堂中,算法的应用也比较多,本文主要提出PAR作为高中阶段对算法学习的基础平台,对素数及多项式两个经典数学问题通过PAR形式化推导进行实现,说明PAR具有较好的程序设计及数学语言的透明性,其算法简单,容易理解,很大程度上也保证了算法的正确性,通过理论和试验表明,PAR是一种数学算法学习的有效平台。