JSF生存指南P1

这是OO的第三次博客做业，也是JSFO（面向JSF编程）的第一次博客做业。暗示了咱们面向对象课程已经再向JSF的编写过渡。

不知不觉OO的做业已经写完3/4，那些熬夜赶做业的日子仍然历历在目，仿佛是昨天同样。好在这三次是不用像开始接触多线程那么拼了。

总而言之仍是先把此次做业写完吧。

---

 论规格化设计

 咱们要进行规格化设计，首先得明白什么是规格化设计，为何要规格化设计。通过简单的调查（百度），咱们来谈谈规格化设计。

规格化设计的发展历史

从发展历史谈起，想知道谁首先提出规格设计抽象，规格化抽象的源头，显然是不现实的。毕竟这并不算计算机科学的一个重大发现，拿不到图灵奖的。可是这并不表明规格化设计就不重要。

早在1969年（是的，你没看错，就是1969），已经有人开始提出规格化设计了。来自北爱尔兰贝尔法斯特女王大学的C.A.R.Hoare发表了一篇名为An Axiomatic Basis for Computer Programming（计算机程序的公理基础）的论文。着实让我大吃一惊，规格抽象从如此之早就已经获得人们的重视。这也是我能调查到规格化发展历史中，其被提出至关早的了。

在这篇论文中，Hoare就已经提出了基于“前置后置条件”的接口规格方法。很容易联想到咱们所写的JSF中的requires和effects。因此说这篇论文的发布，能够说是高瞻远瞩的，到如今都很不可思议在1969年，计算机都还没有推广发展的时候，就有人已经开始思考规格化了。在计算机还未普及时就有人提出规格，也从侧面也反映出来规格化设计的重要性。

在这里我特意贴出原文的一部分供你们瞻仰，并借此说明为何规格化设计获得了coder们的重视。其中中文翻译为机翻，帮助理解的。否则贴这么大段英语原文估计没人愿意读。

The most important property of a program is whether it accomplishes the intentions of its user. If these intentions can be described rigorously by making assertions about the values of variables at the end (or at intermediate points) of the execution of the program, then the techniques described in this paper may be used to prove the correctness of the program, provided that the implementation of the pro- gramming language conforms to the axioms and rules which have been used in the proof.

程序最重要的属性是它是否完成了用户的意图。若是能够经过在程序执行结束时（或在中间点）对变量值做出断言来严格描述这些意图，那么本文描述的技术能够用来证实程序的正确性，提供编程语言的实现符合证实中使用的公理和规则。

But the practical advantages of program prov- ing will eventually outweigh the difficulties, in view of the increasing costs of programming error. At present, the method which a programmer uses to convince himself of the correctness of his program is to try it out in particular cases and to modify it if the results produced do not cor- respond to his intentions. After he has found a reasonably wide variety of example cases on which the program seems to work, he believes that it will always work. The time spent in this program testing is often more than half the time spent on the entire programming project; and with a realistic costing of machine time, two thirds (or more) of the cost of the project is involved in removing errors during this phase. The cost of removing errors discovered after a program has gone into use is often greater, particularly in the case of items of computer manufacturer's software for which a large part of the expense is borne by the user. And finally, the cost of error in certain types of program may be almost alculable--a lost spacecraft, a collapsed building, a crashed aeroplane, or a world war. Thus the practice of program proving is not only a theoretical pursuit, followed in the interests of academic respectability, but a serious recommendation for the reduction of the costs associated with programming error.

但鉴于编程错误的成本增长，程序验证的实际优点最终将超过困难。目前，程序员用本身的方法说服本身程序的正确性的方法是在特定状况下尝试并在产生的结果不符合其意图的状况下对其进行修改。在他找到了该程序彷佛可以工做的各类各样的案例以后，他认为它将始终有效。在这个程序测试中花费的时间每每超过整个编程项目花费的时间的一半;而且对机器时间的实际成本计算而言，项目成本的三分之二（或更多）涉及在此阶段消除错误。消除程序投入使用后发现的错误的代价一般更大，特别是在用户承担大部分费用的计算机制造商软件的状况下。最后，某些类型的程序中的错误代价可能几乎是能够下降的 - 一个丢失的航天器，一座倒塌的建筑物，一架坠毁的飞机或世界大战。所以，程序证实的实践不只是理论上的追求，其次是为了学术的可尊重性，而是为减小与程序错误相关的成本而提出的严格建议。

为何规格化获得了你们的重视

在个人理解，Hoare所提出的规格抽象用于保证程序的正确性。虽然使用规格抽象来验证程序正确性须要花费时间，但若是程序投入使用后发现错误，这个代价远比验证所花的时间要大（做为一个北航的学生看到Hoare提出的例子也是倍感亲切）。若是一个航空器的程序中，出现了哪怕一点的纰漏，都会引发无比惨痛的后果。

