任务书-农夫过河问题的逻辑建模与程序验证
- 格式:doc
- 大小:54.50 KB
- 文档页数:4
数据结构课程设计报告(农夫过河)第一篇:数据结构课程设计报告(农夫过河)目录引言...................................................2 问题描述..............................................3 基本要求 (3)2.1为农夫过河问题抽象数据模型体会数据模型在问题求解中的重要性;........3 2.2设计一个算法求解农夫过河问题,并输出过河方案;......................3 3 概要设计 (3)3.1 数据结构的设计。
....................................................3 3.1.1农夫过河问题的模型化.............................................3 3.1.2 算法的设计 (4)4、运行与测试 (6)5、总结与心得..........................................7 附录...................................................7 参考文献. (13)引言所谓农夫过河问题是指农夫带一只狼、一只羊和一棵白菜在河南岸, 需要安全运到北岸。
一条小船只能容下他和一件物品, 只有农夫能撑船。
问农夫怎么能安全过河, 当然狼吃羊, 羊吃白菜, 农夫不能将这两种或三种物品单独放在河的一侧, 因为没有农夫的照看, 狼就要吃羊, 而羊可能要吃白菜? 这类问题的实质是系统的状态问题, 要寻求的是从初始状态经一系列的安全状态到达系统的终止状态的一条路径。
1 问题描述一个农夫带一只狼、一棵白菜和一只羊要从一条河的南岸过到北岸,农夫每次只能带一样东西过河,但是任意时刻如果农夫不在场时,狼要吃羊、羊要吃白菜,请为农夫设计过河方案。
基本要求2.1为农夫过河问题抽象数据模型体会数据模型在问题求解中的重要性;2.2设计一个算法求解农夫过河问题,并输出过河方案;概要设计3.1 数据结构的设计。
农夫过河问题一、实验目的掌握广度优先搜索策略,并用队列求解农夫过河问题二、实验内容问题描述:一农夫带着一只狼,一只羊和一颗白菜,身处河的南岸,他要把这些东西全部运到北岸,遗憾的是他只有一只小船,小船只能容下他和一件物品。
这里只能是农夫来撑船,同时因为狼吃羊、羊吃白菜、所以农夫不能留下羊和狼或羊和白菜在河的一边,而自己离开;好在狼属肉食动物,不吃白菜。
农夫怎么才能把所有的东西安全运过河呢?实验要求如下:(1)设计物品位置的表示方法和安全判断算法;(2)设计队列的存储结构并实现队列的基本操作(建立空队列、判空、入队、出队、取对头元素),也可以使用STL中的队列进行代码的编写;(3)采用广度优先策略设计可行的过河算法;(4)输出要求:按照顺序输出一种可行的过河方案;提示:可以使用STL中的队列进行代码编写。
程序运行结果:二进制表示:1111011011100010101100011001,0000三、农夫过河算法流程⏹Step1:初始状态0000入队⏹Step2:当队列不空且没有到达结束状态1111时,循环以下操作:⏹队头状态出队⏹按照农夫一个人走、农夫分别带上三个物品走,循环以下操作:⏹农夫和物品如果在同一岸,则计算新的状态⏹如果新状态是安全的并且是没有处理过的,则更新path[ ],并将新状态入队⏹当状态为1111时,逆向输出path[ ]数组附录一:STL中队列的使用注:队列,可直接用标准模板库(STL)中的队列。
需要#include<queue>STL中的queue,里面的一些成员函数如下(具体可以查找msdn,搜索queue class):front:Returns a reference to the first element at the front of the queue.pop:Removes an element from the front of the queuepush:Adds an element to the back of the queueempty:Tests if the queue is empty三、实验代码FarmerRiver.H#ifndef FARMERRIVER_H#define FARMERRIVER_Hint FarmerOnRight(int status); //农夫,在北岸返回1,否则返回0int WorfOnRight(int status); //狼int CabbageOnRight(int status); //白菜int GoatOnRight(int status); //羊int IsSafe(int status); //判断状态是否安全,安全返回1,否则返回0void FarmerRiver();#endifSeqQueue.h#ifndef SEQQUEUE_H#define SEQQUEUE_Htypedef int DataType;struct Queue{int Max;int f;int r;DataType *elem;};typedef struct Queue *SeqQueue;SeqQueue SetNullQueue_seq(int m);int IsNullQueue_seq(SeqQueue squeue);void EnQueue_seq(SeqQueue squeue, DataType x);void DeQueue_seq(SeqQueue);DataType FrontQueue_seq(SeqQueue);#endifFarmerRiver.c#include <stdio.h>#include <stdlib.h>#include "SeqQueue.h"#include "FarmerRiver.h"int FarmerOnRight(int status) //判断当前状态下农夫是否在北岸{return (0!=(status & 0x08));}int WorfOnRight(int status){return (0!=(status & 0x04));}int CabbageOnRight(int status){return (0!=(status & 0x02));}int GoatOnRight(int status){return (0!=(status & 0x01));}int IsSafe(int status) //判断当前状态是否安全{if ((GoatOnRight(status)==CabbageOnRight(status)) &&(GoatOnRight(status)!=FarmerOnRight(status)))return (0); //羊吃白菜if ((GoatOnRight(status)==WorfOnRight(status)) && (GoatOnRight(status)!=FarmerOnRight(status))) return 0; //狼吃羊return 1; //其他状态是安全的}void FarmerRiver(){int i, movers, nowstatus, newstatus;int status[16]; //用于记录已考虑的状态路径SeqQueue moveTo;moveTo = SetNullQueue_seq(20); //创建空列队EnQueue_seq(moveTo, 0x00); //初始状态时所有物品在北岸,初始状态入队for (i=0; i<16; i++) //数组status初始化为-1{status[i] = -1;}status[0] = 0;//队列非空且没有到达结束状态while (!IsNullQueue_seq(moveTo) && (status[15]==-1)){nowstatus = FrontQueue_seq(moveTo); //取队头DeQueue_seq(moveTo);for (movers=1; movers<=8; movers<<=1)//考虑各种物品在同一侧if ((0!=(nowstatus & 0x08)) == (0!=(nowstatus & movers)))//农夫与移动的物品在同一侧{newstatus = nowstatus ^ (0x08 | movers); //计算新状态//如果新状态是安全的且之前没有出现过if (IsSafe(newstatus)&&(status[newstatus] == -1)){status[newstatus] = nowstatus; //记录新状态EnQueue_seq(moveTo, newstatus); //新状态入队}}}//输出经过的状态路径if (status[15]!=-1){printf("The reverse path is: \n");for (nowstatus=15; nowstatus>=0; nowstatus=status[nowstatus]){printf("The nowstatus is: %d\n", nowstatus);if (nowstatus == 0)return;}}elseprintf("No solution.\n");}Sequeue.c#include <stdio.h>#include <stdlib.h>#include "SeqQueue.h"SeqQueue SetNullQueue_seq(int m){SeqQueue squeue;squeue = (SeqQueue)malloc(sizeof(struct Queue));if (squeue==NULL){printf("Alloc failure\n");return NULL;}squeue->elem = (int *)malloc(sizeof(DataType) * m);if (squeue->elem!=NULL){squeue->Max = m;squeue->f = 0;squeue->r = 0;return squeue;}else free(squeue);}int IsNullQueue_seq(SeqQueue squeue){return (squeue->f==squeue->r);}void EnQueue_seq(SeqQueue squeue, DataType x) //入队{if ((squeue->r+1) % squeue->Max==squeue->f) //是否满printf("It is FULL Queue!");else{squeue->elem[squeue->r] = x;squeue->r = (squeue->r+1) % (squeue->Max);}}void DeQueue_seq(SeqQueue squeue) //出队{if (IsNullQueue_seq(squeue))printf("It is empty queue!\n");elsesqueue->f = (squeue->f+1) % (squeue->Max); }DataType FrontQueue_seq(SeqQueue squeue) //求队列元素{if (squeue->f==squeue->r)printf("It is empty queue!\n");elsereturn (squeue->elem[squeue->f]);}main.c#include <stdio.h>#include <stdlib.h>#include "FarmerRiver.h"int main(void){FarmerRiver();return 0;}实验结果:四、实验总结。
农夫过河C语言课程设计一、课程目标知识目标:1. 理解C语言中基本的数据类型和语法结构;2. 学会使用C语言进行逻辑判断和循环控制;3. 掌握C语言中的函数定义和调用方法;4. 了解“农夫过河”问题的背景和解决方案。
技能目标:1. 能够运用C语言编写出解决“农夫过河”问题的程序;2. 培养逻辑思维和问题分析能力,将实际问题转化为程序代码;3. 提高编程实践能力,学会调试和修改代码,解决程序中的错误。
情感态度价值观目标:1. 激发学生对编程的兴趣,培养计算机科学素养;2. 培养学生面对问题积极思考、勇于探索的精神;3. 强调团队合作,学会与他人共同解决问题,培养沟通与协作能力。
分析课程性质、学生特点和教学要求:本课程为C语言编程课程,旨在让学生掌握C语言的基本知识,并通过解决实际问题,提高编程能力。
学生为初中生,具有一定的逻辑思维能力和数学基础。
教学要求注重实践,将理论教学与实际操作相结合,引导学生主动参与,培养其独立思考和解决问题的能力。
课程目标分解:1. 知识目标:通过讲解和实例演示,让学生掌握C语言的基本知识;2. 技能目标:通过编写“农夫过河”程序,提高学生的编程实践能力;3. 情感态度价值观目标:通过课程教学,激发学生对编程的兴趣,培养其积极思考、勇于探索的精神,以及团队合作能力。
二、教学内容1. C语言基础知识回顾:- 数据类型、变量、常量- 运算符、表达式、语句- 选择结构(if-else)- 循环结构(for、while、do-while)2. 函数定义与调用:- 函数的概念和作用- 函数的定义、声明和调用- 递归函数的原理和应用3. “农夫过河”问题分析:- 问题的描述和规则- 状态表示和状态空间- 搜索策略(深度优先、广度优先)4. 编程实践:- 设计“农夫过河”问题的算法- 编写C语言程序实现算法- 调试和优化程序5. 教学内容安排与进度:- 第一课时:C语言基础知识回顾,引入“农夫过河”问题- 第二课时:函数定义与调用,分析问题并设计算法- 第三课时:编写程序,实现“农夫过河”算法- 第四课时:调试优化程序,总结经验,展示成果教学内容关联教材章节:- 《C语言程序设计》第一章:C语言概述- 《C语言程序设计》第二章:数据类型与运算符- 《C语言程序设计》第三章:控制结构- 《C语言程序设计》第四章:函数- 《C语言程序设计》第十章:算法与程序设计实例教学内容注重科学性和系统性,结合教材章节,使学生能够在掌握C语言基础知识的基础上,学会解决实际问题,提高编程能力。
一、题目:农夫过河问题二、目的与要求1、目的:通过布置具有一定难度的实际程序设计项目,使学生进一步理解和掌握课堂上所学各种基本抽象数据类型的逻辑结构、存储结构和操作实现算法,以及它们在程序中的使用方法;使学生掌握分析问题,求解问题的方法并提高学生设计编程实现的能力。
2、要求:基本要求:1.要求利用C\C++语言来完成系统的设计;2.突出C语言的函数特征(以多个函数实现每一个子功能)或者C++语言面向对象的编程思想;3.画出功能模块图;4.进行简单界面设计,能够实现友好的交互;5.具有清晰的程序流程图和数据结构的详细定义;6.熟练掌握C语言或者C++语言的各种操作。
创新要求:在基本要求达到后,可进行创新设计,如系统用户功能控制,改进算法的实现,实现友好的人机交互等等三、问题描述和求解方法:1 、问题描述要求设计实现农夫过河问题(农夫带着一只狼,一只养,一棵白菜,一次只能带一个东西)如何安全过河。
2 、问题的解决方案:可以用栈与队列、深度优先搜索算法及广度优先搜索算法相应的原理去解决问题。
1)实现四个过河对象(农夫、白菜、羊和狼)的状态,可以用一个四位二进制数来表示,0表示未过河,1表示已经过河了。
2)过河的对象必须与农夫在河的同一侧,可以设计函数来判断。
3)防止状态往复,即农夫将一个东西带过去又带回来的情况发生,需将所有可能的状态进行标定。
4)可用深度优先搜索算法及广度优先搜索算法去解题。
四、解题过程1.分析程序的功能要求,划分程序功能模块。
2.画出系统流程图。
3.代码的编写。
定义数据结构和各个功能子函数。
4.程序的功能调试。
5.完成系统总结报告以及使用说明书五、进度安排此次课程设计时间为一周,分以下几个阶段完成:1.选题与搜集资料:每人选择一题,进行课程设计课题的资料搜集。
2.分析与概要设计:根据搜集的资料,进行程序功能与数据结构分析,并选择合适的数据结构、并在此基础上进行实现程序功能的算法设计。
课程设计农夫过河一、教学目标本章节的教学目标包括以下三个方面:1.知识目标:学生能够理解并掌握“农夫过河”问题的背景、条件和目标,了解相关的数学知识,如线性方程、不等式等。
2.技能目标:学生能够运用所学的数学知识,通过分析和逻辑推理,找到解决问题的方法,并能够进行有效的沟通和合作。
3.情感态度价值观目标:学生能够培养问题解决的兴趣和自信心,培养团队合作和沟通的能力,培养对数学学科的积极态度。
二、教学内容本章节的教学内容主要包括以下几个部分:1.引入“农夫过河”问题的背景和条件,引导学生了解问题的目标和意义。
2.引导学生学习相关的数学知识,如线性方程、不等式等,并通过例题和练习题进行巩固。
3.引导学生运用所学的数学知识,分析和解决“农夫过河”问题,寻找最优解法。
4.通过小组讨论和展示,培养学生的团队合作和沟通能力。
三、教学方法本章节的教学方法主要包括以下几种:1.讲授法:教师通过讲解和演示,引导学生理解和掌握相关的数学知识和解决问题的方法。
2.讨论法:教师学生进行小组讨论,鼓励学生提出问题、分享思路和解决方案。
3.案例分析法:教师提供具体的案例,引导学生运用所学的数学知识进行分析和解决。
4.实验法:教师引导学生进行实验操作,通过实践来加深对数学知识的理解和应用。
四、教学资源本章节的教学资源主要包括以下几种:1.教材:教师准备相关的数学教材,提供理论知识的学习和练习题的练习。
2.参考书:教师提供相关的参考书籍,供学生进一步深入学习和探索。
3.多媒体资料:教师准备相关的多媒体资料,如图片、视频等,用于辅助讲解和演示。
4.实验设备:教师准备相关的实验设备,供学生进行实验操作和实践。
五、教学评估本章节的教学评估主要包括以下几种方式:1.平时表现:教师通过观察和记录学生在课堂上的参与程度、提问回答等情况,评估学生的学习态度和表现。
2.作业:教师通过布置和批改相关的作业,评估学生对知识的理解和应用能力。
3.考试:教师通过安排章节考试或者小测验,评估学生对知识掌握的程度和问题解决的能力。
农夫过河问题一、实验目的掌握广度优先搜索策略,并用队列求解农夫过河问题二、实验内容问题描述:一农夫带着一只狼,一只羊和一颗白菜,身处河的南岸,他要把这些东西全部运到北岸,遗憾的是他只有一只小船,小船只能容下他和一件物品。
这里只能是农夫来撑船,同时因为狼吃羊、羊吃白菜、所以农夫不能留下羊和狼或羊和白菜在河的一边,而自己离开;好在狼属肉食动物,不吃白菜。
农夫怎么才能把所有的东西安全运过河呢?实验要求如下:(1)设计物品位置的表示方法和安全判断算法;(2)设计队列的存储结构并实现队列的基本操作(建立空队列、判空、入队、出队、取对头元素),也可以使用STL中的队列进行代码的编写;(3)采用广度优先策略设计可行的过河算法;(4)输出要求:按照顺序输出一种可行的过河方案;提示:可以使用STL中的队列进行代码编写。
程序运行结果:二进制表示:1111011011100010101100011001,0000三、农夫过河算法流程⏹Step1:初始状态0000入队⏹Step2:当队列不空且没有到达结束状态1111时,循环以下操作:⏹队头状态出队⏹按照农夫一个人走、农夫分别带上三个物品走,循环以下操作:⏹农夫和物品如果在同一岸,则计算新的状态⏹如果新状态是安全的并且是没有处理过的,则更新path[ ],并将新状态入队⏹当状态为1111时,逆向输出path[ ]数组附录一:STL中队列的使用注:队列,可直接用标准模板库(STL)中的队列。
需要#include<queue>STL中的queue,里面的一些成员函数如下(具体可以查找msdn,搜索queue class):front:Returns a reference to the first element at the front of the queue.pop:Removes an element from the front of the queuepush:Adds an element to the back of the queueempty:Tests if the queue is empty三、实验代码FarmerRiver.H#ifndef FARMERRIVER_H#define FARMERRIVER_Hint FarmerOnRight(int status); //农夫,在北岸返回1,否则返回0int WorfOnRight(int status); //狼int CabbageOnRight(int status); //白菜int GoatOnRight(int status); //羊int IsSafe(int status); //判断状态是否安全,安全返回1,否则返回0void FarmerRiver();#endifSeqQueue.h#ifndef SEQQUEUE_H#define SEQQUEUE_Htypedef int DataType;struct Queue{int Max;int f;int r;DataType *elem;};typedef struct Queue *SeqQueue;SeqQueue SetNullQueue_seq(int m);int IsNullQueue_seq(SeqQueue squeue);void EnQueue_seq(SeqQueue squeue, DataType x);void DeQueue_seq(SeqQueue);DataType FrontQueue_seq(SeqQueue);#endifFarmerRiver.c#include <stdio.h>#include <stdlib.h>#include "SeqQueue.h"#include "FarmerRiver.h"int FarmerOnRight(int status) //判断当前状态下农夫是否在北岸{return (0!=(status & 0x08));}int WorfOnRight(int status){return (0!=(status & 0x04));}int CabbageOnRight(int status){return (0!=(status & 0x02));}int GoatOnRight(int status){return (0!=(status & 0x01));}int IsSafe(int status) //判断当前状态是否安全{if ((GoatOnRight(status)==CabbageOnRight(status)) && (GoatOnRight(status)!=FarmerOnRight(status)))return (0); //羊吃白菜if ((GoatOnRight(status)==WorfOnRight(status)) && (GoatOnRight(status)!=FarmerOnRight(status))) return 0; //狼吃羊return 1; //其他状态是安全的}void FarmerRiver(){int i, movers, nowstatus, newstatus;int status[16]; //用于记录已考虑的状态路径SeqQueue moveTo;moveTo = SetNullQueue_seq(20); //创建空列队EnQueue_seq(moveTo, 0x00); //初始状态时所有物品在北岸,初始状态入队for (i=0; i<16; i++) //数组status初始化为-1{status[i] = -1;}status[0] = 0;//队列非空且没有到达结束状态while (!IsNullQueue_seq(moveTo) && (status[15]==-1)){nowstatus = FrontQueue_seq(moveTo); //取队头DeQueue_seq(moveTo);for (movers=1; movers<=8; movers<<=1)//考虑各种物品在同一侧if ((0!=(nowstatus & 0x08)) == (0!=(nowstatus & movers)))//农夫与移动的物品在同一侧{newstatus = nowstatus ^ (0x08 | movers); //计算新状态//如果新状态是安全的且之前没有出现过if (IsSafe(newstatus)&&(status[newstatus] == -1)){status[newstatus] = nowstatus; //记录新状态EnQueue_seq(moveTo, newstatus); //新状态入队}}}//输出经过的状态路径if (status[15]!=-1){printf("The reverse path is: \n");for (nowstatus=15; nowstatus>=0; nowstatus=status[nowstatus]){printf("The nowstatus is: %d\n", nowstatus);if (nowstatus == 0)return;}}elseprintf("No solution.\n");}Sequeue.c#include <stdio.h>#include <stdlib.h>#include "SeqQueue.h"SeqQueue SetNullQueue_seq(int m){SeqQueue squeue;squeue = (SeqQueue)malloc(sizeof(struct Queue));if (squeue==NULL){printf("Alloc failure\n");return NULL;}squeue->elem = (int *)malloc(sizeof(DataType) * m);if (squeue->elem!=NULL){squeue->Max = m;squeue->f = 0;squeue->r = 0;return squeue;}else free(squeue);}int IsNullQueue_seq(SeqQueue squeue){return (squeue->f==squeue->r);}void EnQueue_seq(SeqQueue squeue, DataType x) //入队{if ((squeue->r+1) % squeue->Max==squeue->f) //是否满printf("It is FULL Queue!");else{squeue->elem[squeue->r] = x;squeue->r = (squeue->r+1) % (squeue->Max);}}void DeQueue_seq(SeqQueue squeue) //出队{if (IsNullQueue_seq(squeue))printf("It is empty queue!\n");elsesqueue->f = (squeue->f+1) % (squeue->Max); }DataType FrontQueue_seq(SeqQueue squeue) //求队列元素{if (squeue->f==squeue->r)printf("It is empty queue!\n");elsereturn (squeue->elem[squeue->f]);}main.c#include <stdio.h>#include <stdlib.h>#include "FarmerRiver.h"int main(void){FarmerRiver();return 0;}实验结果:四、实验总结。
1、问题描述从前,一个农夫带着一只狼,一只羊和一棵白菜要河(注意该狼被农夫训服了,但还会吃羊)。
他要将所有东西安全的带到河的对岸,不幸的是河边只有一条船,只能装下农夫和他的一样东西,并且农夫必须每次都随船过,因为只有他能撑船。
在无人看管的情况下,狼要吃羊,羊要吃白菜,因此,农夫不能在河的某边岸上单独留下狼和羊,也不能单独留下羊和白菜。
那么农夫如何才能使三样东西平安过河呢?2、需求分析1)、农夫必须把狼,羊,白菜全部都载过河,且一次只能载一个;2)、要求狼和羊不能单独在一起,羊和白菜也不能单独在一起,即要么羊单独在河的一边,要么羊和农夫在一起。
3、系统概述设计对于上述情况,可以将河的两岸抽象成成数学问题,即将河的本岸抽象成数字‘0’,将对岸抽象成‘1’;且将狼,羊,白菜,农夫,分别抽象成数字‘0’,‘1’,‘2’,‘3’。
而用数组a[i][j](取值只能为0和1)表示第i次运载是,j (j=0,1,2,3。
分别表示狼,羊,白菜,农夫)所在的位置。
而用b[i]表示第i 次运载时船上运载的东西(因为农夫每次都必须在船上,所以不用记录,除非穿上只有农夫一人)。
如此一来,是否全部过河的问题就转化为判断a[i][0],a[i][1],a[i][2],a[i][3]是否全为1了,即相加之和是否为4的问题了;而四者中的两者是否能在一起的问题就转化它们各自的a[i][j]是否相等的问题了。
4、系统详细设计创建一个数组a[MAXTIMES][4]用于存放农夫,狼,羊,白菜的位置,用0表示本岸,1表示对岸;b[MAXTIMES]用于存放狼,羊,白菜,农夫的编号; 0: 狼,1:羊,2:白菜,3:农夫;编写一个递归函数Ferry(int ferryTimes),其中ferryTimes为渡河次数,在函数中,应考虑3个问题:1)、用a[ferryTimes][0] + a[ferryTimes][1] + a[ferryTimes][2] + a[ferryTimes][3] == 4语句判断是否全部到达对岸,如果是,则直接输出结果,否则,考虑第二个问题;2)、狼和羊是否单独在一起,羊和白菜是否单独在一起,用语句a[ferryTimes][1] != a[ferryTimes][3] && (a[ferryTimes][2] == a[ferryTimes][1] || a[ferryTimes][0] == a[ferryTimes][1])来实现;3)、如果上两个条件都不满,则可执行运输的动作,但每次都应考虑,该运输情况以前是否执行过(即两岸以及船上的东西以及各自位置和以前完全相同),如果没被执行过,则可以保存此时四者各自的状态,并递归的进行下一次运载。
目录引言 (2)1 问题描述 (2)基本要求 (2)2.1为农夫过河问题抽象数据模型体会数据模型在问题求解中的重要性; (2)2.2设计一个算法求解农夫过河问题,并输出过河方案; (2)3 概要设计 (2)3.1数据结构的设计。
(2)3.1.1农夫过河问题的模型化 (2)3.1.2 算法的设计 (3)4、运行与测试 (5)5、总结与心得 (6)附录 (6)参考文献 (12)引言所谓农夫过河问题是指农夫带一只狼、一只羊和一棵白菜在河南岸, 需要安全运到北岸。
一条小船只能容下他和一件物品, 只有农夫能撑船。
问农夫怎么能安全过河, 当然狼吃羊, 羊吃白菜, 农夫不能将这两种或三种物品单独放在河的一侧, 因为没有农夫的照看, 狼就要吃羊, 而羊可能要吃白菜? 这类问题的实质是系统的状态问题, 要寻求的是从初始状态经一系列的安全状态到达系统的终止状态的一条路径。
1 问题描述一个农夫带一只狼、一棵白菜和一只羊要从一条河的南岸过到北岸,农夫每次只能带一样东西过河,但是任意时刻如果农夫不在场时,狼要吃羊、羊要吃白菜,请为农夫设计过河方案。
基本要求2.1为农夫过河问题抽象数据模型体会数据模型在问题求解中的重要性;2.2设计一个算法求解农夫过河问题,并输出过河方案;3 概要设计3.1 数据结构的设计。
3.1.1农夫过河问题的模型化分析这类问题会发现以下特征:有一组状态( 如农夫和羊在南, 狼和白菜在北) ; 从一个状态可合法地转到另外几个状态( 如农夫自己过河或农夫带着羊过河) ; 有些状态不安全( 如农夫在北, 其他东西在南) ; 有一个初始状态( 都在南) ; 结束状态集( 这里只有一个, 都在北) 。
问题表示: 需要表示问题中的状态, 农夫等位于南P北( 每个有两种可能) 。
可以采用位向量, 4 个二进制位的0P1 情况表示状态, 显而易见, 共24= 16种可能状态。
从高位到低位分别表示农夫、狼、白菜和羊。
农夫过河问题的算法与实现院(系)名称专业班级学号学生姓名指导教师年月日目录引言 (1)一.问题的描述 (2)二.需求分析 (3)三.概要设计 (4)3.1数据结构的设计 (4)3.2算法的设计 (5)3.3抽象数据类型的设计 (5)四.详细设计 (6)4.1算法的主要思想 (6)4.2主要功能函数设计 (7)4.3算法的实现 (7)五.代码实现 (10)六.测试与运行 (18)6.1测试工具 (18)6.2运行结果 (18)七.总结与体会 (19)八.参考文献 (20)农夫过河问题的算法与实现引言所谓农夫过河问题是指农夫带一只狼、一只羊和一棵白菜在河南岸, 需要安全运到北岸。
一条小船只能容下他和一件物品, 只有农夫能撑船。
问农夫怎么能安全过河, 当然狼吃羊, 羊吃白菜, 农夫不能将这两种或三种物品单独放在河的一侧, 因为没有农夫的照看, 狼就要吃羊, 而羊可能要吃白菜? 这类问题的实质是系统的状态问题, 要寻求的是从初始状态经一系列的安全状态到达系统的终止状态的一条路径.一.问题的描述任何的实际问题,都可以抽象成固定的数学模型,然后再根据模型解决问题。
这样就可以不考虑繁琐的实际过程,从而简化问题。
在我们的问题中,过河与没过河是两种不同的状态。
农夫、狼、羊和菜,分别处于这两种状态。
而,如果把他们看成一个系统,则农夫、狼、羊和菜的不同状态组合成系统的2的4次方种,即16种状态。
但在系统的16种状态中,有些不满足题给条件,应给予剔除。
剔除的判断条件:羊跟狼、菜状态相同,且不同于农夫的状态。
当我们挑选好一系列系统的合法状态后,我们的问题就清晰了很多。
我们不妨设,没过河状态为0,过河为1。
我们的问题就抽象为,系统从初始状态(0000),经过有限的合法状态,到达最终状态(1111)的过程。
系统不同的合法状态之间,可能,有的有路,有的则不能到达。
具体的判断条件是,农夫可以与一件物品同时边,或自己单独变。
根据这一个条件,我们可以抽象出一个图来:系统的每一种状态视为一个节点,满足条件的节点间有一条路。
农夫过河实验报告
实验报告:农夫过河
实验目的:
1. 了解农夫过河问题的规则和约束条件;
2. 分析农夫过河问题的求解思路;
3. 实现农夫过河问题的求解算法。
实验原理:
农夫过河问题是一种经典的逻辑推理问题,涉及农夫、狼、羊和菜四个角色过河的情景。
根据约束条件,农夫每次只能带一种物品过河,而且农夫不能将狼和羊、羊和菜同时留在岸边,否则会发生危险。
实验步骤:
1. 设计数据结构表示问题的状态,如使用二进制位表示农夫、狼、羊和菜的位置;
2. 使用递归算法实现问题的解法,通过深度优先搜索遍历所有可能的状态,并根据约束条件进行剪枝;
3. 运行程序,输出农夫过河的解答序列。
实验结果:
根据实验步骤中的算法和程序设计,成功地求解了农夫过河问题,并输出了正确的解答序列。
实验结果表明,农夫可以经过
一系列合法的操作,将狼、羊和菜都安全地带过河。
实验结论:
通过本次实验,我们深入理解了农夫过河问题的规则和约束条件,并成功地实现了问题的求解算法。
实验结果表明,农夫过河问题有多种可能的解法,但只有符合约束条件的解才是正确的解答。
这个经典的逻辑推理问题在计算机科学中具有重要的意义,可以用于教学和娱乐等领域。
农夫、狼、⽺、菜过河简单算法分析农夫、狼、⽺、菜过河简单算法分析陌上花飘落0⼈评论9720⼈阅读2015-02-28 11:04:421、问题描述⼀个农夫在河边要过河,但是他带着⼀匹狼、⼀只⽺和⼀颗⽩菜。
他需要⽤船将这三样东西运⾄对岸,然⽽,这艘船的空间有限,只容得下他⾃⼰和另⼀样东西(或狼或⽺或⽩菜)。
若他不在场看管的话,狼就会吃⽺,⽺就会去吃⽩菜。
此⼈如何才能过河。
2、问题分析根据题意我们可以得出⼀下结论:(1)三样东西必须都过河,但是⼀次只能载⼀个;(2)如果农夫不在场,那么狼会吃⽺,⽺会吃⽩菜。
3、算法概述对于此题,抽象成编程问题来解决。
将⼈、狼、⽺、菜在此岸都设为1,当成功渡河后则都为0。
⽤类bankState来表⽰河岸的状态,⽤类boatState来表⽰船上的状态。
⽤time来表⽰运载的次数。
如此⼀来,问题转化成判断所有的1是不是都转化为0了,以及其中两个在⼀起时是否合法的问题了。
4、详细设计按照⼈、狼、⽺、菜的顺序描述,为了描述⽅便,假设在河岸A,要过河到达到河岸B。
其中,⼈、狼、⽺、菜只能为0或1,其他值都是⾮法的。
新建类boatState⽤来描述船上的状态,可知船上的状态只有4种可能,即⼈⾃⼰、⼈和狼、⼈和⽺、⼈和菜,⽤实例化对象boat[4]来表⽰这四种状态。
新建类bankState⽤来描述河岸的状态,实例化对象stateA[record]⽤来记录河岸A的状态,stateB[record]⽤来记录河岸B 的状态,其中record为可能需要的最⼤次数。
初始化stateA[0]值为{1,1,1,1},实例化boat[4],其可取值为{1,0,0,0}、{1,1,0,0}、{1,0,1,0}、{1,0,0,1}⽤于判断船上状态是否合法。
开始渡河。
依次判断是否已经全为0,即是否已经成功渡河。
若成功,则打印过河过程中河岸A的所有状态,否则继续判断。
判断状态是否合法,状态是否出现过已经,若都通过,则进⾏渡河操作,开始进⾏递归。
基于C++的农夫过河问题算法设计与实现⽅法本⽂实例讲述了基于C++的农夫过河问题算法设计与实现⽅法。
分享给⼤家供⼤家参考,具体如下:问题描述:⼀个农夫带着—只狼、⼀只⽺和—棵⽩菜,⾝处河的南岸。
他要把这些东西全部运到北岸。
他⾯前只有⼀条⼩船,船只能容下他和—件物品,另外只有农夫才能撑船。
如果农夫在场,则狼不能吃⽺,⽺不能吃⽩菜,否则狼会吃⽺,⽺会吃⽩菜,所以农夫不能留下⽺和⽩菜⾃⼰离开,也不能留下狼和⽺⾃⼰离开,⽽狼不吃⽩菜。
请求出农夫将所有的东西运过河的⽅案。
实现上述求解的搜索过程可以采⽤两种不同的策略:⼀种⼴度优先搜索,另⼀种深度优先搜索。
这⾥介绍在⼴度优先搜索⽅法中采⽤的数据结构设计。
程序源码:/************************************************ 农夫过河问题(P64 队列的应⽤)* 约定:⽤四位⼆进制数分别顺序表⽰农夫、狼、⽩菜和⽺的状态* 即:{dddd} <=> {Farmer, Wolf, Cabbage, Goat} 其中:d={0,1}* 说明:0表⽰在东岸 1表⽰在西岸,初始状态为0000,终⽌状态为1111************************************************/#include<stdio.h>#include<stdlib.h>#define MAXSIZE 16typedef int EntryType;typedef struct queue{EntryType data[MAXSIZE];int front,rear; //front队头,rear队尾}SeqQueue, * SeqQueuePtr;// 创建空队列SeqQueuePtr create_sequeue(void){SeqQueuePtr pque;pque = (SeqQueuePtr)malloc(sizeof(SeqQueue));if(pque){pque->front = 0;pque->rear = 0;}else{printf("Error: malloc() failed, out of memory!\n");}return(pque);}int is_queEmpty(SeqQueuePtr pque){return( pque->front == pque->rear );}int is_queFull(SeqQueuePtr pque){return( (pque->rear+1)%MAXSIZE == pque->front);}// ⼊队int enqueue(SeqQueuePtr pque, EntryType x){if(is_queFull(pque)){printf("Queue Overflow Error: trying to add an element onto a full queue\n");return 1;}else{pque->data[pque->rear] = x;pque->rear = (pque->rear + 1) % MAXSIZE;return 0;}}// 队⾸元素出队(返回0表⽰出队异常,出队操作前队列为空)int dequeue(SeqQueuePtr pque, EntryType * e){if(is_queEmpty(pque)){printf("Empty Queue.\n");return 0;}else{*e = pque->data[pque->front];pque->front = (pque->front + 1) % MAXSIZE;return 1;}}int is_farmer_crossed(int state){return ((state & 0x08) != 0);}int is_wolf_crossed(int state){return ((state & 0x04) != 0);}int is_cabbage_crossed(int state){return ((state & 0x02) != 0);}int is_goat_crossed(int state){return ((state & 0x01) != 0);}// 若状态相容(安全)则返回1,否则返回0int is_safe(int state){if((is_goat_crossed(state) == is_cabbage_crossed(state)) &&(is_goat_crossed(state) != is_farmer_crossed(state))) // ⽺菜同岸且农夫不在场return(0);if((is_goat_crossed(state) == is_wolf_crossed(state)) &&(is_goat_crossed(state) != is_farmer_crossed(state))) // 狼⽺同岸且农夫不在场return(0);return(1);}void river_crossing_problem(){int route[16]; // 记录已经考虑过的状态int state; // 记录当前时刻的状态(状态编号的⼆进制形式即状态本⾝)int aftercross; // 记录渔夫当前的选择(渡河对象)会导致的结果状态int passenger; // 临时变量,⽤于表达农夫的选择(对应⼆进制位为1表⽰选中该乘客)int results[16]={0}; // 输出结果int counter, i;SeqQueuePtr states_que; //states_que = create_sequeue(); // 创建“状态”队列enqueue(states_que,0x00); // 初始状态0000⼊队for(int i = 0; i < 16; i++){route[i] = -1;}//route[0] = 0;while(!is_queEmpty(states_que) && (route[15] == -1)){if( !dequeue(states_que, &state) ){printf("Error: dequeue() - the queue is empty\n");}// 依次考虑农夫可能的选择:携带⽺、⽩菜和狼,以及农夫只⾝渡河for( passenger = 1; passenger<= 8; passenger <<= 1 ){// 由于农夫总是在过河,随农夫过河的也只能是与农夫同侧的东西if(((state & 0x08) != 0) == ((state & passenger) != 0)){// 如果农夫与当前乘客在河岸的同⼀侧aftercross = state^( 0x08|passenger ); // 渡河后的情况if(is_safe(aftercross) && (route[aftercross] == -1)){// 如果渡河后状态安全,则将其状态⼊队route[aftercross] = state; // 将当前状态的索引记录到路径数组中(下标索引为后续状态值) enqueue(states_que, aftercross);}}}//end for()}//end while()// 输出过河策略:0表⽰在东岸 1表⽰在西岸,初始状态为0000,终⽌状态为1111if(route[15] != -1){//printf("The reverse path is:\n");counter = 0;for(state = 15; state != 0; state = route[state]){//printf("The state is: %d \n",state);results[counter] = state;counter++;//if(state == 0) return;}for(i = 0; i< counter; i++){state= results[i];aftercross = results[i+1];if(state & 0x08){printf("农夫从东岸到西岸:");}else{printf("农夫从西岸到东岸:");}switch(state^aftercross ){case 12:printf("把狼带过河\n");break;case 10:printf("把菜带过河\n");break;case 9:printf("把⽺带过河\n");break;default:printf("什么也不带\n");break;}}}else{printf("No solution for this problem.\n");}}int main(void){river_crossing_problem();system("pause");return 0;}运⾏结果:希望本⽂所述对⼤家C++程序设计有所帮助。
《农夫的难题》教案
教学方法:体验学习、合作学习,探究学习。
教学重难点:
重点:描述算法。
难点:用PythOn程序语言来描述算法。
教学安排:
给学生发送文件:农夫过河游戏.swf,导学电子书,文本“aaa.txt”
一、引入课题:
今天上的上一节程序课,我们却要从一个古老的故事开始。
从前有个农夫,要带着一条狼、一只羊和一筐白菜过河。
可是船太小,一次只能带一样到河对岸去。
农夫思来想去,找不到一个两全之策。
聪明的你能帮忙设计一个过河方案吗?二、在游戏中描述你的算法。
学生打开游戏“农夫过河游戏.swf”,描述算法
引出算法的概念。
算法--就是解决问题的方法和步骤。
三、用流程图来描述算法
向学生发送“流程图.PPT”
学生完成流程图的填充。
四、自主学习。
向学生发送电子书。
分小组学习。
五、作业
打开作业:
将桌面上的aaa∙txt文件中的内容复制粘贴到PythOn窗口中,补充修改完整,并调试运行,直到得出正确的结果。
有问题可小组讨论。
六、点评作业
七、再完成作业并提交。
八、评介小结
提问环节
总结收获环节
九、比较教材上的程序和我们的程序之不同点,让学生提高对PythOn的语法的认识。
农夫过河算法实验报告组长:崔俊组员:李琦、郑鸿飞、王琅辉、张育博15.12.29摘要农夫过河问题是应用广度优先搜索和深度优先搜索的典型问题,但这里我们应用了简单的数组,通过层层筛选的手段也解决了同样的问题,其中用到了部分广度优先搜索的思想。
前言农夫过河问题描述:一个农夫带着—只狼、一只羊和—棵白菜,身处河的南岸。
他要把这些东西全部运到北岸。
他面前只有一条小船,船只能容下他和—件物品,另外只有农夫才能撑船。
如果农夫在场,则狼不能吃羊,羊不能吃白菜,否则狼会吃羊,羊会吃白菜,所以农夫不能留下羊和白菜自己离开,也不能留下狼和羊自己离开,而狼不吃白菜。
请求出农夫将所有的东西运过河的方案。
正文1.问题抽象和数据组织农夫过河问题应该应用图的广度优先遍历或者深度优先遍历,但这里我们仅使用简单的线性表——数组,通过多重的条件限制,达成目的。
这里我们同样用0和1代表农夫、狼、羊、白菜在左岸还是在右岸,并规定0在左,1在右,我们的目的便是从0000通过一系列变换到1111。
2.农夫过河算法源代码#include <stdio.h>#define MAX 16typedef struct FWSV{int farmer;int wolf;int sheep;int vegetable;}Item;//函数原型//操作:筛选符合条件的安全的数组成员//操作前:无//操作后:返回安全数组的指针void screen(void);//操作:判断下一个数应该取安全数组中那个数//操作前: 传递一个结构体数组成员//操作后:返回另一个结构体数组指针Item * judge(Item Fwsv);Item safe[MAX];int k = 0; //用于计数safe[]中的总数int main (void){screen();Item * next;Item first,second,end;first = safe[0];end = safe[k];printf("first:0000\n");next = judge(first);for (int count = 0;count <= 6;count++){if (next->farmer + next->wolf + next->sheep + next->vegetable != 0){second = *next;next = judge(second);}elsenext++;}printf("end:1111\n");return 0;}void screen(void){int f = 0,w = 0,s = 0,v = 0;for(f = 0;f < 2;f++){for(w = 0;w < 2;w++){for(s = 0;s < 2;s++){for(v = 0;v < 2;v++){if (!(f != s && (s == w || s == v))){safe[k].farmer = f;safe[k].wolf = w;safe[k].sheep = s;safe[k].vegetable = v;k++;}}}}}}Item * judge(Item Fwsv){Item * next;Item compare[4];next = compare;int x1 = 0;int sum = 0;if (Fwsv.farmer == 0){for (int x = 0;x < k;x++){//把出现过的置零操作if(safe[x].farmer == Fwsv.farmer && safe[x].wolf == Fwsv.wolf && safe[x].sheep == Fwsv.sheep && safe[x].vegetable == Fwsv.vegetable ){safe[x].farmer = 0;safe[x].wolf = 0;safe[x].sheep = 0;safe[x].vegetable = 0;}//筛选出农夫状态值与之前相反的 1变0 0变1if(safe[x].farmer == 1 && (safe[x].farmer + safe[x].wolf + safe[x].sheep + safe[x].vegetable != 4 )){compare[x1] = safe[x];x1++;}}for (int x2 = 0;x2 < 4;x2++){//删除状态值与农夫不同但是改变了的sum = Fwsv.farmer + Fwsv.wolf + Fwsv.sheep + Fwsv.vegetable;if ((Fwsv.farmer != Fwsv.wolf && compare[x2].wolf != Fwsv.wolf) ||(Fwsv.farmer != Fwsv.sheep && compare[x2].sheep != Fwsv.sheep)|| (Fwsv.farmer != Fwsv.vegetable && compare[x2].vegetable != Fwsv.vegetable)|| (Fwsv.farmer != Fwsv.vegetable && compare[x2].vegetable != Fwsv.vegetable)){compare[x2].farmer = 0;compare[x2].wolf = 0;compare[x2].sheep = 0;compare[x2].vegetable = 0;}sum+=2;//对和的限制if(compare[x2].farmer + compare[x2].wolf + compare[x2].sheep + compare[x2].vegetable != sum){compare[x2].farmer = 0;compare[x2].wolf = 0;compare[x2].sheep = 0;compare[x2].vegetable = 0;}}printf("-----------------------------------------\n");for(int x3 = 0;x3 < 4;x3++){if (compare[x3].farmer + compare[x3].wolf + compare[x3].sheep + compare[x3].vegetable != 0){printf("上数与:%d%d%d%d相连\n",compare[x3].farmer,compare[x3].wolf,compare[x3].sheep,compare[x3].veget abl );}}}if (Fwsv.farmer == 1){for (int y = 0;y < k;y++){if(safe[y].farmer == Fwsv.farmer && safe[y].wolf == Fwsv.wolf && safe[y].sheep == Fwsv.sheep && safe[y].vegetable == Fwsv.vegetable ){safe[y].farmer = 0;safe[y].wolf = 0;safe[y].sheep = 0;safe[y].vegetable = 0;}if(safe[y].farmer == 0 && (safe[y].farmer + safe[y].wolf + safe[y].sheep + safe[y].vegetable != 0 )){compare[x1] = safe[y];x1++;}}for (int x2 = 0;x2 < 4;x2++){sum = Fwsv.farmer + Fwsv.wolf + Fwsv.sheep + Fwsv.vegetable;if ((Fwsv.farmer != Fwsv.wolf && compare[x2].wolf != Fwsv.wolf) ||(Fwsv.farmer != Fwsv.sheep && compare[x2].sheep != Fwsv.sheep)|| (Fwsv.farmer != Fwsv.vegetable && compare[x2].vegetable != Fwsv.vegetable)|| (Fwsv.farmer != Fwsv.vegetable && compare[x2].vegetable != Fwsv.vegetable)){compare[x2].farmer = 0;compare[x2].wolf = 0;compare[x2].sheep = 0;compare[x2].vegetable = 0;}}printf("-----------------------------------------\n");for(int x3 = 0;x3 < 4;x3++){if (compare[x3].farmer + compare[x3].wolf + compare[x3].sheep + compare[x3].vegetable != 0){printf("上数与:%d%d%d%d相连\n",compare[x3].farmer,compare[x3].wolf,compare[x3].sheep,compare[x3].vegetable );}}}return next;}3.算法功能说明和流程描述首先我们定义了一个结构体Itemtypedef struct FWSV{int farmer;int wolf;int sheep;int vegetable;}Item;Item中包含了农夫(farmer),狼(wolf),羊(sheep),白菜(vegetable),用来表示农夫、狼、羊、白菜的状态,并作出规定当为0的时候表示在左岸,当为1的时候表示在右岸,我们的目标便是从0000的状态到1111的状态。
班级:姓名:三、巩固拓展---〖算法与程序流程图〗学习任务单1、算法:通俗的说算法就是解决问题的和。
2、一个算法应包含有限的操作步骤,不能是有限的,这是指算法的()特性。
A.输入输出B.确定性C.有穷性D.有效性3、【单选题】在流程图的基本图形中,菱形表示()。
A.开始/结束B.输入/输出C.判断D. 处理4、算法常见的描述方法有:___________________、___________________、伪代码、N—S图、PAD图等。
5、算法的三种描述方法的优势和不足:请将以下词语序号填写(剪切粘贴)到表格合适的位置:1、通俗易懂;2、清晰简洁;3、容易造成歧义;4、容易表达复杂的算法;5、语句一般很长;6、复杂算法比较难清晰表示出来;7、不方便翻译成程序设计语言;8、有利于他们快速过河,情况如下:必须从河上唯一的独木桥过,每次最多两人同行,因为是晚上,每次过桥都需用唯一的一个手电筒,所以手电筒必须要传来传去。
每个同学过桥的速度不同,每次过桥当然以较慢的那个人的速度过桥。
同学1:过桥需要1分钟;同学2:过桥需要2分钟;同学3:过桥需要5分钟;同学4:过桥需要10分钟。
比如,如果同学1与同学4首先过桥,等他们过去时,已经过去了10分钟。
如果让同学4将手电筒送回去,那么等他到达桥的另一端时,总共用去了20分钟。
接下来另外两个同学过桥……这是很慢的。
用流程图描述算法:课中任务:一、情景导入——农夫过河1二、小组合作——农夫过河2四、评价收获---星级(1星完全不知道;2星大部分不知道;3星基本知道;4星大部分知道。
5星完全知道)。
上海工程技术大学
毕业设计(毕业论文)任务书
学院继续教育学院
专业计算机科学与技术
班级学号
学生王俊佶
指导教师张辉
题目农夫过河问题的逻辑建模与程序验证
任务规定
进行日期自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
六、系审批意见
系主任(签名):
七、院领导审核意见
院领导(签名):
八、学生实际完成日期九、同组设计(论文)者。