程序的形式推导方法

journal6 ›› 2001, Vol. 22 ›› Issue (4): 54-56.

程序的形式推导方法

( 1. 吉首大学数学与计算机科学系, 湖南吉首 416000; 2.吉首大学教务处, 湖南吉首 416000)

出版日期:2001-12-15 发布日期:2013-01-05
作者简介:彭佳红( 1 963 - ) ,女,湖南省江华县人,吉首大学数学与计算机科学系副教授,主要从事程序设计方法学研究.

Formal Derivation Method of Programs

( 1. Department of Mathematics and Computer Sciences, Joshou University , Jishou 416000, Hunan China;2. Dept. of Educational Administration of Jishou University, Jishou 416000, Hunan China)

Online:2001-12-15 Published:2013-01-05

摘要/Abstract

摘要：阐述了形式推导方法的基本理论和基本思想.程序的形式推导方法是一种基于程序正确性证明理论的程序开发方法,它使得程序的开发与证明同时进行. 以实例说明了程序形式推导方法的使用.

关键词： 程序的形式推导方法, 程序规范, 循环不变式, 界函数

Abstract: This paper expounds the basic theory and basic ideas of Formal derivation method of programs. Formal devivation of programs is a developing method of programs based on the proof theory of program correctness. It can make the proof process and the devolopment of the program in progress in the meantime. And this paper illustrates how to use formal derivation of programs.

Key words: formal derivation method of programs, program specification, loop invariant, boundary function

彭佳红, 张军. 程序的形式推导方法[J]. journal6, 2001, 22(4): 54-56.

PENG Jia-Hong, ZHANG Jun. Formal Derivation Method of Programs[J]. journal6, 2001, 22(4): 54-56.