包括甚至到今天，软件的规模随着软件行业的成熟和发展，软件系统的复杂性使得错误出现的概率大幅提高，而编程错误的成本也不言而喻。为了解决这个问题，使用规格化方法来验证程序的正确性，简化编程过程也是至关有必要的，也获得了很多研究者的承认。

除此以外，一个出色的规格化设计能够帮助程序员理解程序和分割程序。一个企业中不可能只有一个码农。做为一个合做的team，代码须要让团队中的全部人都理解。所以一个好的规格化设计能让他人很容易的理解你的代码，在团队中也十分有用。相信全部码农都但愿阅读到的是风格清晰明确，可读性强的代码，而不肯意阅读乱七八糟，不明就里的代码。

---

规格BUG战

我被报了哪些BUG

三次当中仅有第一次被报了JSF规格BUG，共计13个，可是包括测试者为扣而扣的，如modifies中没有gui，modifies中没有System.out这种莫名其妙的。搞笑的是他备注有问题及时申诉可是一副不想撤的样子。

表格以下：

在第一次就被“狠人”给制裁以后，后面两次我不敢很差好写。第十次做业时我作的第一件事就是把他全部报的地方给修改掉，而后看看还有没有地方写错了。

分析一下这些bug吧，因为个人代码大多数为了美观加了很多空行，这些行数都是过滤掉空行所剩下的行数。能够看出来大部分是没超过50行的。

 requires不完整：这一部分大多为漏写，我在写不少方法的requires时并无考虑太多就写了None，其实是能够填写的。好比这个

　　/**
     * @REQUIRES : None; 
     * @MODIFIES : this.OrderSet;
     * @EFFECTS : (this.OrderSet.contains(taxi_id)) ==> \result == false;
     *            (!this.OrderSet.contains(taxi_id)) ==> (\result == true && this.OrderSet.contains(taxi_id));
     */
    public boolean takeOrder(int taxi_id){
        return this.OrderSet.add(taxi_id);
    }

这是出租车抢单的方法。实际上是能够写requires的，很明显出租车的编号有范围限制，应该为：

　　　/**
     * @REQUIRES : 0 < taxi_id <= 100; 
     * @MODIFIES : this.OrderSet;
     * @EFFECTS : (this.OrderSet.contains(taxi_id)) ==> \result == false;
     *            (!this.OrderSet.contains(taxi_id)) ==> (\result == true && this.OrderSet.contains(taxi_id));
     */
    public boolean takeOrder(int taxi_id){
        return this.OrderSet.add(taxi_id);
    }

固然代码中有很多是这个缘由有雷同，上限为5个。而有意思的是测试的狠人还扣了一个放在了Requires逻辑错误里面。

