上海工程技术大学
毕业设计（毕业论文）任务书
学院继续教育学院
专业计算机科学与技术
班级学号
学生王俊佶
指导教师张辉
题目农夫过河问题的逻辑建模与程序验证
任务规定
进行日期自2011 年9 月？日起，至2012 年 1 月？日止
一、题目来源、目的、意义
数理逻辑作为基础数学的一个重要分支，在通信、电子及计算机科学中起着奠基作用，在模糊数学和人工智能等方面也都有着广泛的应用，其中有限模型、解析算法、有限计算和可判定性等内容都与计算机的软硬件密切相关。

各种游戏的设计，离不开游戏环境的规范描述，大多数使用的都是一个逻辑上的满足关系M╞φ，其中M是某种游戏的场景或模型，而φ是一个情节的规范。

本课题可以有效地锻炼学生的综合应用已有知识、自学新知识的能力，使学生有效的对大学所学过的知识进行深入的总结。

二、主要工作内容
本课题利用逻辑语言Alloy或模型检测工具SMV，通过对农夫过河游戏的场景进行逻辑建模，求解智力难题，充分理解和体会逻辑在软件规范中的作用，学习逻辑程序设计的基本原理和培养实际的开发经验，是对计算机软件与理论教学的有效拓展。

1.学习数理逻辑的基础知识
2.学习逻辑语言Alloy或模型验证工具SMV
3.编写出描述农夫过河游戏的逻辑规范程序
4.程序测试，并对错误进行适当处理
三、主要技术指标（或主要论点）
1. 农夫过河游戏的逻辑模型描述
2. 逻辑语言Alloy程序的开发或模型验证工具SMV的运用
3. 程序结果分析
四、进度计划
第一至二周：进行市场调研和文献检索，并进行整理，写出开题报告；
第三周：外文资料翻译，配置程序开发环境；
第四至五周：学习数理逻辑基础知识和时态逻辑的原理；
第六到七周：学习使用逻辑语言Alloy或模型验证工具SMV；
第八周：设计农夫过河游戏的逻辑模型；
第九至十一周：初步设计逻辑程序；
第十二至十四周：调试逻辑程序；
第十五至十八周：论文写作及答辩。

五、主要参考资料（外文资料至少一篇）
[1] Michael Huth，,Mark Ryan．Logic in Computer Science[M]．2nd Edition．Cambridge University Press，2004．
[2] Anil Nerode，Richard Shore．Logic for Applications[M]．2nd Edition．Springer，1997．
[3] Aho，Hopcroft，Ullman．Data Structures and Algorithms[M]．Addison-Wesley，1983．
[4] Aho，Hopcroft，Ullman．The Design and Analysis of Computer Algorithms[M]．Addison-Wesley，1974．
[5] Edmund Clarke．The SMV System [OL]．/~modelcheck/，1998．
[6] Edward Y ue Shung Wong，Omar Tayeb，Michael Herrmann．A Guide to Alloy [OL]．/project/examples/2007/271j/suprema_on_alloy/Web/，2008．
[7] Chris Herberte．Alloy Community[OL]．/community/，2008．
[8] Herbert Enderton，A Mathematical Introduction to Logic[M]．2nd Edition．Academic Press，2000．
[9] George Boolos，John Burgess，Richard Jeffrey．Computability and Logic[M]．4th Edition．Cambridge University Press，2002
[10] Edmund Clarke．Model Checking[M]．The MIT Press，1999
六、系审批意见
系主任（签名）:
七、院领导审核意见
院领导（签名）:
八、学生实际完成日期九、同组设计（论文）者。