基于语法树和程序正确性验证研究_周必水.pdf

第 24卷第 4期　　　 计算机应用与软件 V ol.24 No. 4 2007年 4月　　 ComputerApplications and Sofwt are Apr. 2007 周必水　李　骏　沃钧军 (　 310018) 　　　提出了 一种新的基于语法树的程序正确性验证方法(STM 方法)。 在理论 算法上对方法的实现进行了初步探讨, 并结 合 XM L技术提出了 一套实现这 一方法的切实可行的解决方案。 　　程序正确性验证　语法树　XML PROOF OF PROGRAM CORRECTNESS BASED ON SYNTAX TREES Zhou Bishui　Li Jun　Wo Junjun (Sof twareSchoo,lHangzhouD ianziUniversity, Hangzhou 310018, Zhejiang, China) Abstract　　This paper presented a new m ethod of the proof of p rogram correctnessbased on syntax trees. It exp lored basic problem s in the mi plem entation of thism ethod on theory and algorithm. In add ition, it presented a solu tion to imp lement th ismethodw ith XM L. K eywords　　 roof of program correctness　Syntax tree　XML ();②, 1　　 。 IT, 、。 , , 。 , D-i jk stra:“, 1　STM 。”, 2. 1　 , 。 , 、 , :, , , -, , , : ; -, 1) , “”。 , 。 , , 、 , , 。 , , 。 , , 2)、, 、。 , 。 IT、 3) XM L。 XM L , , (Syntax , 、。 Tree based M ethod, STM )。 1, 2 , , 。 。 C, 。 2　 2　 ( STM 2