/**
     * @REQUIRES : 0 <= taxi_id < 100; 
     * @MODIFIES : None;
     * @EFFECTS : true ==> (System.out.println("查询时间：" + (System.currentTimeMillis() - Timer.start_time) / 100 + "(*100ms)") &&
     *                      System.out.println("出租车坐标:(" + taxi.getTaxi_x() + "," + taxi.getTaxi_y() + ")") &&
     *                      System.out.println("出租车状态:" + taxi.getState())) ;
     */
    public void inquiryTaxi(int taxi_id){

（当时Requires是None，重复报了）

然而还有两个我认为是不合理的，所以申请仲裁中，表格里面也打了括号。

 

modifies不完整：也是漏写了，类里面有的属性没有加进去。

effects不完整：同上，没有加入effects中。

 

effects逻辑错误：两个方法都是effects里面改写“==”而我写成了 “=”。有一个我本身都找了很久才发现，只能说是个狠人。

 

分析可知主要问题出自于漏写Requires，这一部分多半处于考虑不周形成的。而其他的也是漏写误写巨多，所以很难从代码行数中总结出来规律。在改完了这些漏写的bug后，后两次并无被爆JSFbug。

可是在写JSF的过程当中，对于行数长的方法，在进行规格抽象时确实感觉到了困难压力，所以多用了天然语言来处理，这也是JSF的问题吧。

我为何会产生规格BUG

先找一些客观缘由。

第一，首先我仍是继承着上一次的观点，在做业都难以保证没有bug的状况下，妄谈优化、优雅，显然是不现实的。虽然这三次做业在难度上确实是下降了，大概是但愿咱们能有更多时间来注重规格化。可是当我拿着第七次做业的代码补充了流量以后，只能看着一个个长的不行的方法对如何写JSF发愁。第七次做业，要咱们实现出租车系统，难度虽然不大，比不上电梯、IFTTT，但也不像后面两次那样随便写写就能完成，因此在第七次我仍是把实现放在优雅以前考虑的。后面的做业在第七次做业的基础上完成，根基不稳，致使JSF根本没法立足。而第九次做业我光是写实现就写到了星期三，下午才开始写JSF，基本上是亡羊补牢。

难度是一部分，若是要写的做业是oo实验课上写的那个银行转帐系统，像这种难度，那我确定能把JSF写的又快又好。而第7、九次做业的难度并无这么友好，能让我把代码实现的更为优雅，多是由于我太菜了。

另一部分是但愿课程组能在第七次做业就开始写JSF，而不是那些设计原则。若是能把JSF写好，代码的风格应该也不会违背那些设计原则。一个超过50行的方法就已经很难写JSF了，更况且当咱们不知道要写JSF时，仅仅要实现功能，像我这种菜鸡写出超过50行的代码可能已是常态了。若是早作打算，从第一次出租车做业就要求JSF，那么设计者在编码时必定会认真考虑每个方法。

第二，写JSF和OO这门课的互测机制有着难以调和的矛盾。这一部分也但愿能在以后作好协调。举个例子，咱们作一个选择题

A.拿高分   B.写出好的代码

确定有很多人比起写好的代码，更注重拿高分。就会出现几种极端的存在：

1.选择A，写代码的时候，类能写多"少"写多"少"，方法能写多"少"写多"少"。到时候别人扣我JSF也扣不了几个。这样的代码固然不多是优雅的。

2.选择A，可是懒得好好写代码。那么怎么拿分呢？找bug以外费时又费力，固然是扣JSF简单方便了。现阶段大多数人的编程水平可能谈不上优雅，跟大佬的更是无法比，JSF难以作到十全十美。测试者对每个方法仔细
“揣摩”，而后凭着“本身的理解”来扣JSF，甚至是为了扣JSF而扣JSF，一扣就是10个20个，美其名曰“怕别人扣个人”。这种人我把其称之为“狠人”。

3.选择A和B。这种人咱们称之为大佬。

4.选择B，好好写代码，方法写的巨多，JSF尽可能认真写。可是到最后碰到“狠人”，方法多，JSF被爆的更多，欲哭无泪。下一次吸收教训也开始扣JSF，逐渐变成“狠人”。

JSF自己主观性就很强，致使恶意扣分也很正常。这三次做业我才发现“狠人”并很多，甚至最后一次“狠人”更是到不可思议。像这种恶意扣JSF，并非止步于全部人都开始好好写JSF，而是扩散成更多人开始恶意扣JSF，不少人开始厌恶JSF甚至闻JSF色变，这显然不是一个好现象。面向对象编程已经开始转变成面向运气编程，若是测试者是好人，那么就能好好存活下去。但凡遇到个“狠人”，就只能默默吃瘪。

当恶意扣JSF滋生时，应该想办法杜绝恶意的扣JSF现象发生。JSF应当是一个帮助别人理解代码，描述方法的工具，而不是做为从中赚取分数的工具。

但愿明年可以好好协调好写JSF和互测JSF的关系，让更多人注重于“我要好好写代码，这样才好写JSF”，而不是“我要好好扣他的JSF”。

接下来是分析下自身缘由，首先是由于时间不足，星期三下午开始写JSF，那么多方法一个一个写，不免会出纰漏，由分析看出来漏写误写居多。另一个我的缘由是由于不重视，心想“你们应该都是扣几个JSF意思意思吧”，结果正好碰到的是“狠人”，结果被扣的一塌糊涂。

固然最大的缘由仍是代码写的差，做为一个大部分时间都要用于实现功能的编程菜鸡，写出来的代码天然跟优雅无关。大量的50行以上代码，以至于不得不用天然语言来写effects。在JSF中出纰漏固然也不是偶然了，虽然这些并无被报BUG。

 

---

JSF改进

虽然规格bug大多数来源于漏写误写，可是能够改进的也很多，好比

1.

　　/**
     * @REQUIRES : None; 
     * @MODIFIES : this.AskList;
     * @EFFECTS : AskList.contains(ask);
     */
    public synchronized void addAsk(Ask ask){
        AskList.add(ask);
    }

能够改成@EFFECTS : AskList.contains(ask) && AskList.size == \old(AskList).size + 1;这样表达添加请求更加明正确。

2.

　　/**
     * @REQUIRES : AskList != {}; 
     * @MODIFIES : this.AskList;
     * @EFFECTS : !AskList.contains(ask);
     *            (\all Ask a; a != ask; AskList.contains(a) == \old(AskList.contains(a));
     */
    public synchronized void deleteAsk(Ask ask){
        AskList.remove(ask);
    }

这个虽然正确，可是过于繁琐，能够该为@EFFECTS : !AskList.contains(ask) && AskList.size == \old(AskList).size - 1; 一样的意思，看上去就简洁不少

3.

　　/**
     * @REQUIRES : 0 <= x1 < 80,0 <= x2 < 80,0 <= y1 < 80,0 <= y2 < 80; 
     * @MODIFIES : None;
     * @EFFECTS : \result == ""+x1+","+y1+","+x2+","+y2;  
     */
    private static String Key(int x1,int y1,int x2,int y2){
        return ""+x1+","+y1+","+x2+","+y2;
    }

这个是用于流量判断的，REQUIRES除了知足 0 <= x1 < 80,0 <= x2 < 80,0 <= y1 < 80,0 <= y2 < 80，以外，应该还要保证(x1,y1),(x2,y2)表示相邻点。

4.

/**
     * @REQUIRES : None; 
     * @MODIFIES : None;
     * @EFFECTS : \result == (\exist int k; 0 <= k < asklist.getSize(); asklist.getAsk(k).equals(ask));
     */
    public synchronized boolean judge_same(Ask ask,AskList asklist)
    {
        Point current_src = ask.getOrigin();
        Point current_dst = ask.getDestination();
        long current_time = ask.getTime();
        
        for(int i = 0 ; i < asklist.getSize() ; i++)
        {
            Ask askInList = asklist.getAsk(i);
            if(askInList.getOrigin().equals(current_src) && askInList.getDestination().equals(current_dst) && askInList.getTime() == current_time)
                return true;
        }
        
        return false;
    }

这里REQUIRES能够添加asklist != {} ;不然与get(i)相矛盾。

5.

大多运用天然语言。若是进行重构不少方法能够再抽象出来，这样写JSF时也不会感受无从下手，从而使用天然语言。

---

 功能BUG与规格BUG的汇集关系

 

 第九次做业被爆的最多，上面已是撤回过3个的数据。第十次的测试者仍是比较善良，至少没有从我JSF中找错误而是只关注功能错误。第十一次做业是遇到的最善良的测试者，一个bug都没有申报（估计是没有测试）。祝好人一辈子平安，OO拿高分。

若是仅从表格来分析，貌似找不到什么汇集点，关系不太紧密。可是若是仔细分析一下，会得出以下结论：扣我JSF扣得最凶的人，BUG也不会放过我（报了3个BUG申诉撤回了一个），这说明测试者是个狠人。而以后遇到的人并无扣JSF，说明仍是很善良的。因此得出以下结论：JSF被扣多少很大部分不是取决于你写的如何，而是取决于你的测试者是个好人仍是狠人。

这三次测试过程我只在第一次扣了被测者3个JSF，以后两次测试均未扣JSF。尤为是第三次测试，由于星期四一天基本是在OS上，晚上还要写OS报告。星期五一天都有课，晚上还有马原。所以只是随便测了一下，申报了一个红绿灯文件没有过滤空格的BUG，结果此次遇到好心人并无对我下手。看来善恶终有报，天道有轮回。

---

 总结与体会

一、这三次做业下来，收获仍是至关多的。最大的收获就是从JSF的书写中，了解了规格化设计，对于什么是“好的代码”有了更深入的理解。虽然本身的代码仍是写的跟那些大佬的代码无法比，甚至说是“真的很烂”也没有问题。可是比起之前写的乱七八糟，冗长繁复的代码好太多了。

据说下次做业是向第三次做业加规格。我回过头回顾一下ALS电梯的代码，发现真是没眼看。有的类内容不多，而scheduler类内容多，并且动辄上百行。这样一份代码想写出JSF基本上是很难的，迫切须要重构。好在我如今是知道从何改起了。

二、还有一个收获是心态。之前的我被扣了一个莫名其妙的bug就会难受好久，如今的我已经不会由于这点分数斤斤计较了，对分数看开了。在被狠人给狠狠制裁一把以后，如今我哪怕被扣了三个bug也能坦然面对。感谢OO让个人心态获得了极好的锻炼。

以前有人问前辈OO须要什么，获得的回答让我受益不浅。

 三、就我最后一次听到几个同窗被扣分数量，发现狠人仍是很多。看来和谐6系仅仅只是老师口中的一句笑谈。和谐6系？不存在的。永远不要相信你的同窗。哪怕在群里说本身多惨，你也不知道他扣了别人多少。

 四、这几回写JSF的思路是这样：

已有代码 

补充代码完成功能

按照代码写JSF

 

显然这样是否是一个好的设计思路。理想中的JSF编写思路应该是：

思考如何完成功能

构思一个大体的JSF

经过构思来编写代码

完善JSF

---

 OO的旅程已经走过四分之三，万里长征已经走完了7500里。但愿能顺利熬过最后几回做业，也但愿和谐6系可以真正的构建起来。只要人人都献出一点爱，世界将会变成美好的人间。