（计算机应用技术专业论文）基于xml的程序设计自动批改的研究.pdf

摘要 随着计算机技术特别是网络技术的迅速发展及其在教育领域 中的广泛应用，c a i ( c o m p u t e r a s s i s t e di n s t r u c t i o n ) 和e l e a r n i n g 得 到了飞速的发展，促进了无纸化测评技术的研究。采用无纸化测 评系统对学习对象的学业水平进行科学公正的测评，一直是高等 教育推进教学改革的难点和重点之一。本文对基于局域网的无 纸化测评系统中程序设计的自动批改问题进行了研究和论述， 在智能化教学的理论与实践方面作了有益的尝试。 本文对程序设计自动批改问题进行了剖析，借鉴了程序正确 性验证领域的已有成果，提出了分级别、加权进行程序设计自 动批改的思想，分别从程序结果、词法和语法分析、功能模块、 变量变化曲线和人工检查五个级别对程序的正确程度进行了描 述，并着重探讨了词法分析、功能模块匹配和变量变化曲线匹配 的算法及实现。为了实现系统的可扩展性和可重用性，考虑到 x m l 的扩展性和可标记性，本文采用了标准的中间语言x m l 对源程序进行描述。使用基于d o m 的x m l 解析器m s x m l ，得 到x m l 文档的树状结构图，进行了功能模块匹配。同时采用变 量的变化曲线来反映数据流的变化，提出了变量的变化曲线 验证方法。从而实现了无纸化测评系统中程序设计的自动批 改。 主题词：c a i ，e - l e a 础 n g ，无纸化测评，程序正确性，自动批改， x m l ，变量变化曲线 a b s t r a c t w i mt h er a p i dd e v e l o p m e n to fc o m p u t e rt e c h n o l o g y , e s p e c i a l l y t h ed e v e l o p m e n to fn e t w o r kt e c h n o l o g y , a n di t se x t e n s i v ea p p l i c a t i o n i nt h ef i e l do fe d u c a t i o n ，c a i ( c o m p u t e ra s s i s t e di n s t r u c t i o n ) a n d e - l e a r n i n gh a v eg a i n e dg r e a tp r o g r e s sa n dp r o m o t e dt h er e s e a r c ho f t e c h n o l o g y i n p a p e r l e s st e s t a n de v a l u a t es y s t e m i ta l w a y sb e d i f f i c u l ta n di m p o r t a n tt op u s hf o r w a r dt h er e f o r mi nh i g h e re d u c a t i o n b yu s i n gp a p e f l e s ss y s t e mt ot e s ta n d e v a l u a t et h es t u d e n t s s p e c i a l t y l e v e lr i g h t l y i nt h i sp a p e r , w er e s e a r c h e da n de x p a t i a t e do nt h e p r o b l e mo fp r o g r a ma u t o c h e c k i n gi np a p e r l e s st e s t a n de v a l u a t e s y s t e mb a s e do nl a n ，a n dm a d et h e u s e f u le x p e r i m e n t si nt h e a p p l i c a t i o n a n dt h e o r ya b o u tt h ei n d i v i d u a la n di n t e l l e c t u a l i z e d t e a c h i n g w ea n a l y z et h ep r o b l e mo fp r o g r a ma u t o - c h e c k i n ga n du s et h e p r o d u c t i o n si np r o g r a mc o r r e c t n e s sf o rr e f e r e n c e w ea l s op u tf o r w a r d t h et h o u g h tt h a tp r o c e e d i n ga u t o - c h e c k i n gb yl e v e la n dw e i g h t i n g ， a n dd e s c r i b e sf i v el e v e l so fc o r r e c t n e s sw h i c ha sf o l l o w s ：r e s u l t s ， l e x i c a la n a l y s i sa n ds y n t a xp a r s i n g ，m o d u l e s ，v a r i a b l e sc h a n g i n g c u r v e s ( v c cf o rs h o r t ) a n dc h e c k i n gb ym a n u a l f u r t h e rm o r e ，i t f o c u s e so nt h ea r i t h m e t i ca n di m p l e m e n tf o rl e x i c a ia n a l y s i s ，m o d u l e s m a t c h i n ga n dv c cm a t c h i n g f o rt h ee x t e n s i b i l i t ya n dr e u s a b i l i t y , w e u s es t a n d a r dm i d - l a n g u a g ex m lt od e s c r i b et h es o u r c e w eu s e m s x m l p a r s e rb a s e do nd o m t oo b t a i nx m ld o c u m e n tt r e es t y l e c h a r ta n dt om a t c hm o d u l e s a tt h es a m et i m e ，w eu s ev c ct or e f l e c t t h ec h a n g i n go fd a t af l o wa n dp u tf o r w a r dt h ev a l i d a t em e t h o do f v c c f i n a l l y , w ei m p l e m e n tt h ea u t o - c h e c k i n gi np a p e r l e s st e s ta n d e v a l u a t es y s t e m k e yw o r d s ：c a ，e l e a r n i n g ，p a p e r l e s st e s ta n de v a l u a t es y s t e m ， p r o g r a mc o r r e c t n e s s a u t o c h e c k i n g ，x m l ，v a r i a b l e sc h a n g i n g c u r v e 第一章绪论 1 1c a i 与数字化学习 1 1 1c a i 的现状与发展方向 计算机辅助教学( c o m p u t e ra s s i s t e di n s t r u c t i o n ，c a i ) 是将 计算机应用于教育领域的主要方面，是以计算机帮助或替代教师 执行部分教学任务，传递教学信息，对学生传授知识和训练技能， 提高教学效率和增强教学效果为目的的现代教学技术。它是计算 机科学、教育学、心理学、学科知识等多学科交叉形成的一门新 兴学科。在国际上始于5 0 年代末，在7 0 年代后期已有c a i 专著 问世，形成了c a 课程。8 0 年代初，我国也逐步开展对c a 的 研究，经过几十年的发展，逐渐形成了自己独有的理论研究和开 发应用范畴，产生了一套专门的概念、教学模式、工作方法和常 用技术【1 】。随着计算机技术、教育理论及教育的发展，c a 应用 已经由少数学科发展到几乎每一学科，并已在大、中、小学全面 铺开，对现代教育产生了革命性的影响。以计算机为核心的c a 是一种完全新颖的教学方式，体现了新的教学思想，它进行的是 个别化教学，具有交互性和因材施教的能力，这为培养高质量的 人才提供了活动空间和先进的教学手段，新的教育思想和教学原 则也逐步在新的计算机环境中确立起来。 目前c a 的形式主要表现为： 1 多媒体化c a 这种形式的c a i 广泛应用了9 0 年代兴起的多媒体技术，综 合处理和控制文字、声音、图形、图像、动画和活动视频等多种 形态的媒体信息，并按照教学活动的需要在诸多媒体元素之间建 立起一定的逻辑关联( 目前广泛以超文本超媒体方式来实现) ，从 而把它们有机组合并呈现出来，同时完成一系列随机性的人机交 互式操作，在这个交互过程中实现教学目树2 1 。多媒体课件形式 多样生动活泼、高度交互因材施教、信息量大、重现力强、界面 友好、操作简便，因此目前许多学校都相继建立了多媒体教室， 运用多媒体课件辅助教学。 2 网络化c a i 这是当前最盛行的c a t 方式。网络和多媒体技术与教育理 论结合的c a i 环境，改变了学生和教师在教学中的地位，实现了 “学生为主体，教师为主导”的现代教育思想，给学生提供了生动、 完善的教学环境，打破了时空范围，实现了资源共享，获得最佳 的教学效果。这种新型的教学环境是以校园网教学系统为代表。 一般学校常用的应用系统有：多媒体网络教室、多媒体电子阅览 室、网络多媒体课件制作系统、课件点播系统、远程教学系统等。 虽然c a i 在我国得到了广泛的关注和应用研究，但它仍存 在着一些缺点，如c a i 课件制作技术与教学实际脱节，部分教师 对c a i 的作用认识存在误区等。因此我们还需对c a i 的发展作进 一步的探索。目前的研究方向主要在智能化、虚拟现实、集成化、 可视化和基于c a i 的学科教学理论的研究几个方面i l l 。 c a 是计算机科学、教育学、心理学、信息科学、自动控制 理论、系统论等多学科交叉而形成的- - i 1 新兴学科。通过4 0 多年 的研究和实践，c a i 随着计算机在教育领域应用的深入及教学改 革的发展，得到了社会认同和普及推广。在c a t 领域，计算机及 网络信息技术提供了先进的知识表示方式与获取方式，改变了以 教师为中心的传统教学模式和以教师传授、灌输为主的学习模式。 c a i 不仅体现了先进的教学手段，而且体现了新的教育思想和教 学方法，是教育现代化的重要组成部分 3 1 。 c a i 的出现，对课程与教学的巨大冲击首先表现在它的教学 媒体( 计算机) ，不但作为教学内容多种信息表现形式的载体，而 且作为可以主动探索的设备，能够激发思维、训练思维，用作认 知工具和情感激励的工具。其次，则提出了对师生乃至管理人员 进行大规模全员信息技术培训、教育的需求。 c a i 对课程与教学改革的重大意义在于： 1 促进了教学手段的现代化，提高了师生的信息素养： 2 把教学媒体扩展为新的教育环境，引起教学模式的变化； 3 教学手段的多样化引发了教学内容、课程与教材模式的变化： 4 导致了整个教育目标与评价体系的变化； 5 带来了教育思想、观念和课程教学理论与实践的改变。 c a i 对课程与教学的冲击是巨大的，但带来的变革和进步影 响促进了教育的跨越式发展。在2 1 世纪信息社会中，c a i 必将继 续对教育改革产生重要作用p j 。 1 1 2 数字化学习 当前，信息技术教育已经进入到了一个新的阶段，即i i t c r i n t e g r a t i n gi n f o r m a t i o nt e c h n o l o g yi n t ot h ec u r r i c u l u m ，信息技术 与课程整合1 阶段，提出了“数字化学习”的概念。互联网的诞生和 c a i 的发展，使基于计算机、多媒体技术、网络通讯技术和卫星 传播技术的e - l e a r n i n g ( 数字化学习) 应运而生。e l e a r n i n g 是c a i 在多媒体计算机网络的基础上发展起来的，它的出现与发展是信 息技术应用于教学的必然，也是一个自然的演进过程。在先进的 建构主义学习理论指导下，计算机会议型c a i 系统、计算机网络 型c a i 系统与多媒体技术结合，通过计算机网络、多媒体、专业 内容网站、信息搜索、数字图书馆、远程学习与网上教室等新的 沟通机制来建构利于培养创造性人才的开放学习环境和全新的学 习方式，从而诞生了e - l e a r n i n 9 1 3 1 。 “e - l e a r n i n g ”的概念来自于国外。美国教育部教育技术办公 室在2 0 0 0 年底提出了“美国国家教育技术计划信息化学习： 把世界教育放到每一个儿童的指尖! ”( e l e a r n i n g ：p u t t i n ga w o r l d c l a s se d u c a t i o na tt h e f i n g e r t i p s o fa l l c h i l d r e n ，n a t i o n a l e d u c a t i o nt e c h n o l o g yp l a n ) ，将e l e a m i n g 作为国家教育技术计划 的总标题。2 0 0 0 年后，e l e a r n i n g 在国内专家学者的报告中开始 出现。2 0 0 1 年底，北京大学教育技术系举办国内首次e - l e a r n i n g 研讨会议，反映了国内教育技术领域追踪世界教育改革发展的最 新动态。何克抗教授提出了关于e l e a r n i n g ( 数字化学习) 的完整 内涵是：利用现代信息技术手段，通过信息技术与学科课程的有 效整合来实现一种理想的学习环境和全薪的、能充分体现学生主 体作用的学习方式，从而彻底改革传统的教学结构和教育本质， 达到培养大批具有2 1 世纪能力索质的人才( 即创新人才) 的目的 1 4 1 。这个内涵包含了三个方面的因素： 1 现代信息技术( 以多媒体和网络通信技术为代表) 数 字化学习的条件； 2 信息技术与学科课程的整合数字化学习的方法( 通过 有效的整合可以建构出一种理想的学习环境，这种环境可以支持 真实的情境刨设、不受时空限制的资源共享、快速灵活的信息获 取、丰富多样的交互方式、打破地区界限的协作交流、以及有利 于培养学习者创造性的自主发现和自主探索，在此基础上就可以 实现一种能充分体现学生主体作用的全新学习方式例如研究 性学习与合作式学习) ； 3 教学深化改革和创新人才培养数字化学习的目彬引。 数字化学习包含三个基本要素：即数字化学习环境、数字化 学习资源和数字化学习方式1 6 1 。数字化学习的特点是：课程学习 内容和资源的获取具有随意性，实效性，可操作性和可再生性， 并且在学习内容的探究上具有多层次性。 传统的c a i 方式仅仅是对教学方法与教学手段的改变，基 本上没有改变教学内容，更没有改变教学结构。而信息技术与课 程整合的目标是要通过信息技术所创建的理想学习环境和全新的 学习方式，从根本上改变传统的教学结构，所以二者之间有本质 的区别。e l e a r n i n g 是信息技术的产物，是教育改革的产物。它不 是c a i 的简单升级，也不是媒体与通讯系统的简单组合。 e l e a r n i n g 对c a i 的最大发展在于： 1 互联网是世界上最大的信息库、资源库、知识库，这些 知识库和资源库以符合人类联想思维特点的超文本结构方式组织 起来，为教学提供了组织、管理最有效，使用最便捷，内容最丰 富的教学内容和资源。在互联网上进行学习与教学活动的 e l e a r n i n g 特别适合于学生进行基于自主发现、自主探索的探究性 学习，提供了最能体现网络特性、最有利于2 l 世纪新型人材能力 素质培养的一种重要教学模式。 2 c a 强调的个别化教学策略利于发挥学生的主动性和进 行因人而异的个别指导，但在涉及高级认知能力学习的场合( 例如 对疑难问题的求解，或者要求对复杂问题进行分析、综合与评价) ， 则需要采用协作( c o l l a b o r a t i o n ) 式学习策略。e l e a r n i n g 的网络特 性为协作式学习提供了交互学习环境，满足了2 l 世纪新型人才能 力素质培养教学模式的要求。 3 e l e a r n i n g 的超文本特性与网络特性的结合使学生通过在 互联网的信息海洋中自由地探索、自主地获取信息，对所获取的 大量信息进行分析、评价、优选和进一步的加工，再根据自身的 需要予以应用，从而在信息技能方面得到很好的学习和锻炼，较 快地成长为既有高度创新精神、又有良好信息素养的符合2l 世纪 需求的新型人才。 4 e l e a r n i n g 以先进的建构主义教学理论为指导，创建由教 师、学生、教学内容与教学媒体等四要素组成的新型教学结构。 在e l e a r n i n g 的教学结构中，教师成为教学过程的组织者、指导 者、意义建构的帮助者、促进者；学生成为信息加工的主体和知 识意义的主动建构者；教材( 教学内容) 所提供的知识不是学生知 识的唯一来源，也不再是教师灌输的内容，而成为学生主动建构 意义的对象之一；教学媒体也不再仅仅是帮助教师传授知识的手 段，而成为用来创设情境和帮助学生自主学习、讨论交流、进行 协作式探索的认知工具与情感激励工具。e 。l e a r n i n g 以其全新的学 习方式彻底改变了教师的作用和师生之间的关系，从而根本改变 了教学结构和教育的本质。 从c a i 到e l e a r n i n g ，是c a i 随着教学改革深入的发展趋势， 是c a i 随着信息技术发展的历史必然i s 。 1 2 基于局域网的无纸化测评技术 1 2 1 概述 c a i 和e - l e a r n i n g 的深入研究，使无纸化测评技术的研究提 上了议事日程。教学中的无纸化测评包括两个方面：测与评。测 即实现无纸化作业和考试；评则是实现计算机自动批阅，检查学 生作业和考试答卷，给出评阅信息以指导学生学习和老师教学。 无纸化测评技术正好对应着教学中的测、评两个环节，实现由计 算机辅助的测试与评阅。显然，无纸化测评技术的研究与实现将 极大地促进e l e a r n i n g 的实现。 在数字化学习的发展趋势下，教学中越来越多的应用了信息 技术特别是计算机技术，掌握计算机基础知识和操作技能已经成 为现代教育体系下每一个学生所必备的基本素质。随着计算机应 用的普及，学校作为为社会培养高素质人才的基地，对计算机基 础教学的内容、手段及方法等进行全方位的改革以适应信息社会 的发展要求势在必行。计算机基础课程不仅是- - f 技术更新快、 信息量大的课程，同时也是一门实践性、操作性很强的课程。因 此，从教学内容上着手，紧跟计算机技术发展的新趋势，同时更 新教学手段，增加上机操作课程，促使学生能真正地学会使用计 算机、利用计算机进行思考，是非常必要的。同样计算机课程的 测评也应转变成无纸化的形式，以符合教学的要求。 教学和考核形式的改变，给从事计算机基础教学的教师带来 了一系列的问题。首先是硬件环境，即计算机的数量和硬件配置， 能否支持众多学生的学习和测评的需求，以及对测评软件的支持 的问题。由于计算机的发展使价格下降以及学校对教学设备投入 的增加，因此这个问题已得到基本解决。其次是软件环境，这就 需要开发全方位的无纸化测评系统。所谓全方位包括管理上的全 方位和测试内容的全方位。管理全方位是指测评管理、题卷管理、 题卷生成、上机测试、自动评阅各个环节。测试内容全方位是指 能覆盖测试要求的全部内容，例如w i n d o w s 、i n t e m e t 和文字处理 的常用操作，以及更高层次如简单程序设计。李克东的数字化 学习( 下卜信息技术与课程整合的核心一文中就曾经提到过 “充分发挥信息技术作为认知工具的作用主要做法有作为自 我测评和学习反馈工具” 7 】，这充分地说明了无纸化测评技术在 e - l e a r n i n g 中占有重要而不可或缺的地位。 在开发全方位的测评系统的思想指导下，利用现有的无纸化 测评技术，我们开发了一个基于w i n d o w s9 8 n t 2 0 0 0 平台的局域 网无纸化测评系统，实现测评管理、题卷管理、上机测试、自动 评阅各个环节的计算机自动处理。这一问题的解决，不仅着重测 评了学生的上机操作能力，而且大大提高了工作效率，规范和统 一了计算机基础课程的教学和测评，有效地促进了计算机基础教 学上e - l e a r n i n g 的改革。 1 2 2 基于局域网的无纸化测评系统总体功能及结构 一般来说，无纸化测评系统包括了五大模块： 1 测评管理子系统 测评管理子系统是对学生信息和学习成绩进行管理的系统。 其功能包括学生信息录入，成绩统计与分析，成绩查询，报表生 成等。 2 题卷管理子系统 题卷管理子系统主要是对测试题卷进行管理的系统。功能包 括题目及典型答案的录入，题卷的保存和管理。 3 题卷生成系统 手工生成题卷或按知识点、难度要求自动抽题生成题卷。 4 上机测评子系统 上机测评子系统是针对上机实时测评进行管理的系统。主要 功能有：验证身份，生成测评环境，组织学生上机测评，对上机 过程中出现的异常情况进行处理，并正确及时地收集学生答案数 据。 5 自动评阅子系统 自动评阅子系统实现对各种题型的自动判别、评分和评价， 包括：按批次收集学生答案数据，为防止异常中断进行数据各份， 以及将学生的成绩导入文本保存。 各个子系统协同工作，为教师提供一个合理化和规范化的工 作环境，同时也为学生营造了一个无纸化的计算机测试环境。系 统实现了无纸化评测的一系列活动的计算机自动化管理。大大地 提高了工作效率，极大地丰富了教学内容，同时也锻炼了学生的 计算机操作和实际应用能力，提高了计算机基础普及教育的质量。 基于局域网的无纸化测评系统总体逻辑结构如图1 1 所示： 圈1 - 1基于局域网的无纸化测评系统总体逻辑结构 1 2 3 基于局域网的无纸化测评技术的现状分析 对于基于局域网的无纸化测评技术，目前已有很多研究成果， 其中大部分针对的是客观题的测评，如选择、判断等。这些习题 类型的测评较为简单，也较容易实现，多数是通过对a s c i i 码的 比较来实现。对于主观题，如m i c r o s o f to f f i c e 系列、w p s 系列办 公软件，填空题和简答题及简单程序设计等，还不能完全实现智 能化测评。我们在条件限制下，使用m i c r o s o f t 的v b a ( v i s u a lb a s i c f o ra p p l i c a t i o n s ) 技术直接对w o r d 文档和e x c e l 电子表的属性进行 读写，实现了o f f i c e 系列w o r d 、e x c e l 文档的智能化测评【8 】【9 1 ， 并在此基础上类似地对w p s 文档实现了i 刍动测评。对于填空题和 简答题也给出了分类型的解决算洲1 0 】。但对于程序设计题的测评 技术一直进展缓慢。如c 语言程序设计题，测评的思路主要有以 下几种： 1 简单比较：将多个但是有限个的正确答案做出来，将学生 所做答案与这些答案一一比较，看是否相同来判定正确与否。但 这种方法存在弊端：有的情况下，将所有正确答案都列举出来是 非常困难甚至是不可能的；而对于简单的题目，学生可以用纸笔 计算后，直接写出答案来“欺骗”测评系统。 2 直接运行结果：程序总是可以运行的，虽然结果并不一定 正确。所以可以直接比较学生程序与标准答案程序结果是否相同， 根据比较结果判分。但这种方式不能很好地解决学生程序不能正 确运行或结果不符合要求时的评测问题，也不能反映错误在何处。 3 理论分析方式：通过分析学生程序及标准答案的源程序找 出他们的相同及不同处，根据比照结果来进行判分。从理论上说， 这种方法准确率最高，但目前在这方面的成果较少。本文着重在 这一方面进行研究和论述【l 。 1 3 本文的研究目的、主要成果及意义 显然，在基于局域网的无纸化测评系统中，自动评阅子系统 是极为重要的一个模块。它必须保证能够迅速及时地批阅学生的 答案，并保证评分的准确性。在作为练习系统使用的无纸化测评 系统中，自动评分子系统还应具有反馈错误的功能，以使学生在 自学自测的过程中掌握学习的主动性，确定下一步学习的重点， 体现数字化学习的内涵。同时自动评阅子系统也是整个测评系统 的难点所在，其关键问题就在于主观题的判读与评分，包括文字 操作题、简答和填空题及简单程序设计的自动评阅。 1 , 3 1 本文的研究目的和主要成果 本文的研究目的是在一定的条件下，解决无纸化测评系统中 简单程序设计的自动批改问题，保证评测系统要求的及时性和正 确性。为此我们做了较深入的探讨，主要成果有： 1 综述当前软件工程领域关于“程序正确性校验”的发展与 现状，借鉴了程序正确性验证的部分成果。根据f l o y d h o m e 方 法，对当前基于局域网的无纸化测评技术中简单程序设计的自动 批改提出了模块化的评阅方法。在结构化程序中，运用断言和形 式逻辑推理系统，将程序分解为四类基本功能模块：顺序、分支、 循环、过程，进行功能模块的匹配和变量变化曲线匹配，综合验 证程序中控制流和数据流的正确与否。 2 由于本文的测评技术分析仅针对c 语言程序设计题，为 了实现程序的可重用性和可扩展性，我们将具体程序转换为一种 标准的中间语言，留出标准接口以便对其他程序设计语言也能方 便地应用测评模块。这种标准的中间语言并非程序设计语言，也 不是自然语言，而是介于二者之间的，语法较简单。本文中采用 的是x m l 语言，定义了一个x m ls c h e m af o rc ，作为c 语言程 序文档转换的规则。由于x m l 具有可扩展、易标记的特性，较 好地实现了我们的要求。使用m s x m l 解析x m l 文档得到树状 结构图，实现c 语言程序功能模块的结构匹配； 3 根据无纸化测评系统中的程序设计测评的要求，其目的 是为了考核学生掌握程序设计语言和程序设计方法的程度，因此 我们提出了“加权评分”的概念，设置了五个级别的正确程度，每 个级别可以设置不同比重的“权”，以此在自动评分子系统中实现 判别和计分的智能化。 1 0 1 3 2 本文的意义 随着信息技术和人工智能技术的发展，借助网络和计算机进 行学习已经成为现代教育的一种新思路。为了正确及时地反映学 习的效果，实现真正意义上的数字化学习，作业和考试测评系统 也必须体现“智能化”的特点。基于局域网的无纸化测评技术中， 程序设计的自动批改问题是一个尚未解决的难点，基本没有可参 照成果。本文对此作了有益的探讨，为解决这一关键问题进行了 深入的研究。其研究成果可应用到无纸化测评系统中，促进c a i 和e - l e a r n i n g 的发展。 1 4 本文的结构 本论文的内容组织如下： 第一章“绪论”介绍了有关背景知识：c a i 与数字化学习的发 展，基于局域网的无纸化测评技术以及本文的研究目的、主要成 果和意义； 第二章“程序设计自动批改及相关领域的研究概况”介绍了程 序设计自动批改与正确性验证的区别，程序正确性验证的已有方 法和研究成果等； 第三章“程序设计自动批改系统的实现思想及关键问题”阐述 了自动批改系统的实现思想，描述了实现过程中的关键问题； 第四章“程序语句结构的x m ls c h e m a 定义( c 语言1 ”简单介 绍了将要用到的工具x m l 及其模式语言s c h e m a 、文档对象模型 d o m 和解析器m s x m l ；给出了c 语言中各种结构语句的x m l s c h e m a 定义，用图形的方式表示了这一定义，并给出了一个简单 的例子； 第五章“基于x m l 的程序设计自动批改系统的实现方案”给 出了具体实现的流程，并分别论述了词法和语法分析模块、结构 模块匹配算法和变量变化曲线的表示及匹配的实现算法； 第六章“实验系统及结果分析”对问题进行了描述和一定条件 上的限制，针对典型性验证实例，包括正确的实例、语法错误的 实例、逻辑错误的实例、结构不匹配的实例等的结果分析，并对 随机取样的试卷进行了实例的结果分析： 第七章“总结与展望”总结了本文的工作成果，指出了其中的 不足，提出了有待解决的问题。 第二章程序设计自动批改及相关领域的研究概况 2 1 程序设计自动批改与程序正确性验证 在计算机广泛应用于人类生活各个方面的今天，许多计算机 软件系统与人类的生命和财产安全直接相关，例如银行管理、交 通管理、航天和航空管理等系统。设计人员和使用人员都希望在 将软件系统投入正式运行之前，能得到系统正确性的保证，或能 将正确性提高到比较高的程度。程序验证是保证软件系统正确性 的一个重要手段，也是计算机软件工程方法和技术的一个组成部 分。其意义在于： 1 保证相关人员的生命安全，如交通管理、航天和航空管理 等系统； 2 节省费用，避免不必要的损失； 3 保证计算机系统本身的安全性，防止因不合法输入或恶意 代码导致的溢出、系统崩溃或死循环等情况发生。 由于面向的对象和评判的前提不同，程序设计自动批改系统 与程序正确性验证既有联系，又有区别。其区别在于： 1 一般的程序正确性验证针对大型软件进行，其所验证的对 象并没有一个绝对正确的标准答案可以用来参照，而在程序设计 自动批改系统中要达到的目的是验证小型程序设计的正确性，因 此存在标准程序可用来进行算法、流程图等各方面的对比与匹配。 2 对大型应用软件的正确性验证，由于涉及到实际生活中的 各方面，甚至关系到人身和财产安全，要求绝对意义上的正确， 对任何输入( 不管合法与否) 都必须能够停机并给出合理的输出。 而作业批改与测评系统中的程序设计验证并不要求绝对正确，其 目的是为了测评学生掌握程序设计语言的程度，因此需要实现模 糊判别，分步骤加权检验和计分。 程序设计自动批改是一类很特殊的程序正确性验证问题，其 目的不是单纯地证明程序的正确性，而是以程序的正确程度为依 据，测评学生对程序设计语言、程序设计方法以及相关的知识的 正确理解和熟练运用程度。测评结果可以用于指导教师教学和学 生学习。由于测评的依据是程序正确的程度，我们可以利用已有 程序正确性验证研究的成果，主要是运用其思想来解决程序设计 自动批改这个特殊问题。因此，我们对程序正确性的研究现状和 已有成果做了深入的研究。 2 2 程序正确性验证的研究概况 所谓一段程序是正确的，是指对任何一组允许的输入数据， 程序执行终止，并能得到一组与之相对应的正确的输出数据【l 引。 因此程序正确性验证方法包括了证明程序正确性和证明程序终止 性两类。 目前在程序正确性验证领域，国外研究的成果主要有：证明 程序部分正确性的r w f l o y d 在1 9 6 7 年提出的归纳断言法、h o a r e 在f l o y d 方法的基础上提出的验证规则方法( v e r i f i c a t i o nr u l e s ) ， 即“公理式方法”以及由戈登( m g o r d o n ) 首创提出、霍迈尔 ( p h o m e i e r ) 和马丁( d m a r t i n ) 进行改进和完善的基于定理证明系 统的形式化的开发方法1 1 2 ；证明程序终止性的1 9 6 7 年由 r w f l o y d 提出来的良序集方法和1 9 6 8 年由d e k n u t h 提 出来的计数器方法。 国内研究的成果有南京大学的章萃等在戈登和霍迈尔的基础 上进一步完善的基于定理证明系统的方法；东南大学滕至阳、袁 全生、程正潮提出的分割图方法。 2 2 1 证明程序正确性的方法 1 r w f l o y d 的归纳断言法 1 9 6 7 年，r o b e r t f l o y d 发明了把计算机程序和一系列逻辑断 1 4 言联系起来的技术。无论”控制”何时经过，每个断言总是为真。 所有的断言被在断言之间出现的一些程序语言里的声明约束在一 起。有希望的是：进入断言规定了在何种情况下程序会运行，而退 出断言描述了程序计算什么。该方法在几年以后被c a r h o a r e 采用，他将其应用到自明性方法中去定义语义学，或是定义一个 编程语言中的每个断言的意义。这种方法成为了定义语言语义学 的两个方法中的一种【1 5 】【1 6 l 。 其具体作法是：在程序流程图的每一条边上附上一个谓词公 式( 称为断言) 对于循环即流程图中的回路，他定义了一个切 点，并在切点上设置一个断言。然后定义：一个程序是正确的， 如果： ( 1 ) 对于程序流程图中的每一条边，当程序运行到该条边时， 其所附的断言为真； ( 2 ) 对于循环，若回路开始执行时其切点上的断言为真，则当 循环回复到该切点时其断言仍应该为真，即所谓的“循环不变 式【1 7 】。 断言式方法主要困难就是如何选择正确的断言，无法设计一 个通用的算法由计算机来完全承担。这样在验证的过程中，人的 提示将无法避免，程序的正确性验证工作就会大大地依赖于操作 人员的实际工作能力，而且也会极大地增加验证工作所花费的时 间。同时，在断言的证明过程中还会遇到类似于公理式方法中所 遇到的困难：由于有意义的公理系统通常包括不止一条公理，根 据数理逻辑的理论研究，不存在一个能行的机械算法可以使计算 机能从公理系统中选择合适的公理来证明所需的结论，这种方法 的计算复杂度是指数形式的。更为重要的是，当程序不正确时， 计算机会一直工作下去而不停止。( 根据数理逻辑的研究：一个一 阶谓词逻辑系统的定理集合是递归可枚举集，即半可计算集【2 卯。) 2 h o a r e 的验证规则方法( v e 畦f i c a t i o nr u l e s ) 1 8 】 1 9 6 9 年，h o a r e 发表了计算机程序设计的公理基础一文， 1 5 建立了所谓的“h o a r e 逻辑”。这是一种含有程序公理和推理规则的 形式逻辑推理系统由于这种逻辑系统可在计算机上实现，人们 使用它来证明程序的部分正确性。这种程序正确性验证方法称为 “公理式方法”【1 7 1 。 程序的规格说明必须按以下形式给出： 前置条件) 程序或语句 后置条件) 前置条件定义了执行程序或语句前程序状态和变量所需要满 足的条件，后置条件则定义了执行程序或语句后程序状态和变量 所需要满足的条件。当前置条件满足时，正确的程序必须保证其 程序状态和变量在经过程序执行后满足其后置条件。因此，一个 程序正确性的定义是与给定的前置条件和后置条件相关的。一个 程序的规格说明给出后，程序的正确与否就可以在程序逻辑中进 行形式化的验证了。由于整个程序验证过程中的每一步都要使用 程序逻辑中的公理或推理规则，程序正确性的验证过程实际上就 是一个用程序逻辑构造定理证明的过程。 大多数程序验证系统是半自动化的或称为交互式的。程序验 证系统通常采用面向目标的验证方法。其核心部分是一个验证条 件产生器。验证条件产生器从最大的、整个程序的验证目标出发， 根据程序逻辑中的推理规则，不断地从大验证目标中分解产生出 它的子验证目标，也称之为验证条件。当最小的、最基本的验证 条件，可用程序逻辑中的公理直接验证其正确性时，程序验证系 统再由小到大地逐步构造起整个程序正确性的证明。因此，整个 程序正确性证明的构造过程是分解产生程序验证条件的逆过程。 从程序逻辑中的推理规则这个角度来看，程序正确性证明的构造 过程是正向地使用推理规则，而程序验证条件的分解产生过程则 是逆向地使用推理规则u 9 1 。 公理式方法存在的问题有： ( 1 ) 自动化程序逻辑的可靠性，也就是程序验证系统和语言 实现系统的语义一致性问题。对于一个给定的程序设计语言，其 程序验证系统是根据这个语言的公理化语义定义( 即该语言的程 1 6 序逻辑) 来研制开发。而这个语言的实现系统，如编译系统或解 释系统，则根据这个语言的指称化语义定义来研制和开发。理论 上，对于一个语言给出这两种语义定义时，可以用数学的方法验 证其一致性。而根据这两种语义定义，对同一语言分别研制开发 一个程序验证系统和一个语言实现系统时，保证这两个软件系统 语义的一致性决不是一个简单的问题。从程序验证系统的角度来 看，这是一个如何保证其语义可靠性的问题。程序逻辑的可靠性 要求所有的自动化公理和推理规则都是指称化语义的语义蕴含。 即当个程序在程序验证系统中被证明正确时，要能保证这个程 序经过语言实现系统处理后实际运行时的正确性。然而，大多数 自动化程序验证系统要么没有进行这种可靠性的验证，要么只是 对此进行了手工验证。由于这种可靠性的验证过程非常复杂，手 工验证不仅容易出错，而且难以保证与实际系统一致【2 6 】。 ( 2 ) 程序验证系统的正确性。当用一个程序验证系统来验证 程序时，整个程序验证系统的工作就是不断正向或逆向地使用程 序逻辑中的公理和推理规则。程序验证过程的正确与否完全取决 于整个程序验证系统工作的正确与否，特别取决于其中的验证条 件产生器工作的正确与否。也就是说，验证系统本身的正确性， 决定了程序验证过程的正确性。在相当长的时期内，研究人员通 常只是采用各种软件测试方法( 如：黑盒测试自盒测试) ，来检 测系统中存在的错误和问题，但无论软件测试方法如何先进，都 不可能提供整个程序验证系统正确性的保证【2 6 1 。 3 基于定理的证明方法 由戈登( m g o r d o n ) 首创提出一种基于定理证明系统的形式化 的开发方法，将程序验证系统的可靠性和正确性完全建立在严格 的数理逻辑基础上【2 0 】。这种方法强调将定理证明系统提供的形式 化的和自动化的数学证明方法和技术，应用于程序验证系统本身 的开发和验证过程。 首先要求使用定理证明系统提供的界面语言来编制和开发程 1 7 序验证系统，然后要求整个开发过程的每一步都使用定理证明系 统来进行自动化或半自动化的验证。在定理证明系统中进行的验 证是严谨的，从而，保证了自动化程序逻辑的可靠性和程序验证 系统本身的正确性【2 i j 。 这种形式化的开发方法有五个主要步骤。其中，三个规格说 明步骤可被视为用一个选定的定理证明系统提供的界面语言，对 程序验证系统进行定义和编写程序的步骤。其余两个验证步骤则 分别对自动化程序逻辑的可靠性和程序验证系统本身的正确性进 行验证：步骤一必须对程序设计语言的指称化语义进行形式化的 规格说明；步骤二进一步要求对该语言的公理化语义也就是 该语言的程序逻辑进行规格说明。对该语言的每一个语句构造结 构，必须给出其相应的公理或推理规则的规格说明1 2 2 1 。 4 分割图证明 分割图方法适用于对应用系统内部功能的描述。该方法把内 部功能看成是一个主功能模块，它接受一组输入而产生一组输出， 主模块的功能可分割成由若干个子模块完成。每个子模块又可继 续分割直到它的功能简单得能直接给出为止。因此，内部功能的 设计过程是一个自顶向下的分割过程。模块和模块分割是该方法 的主要概念1 2 引。 2 2 2 证明程序终止性的方法 1 计数器方法 计数器方法是1 9 6 8 年由d e k n u t h 提出来的。它的基本 思想是：对程序中的每一个循环附加一个新的变量( 通常称为计 数器) ，在进入该循环前计数器置0 ，循环通路每执行一次计数器 加1 。对每一个循环提供一个新的中间断言，它表示相应的计数 器不会超过某个固定的界限。进一步，证明此中间断言是不变式 断言，因而可以断定循环只能执行有限次，由此程序是终止的。 计数器方法的另外一种形式是：对程序中的每个循环，构 1r 成一个和该循环有关的整数n ( x ，y ) ，n ( x ，y ) 满足下面两个条件： ( 1 ) 当使循环继续进行的条件成立时，n ( x ，y ) o ； ( 2 ) 每执行一次循环，n ( x ，y ) 的值都减小，这时n ( x ，y ) 的值 构成一个单调减小整数序列，且n ( x ，y 砭0 ，因而循环只能执行 有限次1 。 2 r - w f l o y d 的良序集法 良序集方法是1 9 6 7 年由r w f l o y d 提出来的。它是证明 程序终止性的一种基本的方法。该方法基于良序集的概念。 设程序p 的输入断言为中( 均。利用良序集方法