oo第十二次作业

一、调研，然后总结介绍规格化设计的大致发展历史和为什么得到人们的重视

（1）规格化设计的大致发展历史

规格化设计与结构化、模块化设计密不可分，伴随着OOP语言的发展，规格化设计思想逐渐形成体系，慢慢完善。从1940年的面向机器编程，到之后的面向过程编程，逐渐出现了我们现在使用的各个语言的原始版本。而随着代码量的不断增加，程序功能的不断复杂化，简单的面向过程编程不再能够满足人们的需要，因此，出现了结构化程序设计。

在这一过程中，编写代码的人们也注意到了规格的重要性。Edsger Dijkstra 于 1968 发表了著名的《GOTO 有害论》的论文,提出了程序设计中常用的GOTO语句的三大危害:破坏了程序的一致性,程序不易测试,限制了代码优化,引起了长达数年的论战,并由此产生了结构化程序设计方法。结构化程序设计的主要特点是抛弃 goto 语句,采取“自顶向下、逐步细化、模块化”的指导思想。结构化程序设计本质上还是一种面向过程的设计思想,但通过“自顶向下、逐步细化、模块化”的方法,将软 件的复杂度控制在一定范围内,从而从整体上降低了软件开发的复杂度。

在此之后，随着硬件的快速发展，程序的复杂度迎来了再一次的飞跃，由于结构化程序设计的“可扩展性”、“可维护性”不强，已经满足不了快速多变的业务需求，这时出现了面向对象编程。规格化设计也随着面向对象编程的发展而不断完善，Hoare提出了基于“前置后置条件”的接口规格方法。但现在的软件系统越来越复杂，在规模和功能上都有大幅扩展，因此需要发展Hoare的方法以适应新的大规模复杂系统开发。Hoare提出的这个结论为规格化发展起到了奠基作用，也为类中接口的规格化提供了理论基础。

此后，人们不断发展Hoare的理论以适应面向对象的特殊性，Guttag使用抽象的数据类型来降低设计和实现大型软件的复杂度，用代数公理证明规格的正确性。Goguen和Zilles都着重强调代数化方法，使用代数方法验证抽象数据类型的规格化的正确性。使用抽象数据类型的代数规格法虽然可以描述方法之间的相关关系，但是却失去了对单个方法的准确规格定义。

针对各方法的准确规格定义，Meyer提出契约式编程，延续了对方法的精确定义，但其不足是依赖内部状态来体现方法之间的相互依赖。Robert也引入契约来表达接口的前置条件和后置条件，在调用这个接口时可以用前置条件和后置条件来验证正确性。面向对象规格的难点在于方法间的相互影响，人们也尝试界定这种影响。在面向对象语言中，类总能把状态和能改变这些状态的行为放在一起，而实际上这些行为中有一部分行为会改变这些状态，那么对状态没有影响的行为就被界定为没有副作用的方法，即查询方法。查询方法只给出了方法间依赖关系的界定方法，没有给出存在依赖的那些方法的规格解决方案。

（2）为什么得到了人们的重视

从程序设计和开发的角度，规格化设计可以让用例的读者更清楚系统所处的状态，有利于读者对用例的理解，也可以让用例的作者不必将一些实现相关的错误处理细节写入用例当中，而是以前置条件的形式将它们记录在用例当中，未来测试人员可以编写前置条件不满足时的测试用例。此外，在前置条件都满足的情况下，可以根据后置条件查看程序是否达到相应状态或得到相应的结果，为程序的正确性验证提供了高效的方法。

二、规格bug分析

规格bug主要在第九次作业，这也是第一次写规格，写的比较匆忙，一些细节的地方没有注意，有两个EFFECTS不完整是由于用了自然语言，测试者认为太过简略，另外两个requires错误是以对象为传入的参数时应该加上不为空的条件，我在第一次写的时候忽略了这一点，在后两次作业上时间比较充裕，我对自己的规格补充并且完善，不过也是由于遇到比较善良的测试者，没有报一些吹毛求疵的规格bug。总的来说出现规格bug的主要原因还是由于自己不认真对待，一些方法的规格写的比较草率。

三、列举不好写法并给出改进写法

1.

/**
     * @MODIFIES: None;
     * @EFFECTS:
     *\result == array[];
    */
    public CarInformation[] getTaxiStatus(CarInformation[] cars)

这个就是我在第二部分提到的Requires不完整的规格，这个方法是传入当前所有出租车的信息，返回相同具有信息的出租车信息数组，即对出租车建立快照，这部分规格我在一开始写的时候认为Requires不需要限制条件，即为none，但是这种情况需要对传入的数组是否为空进行判断，即改为

