OO第三次博客总结

程序设计规格化的反思与探究

第三阶段的这三次作业，只能说是运气蛮好的了，遇到的测试者与被测者都很友善，没有被挂什么起奇奇怪怪的bug。但确实有一些不好好读指导书，仅凭自己臆断导致的错误。这里回顾一下这三次作业，并对程序设计的规格化，说一下自己的理解。

程序设计的发展

这里部分参考了https://www.cnblogs.com/linhaifeng/articles/6428835.html，可以移步去看一看，对程序设计思想介绍的很详细。

最初的程序设计是直接面向机器的，代码编写困难、可读性差，只能满足计算机发展之初的小规模程序设计。随着对于程序规模的需求，出现了面向过程的设计思想，开发者开始忽略底层实现，进行程序设计。对于面向过程设计思想的变革，goto语句成为讨论的热点。Dijkstra于1968年发表著名的《GOTO有害论》，引起了广泛的关注，结构化的设计思想也在此时应运而生。结构化设计思想，还是一种面向过程的设计思想，结构化指的是通过“自顶向下、逐步细化、模块化”的方法进行程序设计。这种设计思想旨在控制各个模块的程序复杂度，从而保证整体工程的正确性。面向过程的设计存在着扩展性不好的弊病，由此，产生了面向对象的设计模式。程序设计的模块化体现的更为明显，各个部分更加独立，相应地，各个模块之间的交互也更加重要。

无论是面向过程还是面向对象，只要存在模块之间的交互，就必然存在着规格规范的问题。就个人感觉来说，规格是说明了模块的接口，说明了模块的IO要求。所以，规格化是模块化的发展的必然需求。

作业中的规格bug

对不起，没有。

2333，开个玩笑。这几次作业中十几个类，方法数量就多的懒得数了，要说JSF没一点问题，肯定是不可能的。但是测试者都很宽心地没报这些bug。可能和我的想法差不多，JSF的对错难以衡量，可能写出来的JSF已经足以说明程序接口，但是总有没必要的瑕疵照顾不到，被挂出不合理的bug。所以自己感觉JSF只不过起辅助作用，增强代码可读性，指出代码接口。只有一个return的方法，写上三行的JSF，这种感觉真的不好，因为那一句return的可读性更强。

JSF实例分析

找一点自己代码的JSF分析一下，就不分什么好的、不好的了。

Ground.changeRoad()

