| 若干算法程序的形式化推导与生成技术研究 |
| |
| 引用本文： | 胡启敏,薛锦云.若干算法程序的形式化推导与生成技术研究[J].计算机研究与发展,2008,45(Z1):148-153. |
| |
| 作者姓名： | 胡启敏 薛锦云 |
| |
| 作者单位： | 1. 江西省高性能计算技术重点实验室,南昌,330022
2. 江西师范大学瑶湖校区计算机信息工程学院,南昌,330022 |
| |
| 基金项目： | 国家自然科学基金
,
国家重点基础研究发展计划(973计划)
,
江西师范大学校科研和教改项目 |
| |
| 摘 要： | PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于形式化证明的求解算法问题的递推关系;并在此基础上,自然地导出循环不变式.在得到简短、易于理解、高可靠性的Apla算法程序之后,通过转换工具自动生成Java,C 等可执行程序.
|
| 关 键 词： | PAR方法 形式化推导 算法程序 递推关系 |
| 修稿时间： | 2007年7月10日 |
Research on the Formal Derivation and Generation Technique of Several Algorithmic Programs |
| |
| Hu Qimin,Xue Jinyun.Research on the Formal Derivation and Generation Technique of Several Algorithmic Programs[J].Journal of Computer Research and Development,2008,45(Z1):148-153. |
| |
| Authors: | Hu Qimin Xue Jinyun |
| |
| Affiliation: | Hu Qimin , Xue Jinyun(Key Laboratory for Computer Science of Institute of Software,Chinese Academy of Science,Beijing 100080)(School of Computer Information , Engineer in Yaohu District,Jiangxi Normal University,Nanchang 330022)(Key Laboratory of High Performance Computing Technology in Jiangxi Province,Nanchang 330022) |
| |
| Abstract: | Based on partition and recurrence, rules of quantifier transformation, new strategies for developing loop invariants, and software transforming tools, a unified formal approach called PAR method gives a new way to develop complicated algorithmic programs. Several typical algorithms are formally derived using PAR method. The derivation can achieve algorithms represented by recurrence relation which has mathmatical transpanrency and is provable. Loop invariants of those algorithms can be educed naturally usin... |
| |
| Keywords: | PAR method formal derivation algorithmic program recurrence relation |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