/**
     * @REQUIRES: cars!=null && cars.length==100;
     * @MODIFIES: None;
     * @EFFECTS:
     *\result == array[];
    */
    public CarInformation[] getTaxiStatus(CarInformation[] cars)

2.

/**
     * @REQUIRES: lights!=null && gui!=null && map!=null;
     * @MODIFIES: None;
     * @EFFECTS:
     *this.lights = lights;
     *this.gui = gui;
     *this.map = map;
    */
    public Light(LightInformation lights,TaxiGUI gui,Map map)

这个方法是Light类的构造方法，这个规格写的有问题的地方应该是EFFECTS，应该使用布尔表达式进行表达，不应该直接写成赋值的形式，应该改为：

/**
     * @REQUIRES: lights!=null && gui!=null && map!=null;
     * @MODIFIES: None;
     * @EFFECTS:
     *this.lights == lights;
     *this.gui == gui;
     *this.map == map;
    */
    public Light(LightInformation lights,TaxiGUI gui,Map map)

3.

/**
     * @REQUIRES: None;
     * @MODIFIES: None;
     * @EFFECTS:
     *\result == this.number;
    */
    public synchronized int getNumber()

这个方法是获得出租车信息的编号，由于出租车信息在程序中是共享资源，因此这个方法是加了synchronized关键字的，所以还要写Thread_requires和Thread_effects。

/**
     * @REQUIRES: None;
     * @MODIFIES: None;
     * @EFFECTS:
     *\result == this.number;
     * @THREAD_REQUIRES: \locked(this);
     * @THREAD_EFFECTS: \locked();
    */
    public synchronized int getNumber()

4.

/**
     * @REQUIRES: str!=null && gui!=null && cars!=null && graph!=null && print!=null && light!=null && taxis!=null;
     * @MODIFIES: file, map, gui, cars, graph, print, light;
     * @EFFECTS:
     *this.file == new File(str);
     *this.map == map;
     *this.gui == gui;
     *this.cars == cars;
     *this.graph == graph;
     *this.print == print;
     *this.light = light;
     */
    public LoadFile(String str,Map map,TaxiGUI gui,CarInformation[] cars,Graph graph,PrintInformation[] print,Light light,Taxi[] taxis)

这个方法是Loadfile类的构造方法，对于这个方法的后置条件，忽略了文件不存在这一异常情况的结果，应改为

/**
     * @REQUIRES: str!=null && gui!=null && cars!=null && graph!=null && print!=null && light!=null && taxis!=null;
     * @MODIFIES: file, map, gui, cars, graph, print, light;
     * @EFFECTS:
     *this.file == new File(str);
     *(!file.exists()) ==> print "文件不存在";
     *this.map == map;
     *this.gui == gui;
     *this.cars == cars;
     *this.graph == graph;
     *this.print == print;
     *this.light = light;
     */
    public LoadFile(String str,Map map,TaxiGUI gui,CarInformation[] cars,Graph graph,PrintInformation[] print,Light light,Taxi[] taxis)

5.

/**
    * @REQUIRES: None;
    * @MODIFIES: None;
    * @EFFECTS: 
    * The lights change constantly and update the state;
    */
    public void run()

灯的线程的run方法，每隔一段时间修改一次灯的状态，EFFECTS中的自然语言可以用布尔表达式代替

/**
    * @REQUIRES: None;
    * @MODIFIES: None;
    * @EFFECTS: 
    * state==1 ==> state == 0 && lights.getState() == 0;
    * state==0 ==> state == 1 && lights.getState() == 1;
    */
    public void run()

四、功能bug和规格bug在方法上的聚类关系

五、设计规格和撰写规格的基本思路和体会

我像很多同学一样，没有设计规格这一过程，都是先写完代码，debug结束后才进行规格的撰写，不过在后两次作业我对规格和方法进行对照，还是能发现一些代码逻辑或者规格上的问题，直到第六次面向对象实验上机，可以说这时我才体会到规格的用处，根据已写好的规格来编程，效率大大提高，对程序的结构和逻辑也能理解的非常快。

在工程中，在方法头之前的注释中充分说明每个公有方法。对于确保方法能正确执行而必须满足的条件，要说明是由方法还是由客户来负责进行检查。以这种方式，既做了检查又不会重复检查。但在调试过程中，方法应该检查前置条件是否满足。

当使用继承和多态来重写父类中的一个方法时，子类中的方法可能会出现与父类中的方法不一致的问题。前置条件和后置条件可以帮助程序员避免这个问题。后置条件必须适用于子类中方法的所有版本。重写的方法可以添加到后置条件中——即它能做的更多——但不能做的更少。不过重写的方法不能增加其前置条件。换句话说，它不能比基类中的方法要求得更多。总的来说，只有真正参与工程项目中，才能体会到规格的好处。