public static void changRoad(Position pn, int dir) {
    /** @REQUIRES:  \all Position pn, int dir;
     *              pn \in map && dir \in PathDir
     *  @MODIFIED:  this
     *  @EFFECTS :  \all Edge edge;
     *              edge.begin == pn && edge.dir == dir;
     *              edge \in map != edge \in old(map)
     *  @THREAD_EFFECT: \locked(map)
     */

自然语言描述一下，就是传进来一个点和一个方向，就确定了一个地图上唯一的道路，若这个路径在地图上不存在，就打开这条道路；否则，就关闭这条通路。这个JSF的问题是存在考虑不周。在REQUIRES和EFFECTS中，都没有说明当这个边是不合法的边时的处理，比如 pn = (79,79), dir = PathDir.RIGHT。

可以修改为下面这个样子。

public static void changRoad(Position pn, int dir) {
    /** @REQUIRES:  \all Position pn, int dir;
     *              pn \in map && dir \in PathDir
     *  @MODIFIED:  this
     *  @EFFECTS :  \all Edge edge;
     *              edge.begin == pn && edge.dir == dir;
     *              edge.isLegal() ==> edge \in edge \in map != edge \in old(map)
     *              !edge.isLegal() ==> exception_behavior(IllegalEdgeException)
     *  @THREAD_EFFECT: \locked(map)
     */

Position.clone()

    public Position clone() {
    /** @REQUIRES:  NONE
     *  @MODIFIED:  NONE
     *  @EFFECTS:   \result.equals(this)
     */

其实从方法名就知道这个方法在干嘛，但是JSF的描述是有歧义的。因为可能是

        return this;

这样也满足了JSF的描述，但不符合我们的原意。实际上自己的代码是这样写的。这里利用了java中引用相等的含义。

    public Position clone() {
    /** @REQUIRES:  NONE
     *  @MODIFIED:  NONE
     *  @EFFECTS:   \result.equals(this) && this != \result
     */
        return new Position(this.x,this.y);
    }

Taxi.drive()

public long drive(int dir) {
    /** @REQUIRES:  \all int dir;
     *              dir \in PathDir
     *  @MODIFIED:  this.location
     *  @EFFECTS:   \exit Edge edge;
     *              edge.begin == \old(location) && edge.dir == dir;
     *              location == edge.end
     */

JSF出错感觉基本上都是一些考虑不周的问题吧。这里也是一样的。比如当前Taxi在（79，79），传进一个dir=PathDir.RIGHT的情况。事实上这种情况由路径的合理性保证了不会出现。于是，这里写成这样。

public long drive(int dir) {
    /** @REQUIRES:   \all int dir;
     *              dir \in PathDir
     *              &&  \all Edge edge;
     *                  edge.begin == \this.location && edge.dir == dir;
     *                  edge.isLegal()
     *  @MODIFIED:   this.location
     *  @EFFECTS:    \exit Edge edge;
     *              edge.begin == \old(location) && edge.dir == dir;
     *              location == edge.end
     */

JSF分析总结

翻了一下自己代码，也没有其他的有意思的JSF可以分享了，所以就写这么多了，就不强行凑个数了。从上面也可以看出来，JSF出问题一般都是考虑不周，而不是描述有误。所以写规格的话，必须要考虑各种情况；尤其是输入的不合法行。

其他bug反思

这几次的bug，主要问题是大都是读指导书不仔细造成的。

红绿灯变换时间不统一。因为当时感觉每个红绿灯变换不应该是在同一时刻的，所以就每个红绿灯有自己随机出来的变换时间。事实表明，这个是主观臆断了。
等待红绿灯是以100ms为单位的。因为考虑到反正出租车的时间单位是100ms，所以等红绿灯也按照100ms，这样可以让线程调度的效率更高。
在load_file里设置了出租车初始位置后，会导致程序退出。这个bug就比较严重了，是添加出租车红绿灯这个需求的时候，没有考虑到出租车上一个位置由于load_file初始化，与一般情况不一致。这个确实挺严重，看来添需求真的挺麻烦，很容易造成考虑不周的问题。

设计规格和撰写规格的基本思路和感受

由于大部分代码都是第七次作业里写好的，又要在第九次作业加JSF，所以撰写体验相当不好，QAQ。

其实认真写写JSF的话，可以感觉到JSF设计的用意。如果EFFECTS使用符号逻辑描述的话，撰写者就只能从方法调用后的现象来分析问题。比如，\this.index = i 和 \this.index == i 。这两句话，都可以表示方法是用 i 对 index 赋值了。但是角度就不同，前者表述了赋值的过程，而后者陈述了赋值的结果。客观来说，规格就是应该从结果的角度来表述，所以JSF确实可以帮助撰写者思考自己的代码，至少强迫撰写者从更合理的角度思考代码的接口设计。

其他想说的话

从已经结束的OO来说，自己真的被世界温柔以待了。遇到的所有测试者与被测者都会很和气，没有莫名其妙的bug，没有执拗的争辩。emmm，这样想可能大部分同学应该都是这样挺和谐的吧，只不过和谐的互测不会让很多人知道。而不和谐的互测会被吐槽版什么的放得很大，“不加控制的媒体宣传，只会扩大负面影响”，2333。有一互测，测试者最后说，“不用客气，希望代码越写越好，互测心情不要被影响了，加油”，这句话还是让人蛮开心的，所以后来每次测试都会最后加一句这样的祝福。之前听身边的人讨论OO的博弈论、纳什均衡、黑暗森林什么的，对比起来，还是蛮好玩的。