码迷,mamicode.com
首页 > 其他好文 > 详细

oo第三次总结

时间:2018-05-29 13:15:42      阅读:153      评论:0      收藏:0      [点我收藏+]

标签:自动生成   ali   理解   软件危机   加载   推出   谓词逻辑   推荐   请求   

调研

软件形式化方法最早可追溯到20世纪50年代后期对于程序设计语言编译技术的研究,即J.Backus提出BNF描述Algol60语言的语法,出现了各 种语法分析程序自动生成器以及语法制导的编译方法,使得编译系统的开发从“手工艺制作方式”发展成具有牢固理论基础的系统方法。

形式化方法的研究高潮始于20世纪60年代后期,针对当时所谓“软件危机”,人们提出种种解决方法,归纳起来有两类:一是采用工程方法来组织、管理软件的开发过程;二是深入探讨程 序和程序开发过程的规律,建立严密的理论,以其用来指导软件开发实践。前者导致“软件工程”的出现和发展,后者则推动了形式化方法的深入研究。

 

1940年以前:面向机器

第一次软件危机:结构化程序设计:根本原因就是一些面向过程语言中的goto语句导致的面条式代码,极大的限制了程序的规模。

1950与1960年代:有三个现代编程语言于1950年代被设计出来

1967-1978:确立了基础范式

1980年代:编程语言与之前相较显得更为强大。C++合并了面向对象以及系统程序设计。

1990年代:未见到有什么重大的创新,大多都是以前构想的重组或变化。

规格BUG分析

技术分享图片

规格bug产生的原因

在这几次作业中,规格bug产生的主要原因竟只有两个字----手滑orz,在第十次和第十一次作业中,都有一个方法忘记书写JSF;在第十一次作业中,在requires中将strin打成了stringin,在modifies中将requires中的变量名复制下来时没有删除不等号,在改写方法后仅改写了effect中的内容而忘记删除在改写方法时删除的一些变量,在改写方法后忘记将新加入的变量添加到JSF中,复制JSF的时候忘记删除线程规格部分的说明(疯狂卖蠢,真是给跪了,我觉得我的测试者一定笑开了花orz)。诸如此类的错误直接送出了将近20个点,我想一定是我自作孽不可活吧。

然而发生大量这样的手滑错误,实际上与程序的实现并不无关系,在实现代码的时候,不得不面对:我方法没写出来,我也不知道我该用到什么变量该写点什么效果;第一次代码都写完了,才补写JSF的这两种困境。因此JSF并没有发挥出它真正的功效----并不是现有蛋后有鸡,而是先有鸡后有蛋。对于我来说,JSF在这几次作业中,更多的是为了完成作业才书写的,更多的精力被放在了功能的实现上,验证功能的正确性,尤其是当一个JSF仅占0.6分的情况下,我本人其实并没有把它太当回事(但实际上却为此付出了巨大的代价)。

不推荐的JSF写法

前置条件

@REQUIRES:          startpos!=null; movetowards!=null;

对于int类型的数据,不存在是否等于null的判断,因为作为基本数据类型不会出现null,应该直接对数据大小进行约束,若不约束,应无需赘述。应改进为:

@REQUIRES:          0<=startpos<6400&& 0<=movetowards<6400;

 

@REQUIRES:          reqin != null;

没有判断具体的数据类型,在实现中要求方法传入的是一个Request类型变量,但实际上没有在requires中体现出来,应改为:

@REQUIRES:          reqins instanceof Request && reqin != null;

 

@REQUIRES:\this.origingraph.size>6400&&(int i ; 0<=i <=\this.origingraph.size; \this.origingraph[i].size >6400); 0<=src<6400; 0<=des<6400;

对于数据i的范围没有约束,不符合一阶为谓词逻辑的要求,应改为

@REQUIRES:\this.origingraph.size>6400&&(\all int i ; 0<=i <=\this.origingraph.size; \this.origingraph[i].size >6400); 0<=src<6400; 0<=des<6400;

 

@REQUIRES:          \this.snapshots.size >100; 1<=taxiid <=100;

多个条件需要同时满足时,不应用分号隔开,而应写成一个表达式。应改为:

@REQUIRES:          \this.snapshots.size >100 && 1<=taxiid <=100;

 

 

 

后置条件

@EFFECTS:      \result == 指导书要求的格式化输出;

在能够使用一阶逻辑时使用了自然语言,应改为

@EFFECTS:      \result =="taxi: "+ id +",position:("+ currentpos/80+","+ currentpos%80+"), credit: "+ credit +", state: "+ state;

 

@EFFECTS:     \this.path.contains(strin) == true;

后置条件不全面,对于不删除元素的要求没有写明,无法判断是添加操作还是替换操作,应改为

@EFFECTS:     \this.path.contains(strin) == true && \this.path.size==\old(\this).path.size+1;

 

@EFFECTS:      \this.timestamp == timein ==>\this.updatestate()&&\this.snapshot.updatestate();

在不构成因果关系时,不应使用推出符号,应改为

* @EFFECTS:   \this.timestamp == timein &&\this.updatestate()&&\this.snapshot.updatestate();

 

@EFFECTS:  \this.filename == filenamein;

                          \this.bufWriter == (new BufferedWriter);

在构造对象时,其实是调用了构造方法,应该引用其构造器的规格,应改为

@EFFECTS:  \this.filename == filenamein && \this.bufWriter == BufferedWrite();

 

@EFFECTS:     \result == (fully clone this object) == true;

不应使用连等,应改为

@EFFECTS:     \result == (fully clone this object);

Bug聚集关系

功能性bug的产生原因非常意外的没有和JSF产生联系,在第九次作业中,由于完成的过于匆忙,readme中的说明并不是很详细,甚至出现了错误,导致测试者大佬针对出租车标号,loadfile 文件格式,loadfile中坐标信息等问题频频出手,揍得我哑口无言。在第十次作业中,痛定思痛,好好写了一次readme,但是依旧被抓了readme的语言漏洞。在loadfile文件中倘若不输入红绿灯文件路径,我默认不加载红绿灯文件,视为本次运行不需要任何的红绿灯信息(毕竟指导书真的没说需不需要自动读取orz,而没写就不加载看上去非常合理),但是测试者大佬表示对此无法认同,坚持认为这不是一个feature而是一个bug。在最后一次作业中,测试者大佬再一次显了神通,出现了魔改代码测试法,GUI目测法,还利用超长的loadfile测试出请求时间不相同的错误,非常令人敬佩。

 

体会与感想

撰写规格的时候,应当考虑的重点是能否根据规格正确实现方法,对于必要的约束进行说明,按理来讲,这个步骤应该是放在实现方法之前就已经完成的,但是在学习的过程中,JSF的书写被放在了实现方法之后,但即使这个样子仍然有大量的方法没有得到合理的抽象,可见有效书写JSF的难度所在。

但与此同时,在实验课上,通过JSF实现方法时,也体会到了通过优秀的JSF实现方法的畅快,逻辑清晰,需求明确,写起来如鱼得水,实现正确后直接可以与其他大量的代码配合使用,无需理解全部代码的逻辑,可见JSF在实现多人合作的工程化开发时的重要性。

oo第三次总结

标签:自动生成   ali   理解   软件危机   加载   推出   谓词逻辑   推荐   请求   

原文地址:https://www.cnblogs.com/t68i663/p/9104479.html

(0)
(0)
   
举报
评论 一句话评论(0
登录后才能评论!
© 2014 mamicode.com 版权所有  联系我们:gaon5@hotmail.com
迷上了代码!