标签：自动生成 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在实现多人合作的工程化开发时的重要性。
标签：自动生成 ali 理解 软件危机 加载 推出 谓词逻辑 推荐 请求
原文地址：https://www.cnblogs.com/t68i663/p/9104479.html
