孙永强著名计算机科学家和教育家

《孙永强著名计算机科学家和教育家》由会员上传分享，免费在线阅读，更多相关内容在应用文档-天天文库。

1、孙永强著名计算机科学家和教育家孙永强著名计算机科学家和教育家2010-05-1523：27孙永强著名计算机科学家和教育家孙永强，浙江嘉善市人。1955年毕业于交通大学电力系，历任清华大学讲师，上海交通大学副教授、教授。曾担任国务院学位委员会学科评议组成员。从事计算机科学研究50余年，涉及编译原理、函数程序代数理论、软件自动验证、重写技术等多个软件技术分支，在国内外重要刊物和会议发表论文百余篇，培养计算机软件与理论博士30余名，获得国家自然科学奖等多项奖励，是我国著名的计孙永强教授算机科学家和教育家。辛勤耕耘软件杏坛称巨擎1955年毕业于上海交通大学的孙永强被分配到了

2、清华大学工程力学数学系，开始从事计算机科学的教学和研究工作，那时中国的计算机事业刚刚起步，为了配合国产计算机硬件系统的开发，孙永强将研究方向定位为计算机软件。当时算法语言和编译技术的材料还很缺乏，年轻的孙永强带领学生每天扑在实验室，凭借简单的指令手册，日夜调试程序，历经多年攻关，终于在1964年实现了我国第一代编译系统：运行于国产911机器的ALGOL60编译器。由于911机器只有数KB的内存，程序编译慢，影响了软件的开发速度，经过思考，孙永强大胆提出了分趟编译策略，也就是将编译分成词法分析、语法分析、中间代码生成、优化和目标代码生成等若干阶段，每个子任务完成的阶段

3、性输出存于外存，再在下一个阶段导入内存，借此有效克服了当时计算机内存较小所带来程序编译困难的问题，该技术后在DJS-5机器上加以优化改进，被浙江大学等国内十余家单位采用。为了推广编译技术，孙永强主持编写了《程序设计自动化基础》(科学出版社，1975年)一书，促进了国内早期程序语言编译器的构建，之后又与陈火旺教授和钱家骅教授一起撰写了《程序设计语言编译原理》(国防工业出版社，1978年)一书，该书作为计算机专业教材，二十余年来数度再版，赢得赞誉无数，获得了国家级优秀教材一等奖，推动了计算机编译技术的发展。1974年孙永强回到了上海交通大学，他的兴趣也转向了计算机软件理

4、论，他开始思考计算机程序的性质，研究借助程序性质的推导就可以了解程序的执行是否满足给定规范的方法。在他苦苦思索之际，美国的J.Backus教授在图灵奖演说中提出了函数程序代数理论，在该理论中，程序可以看成数学中的函数，而程序的性质可以通过代数的方法推导而出。看到Backus的演讲报告，孙永强立即组织了一个研究组对其可行性进行验证，不久研究组就根据函数式语言FP的代数性质得到了一些重要的基本展开定理，获得了一系列线性方程(组)、非线性方程(组)以及拟双线性方程展开式的求解方法，使用该方法大多数以递归形式表达的函数程序只要根据它的方程形式就可以直接获得相应的时、空效率较

5、高的等价程序，这个研究成果可广泛应用于程序转换、正确性验证等领域。该工作很快就被列入国家自然科学基金资助的重大科技成果，孙永强也于1987年获得了国家自然科学三等奖。研究成果的发表博得了国外著名学者的高度赞赏，FORTRAN语言及FP语言创始人、美国国家科学院院士J.Backus对这项工作非常感兴趣，邀请孙永强赴美访问交流。在访问卡内基-梅隆大学期间，孙永强大胆地将此方法应用于脉动阵列机的验证，并在回国后完成了以FP作为描述语言的多层次的VLSI(超大规模集成电路)自动综合和设计系统。该系统能将一般的典型算法通过上述代数理论的推导自动导出对应的脉动式阵列算法，生成逻

6、辑线路图并绘出CMOS版图。如此能够完整地、多层次地完成一个VLSI自动设计系统，在当时国际上尚属鲜见。1991年在上海交通大学举行的中德电子周活动上，孙永强将这一系统做了演示，受到德国著名计算机科学家Hotz教授、B.Mahr教授及其它计算机科学家的高度赞赏，他们回国后立即写信邀请孙永强赴德介绍此项技术。此应用成果于1993年获国家教委科技进步三等奖，被国家自然科学基金会列为优秀科技成果。在研究函数程序性质取得成果的同时，孙永强在考虑这样一个问题：函数语言在工程实际中应用较少，研究组取得的成果是否可以推广到一般语言编写的程序?是否可以自动判别一个使用一般的算法语言

7、，如FORTRAN，编写的程序满足某种给定的规范?经过数年的研究和实践，一个使用自行开发的定理证明器，以自上向下方式进行程序综合的国内首个用于程序验证的实验系统产生了，该工作完善了Boyer-Moore方法，突破了著名学者Z.Manna关于程序综合必须结合归纳和消解二种方法的论断。与国外同类系统相比，该系统具有可自动生成断言、能处理交错嵌套循环等特点。物理学、数学系的老师纷纷拿着自己开发的FORTRAN程序前来一探究竟，结果证实了系统确能自动验证用FORTRAN语言书写的具有整数类型数据处理的程序。此项研究成果于1985年获得国家教委科技进步二等奖。在研究程序性