标签：end 结构化 jsf lock 增强 img 思路 jpg 设计者
规格化设计的发展历史和重要性：
规格化设计与结构化、模块化设计密不可分。从计算机开始发展以来，随着代码量的不断增加，程序功能的不断复杂化，简单的面向过程编程不再能够满足人们的需要，因此，出现了结构化程序设计。
在之后程序设计思想的不断发展过程中，规格越来越显得重要。Dijkstra 于 1968 发表了著名的《GOTO 有害论》的论文,提出了程序设计中常用的GOTO语句的三大危害,引起了长达数年的论战,并由此产生了结构化程序设计方法。第一个结构化的程序语言Pascal也在此时诞生,并迅速流行起来。
在此之后，随着硬件的快速发展，程序的复杂度迎来了再一次的飞跃，而这时出现了面向对象编程。此后规格化得到了人们越来越多的重视，因为其可以帮助设计者更好的设计自己的程序，避免在设计过程中产生严重错误，同时也能够增强程序的可维护性。
作业中的规格BUG及出现原因：
列举不好的前后置条件并给出改进写法：
1. 前置条件
(1)
/**
* @REQUIRES: None;
* @MODIFIES: credits;
* @EFFECTS: credits == \old(credits)+x;
*/
改进写法：由于出租车作业中出租车的信用只可能增加，所以这个函数中x的值只能为正数，需要在Requires中限制x为正数，改进为：
/**
* @REQUIRES: x>0;
* @MODIFIES: credits;
* @EFFECTS: credits == \old(credits)+x;
*/
(2)
/**
* @REQUIRES: (\all int i; 0 <= i < 80; m[i].length() == 80 );
* @MODIFIES: map;
* @EFFECTS: map == m;
*/
改进写法：由于地图是80X80的数组，所以既要判断传入数组的行数为80，又要判断其列数为80。Requires中只进行了每行列数的判断，还需要限制行数为80行，改进为：
/**
* @REQUIRES:
(\all int i; 0 <= i < 80; m[i].length() == 80 )&&(m.length()==80);
* @MODIFIES: map;
* @EFFECTS: map == m;
*/
(3)
/**
* @REQUIRES: (i>=0 && i<80) && (t>0) && (g!=null) && (p!=null);
* @MODIFIES:
* System.out, id, status, time, x, y, reqID, reqSet, posSet;
* @EFFECTS:
* Initial the position and state of a special taxi;
*/
改进写法：这是可追踪出租车构造函数的JSF，由于可追踪出租车的序号为0-29，因此Requires中i的范围应该为[0,30]，改进为：
/**
* @REQUIRES: (i>=0 && i<30) && (t>0) && (g!=null) && (p!=null);
* @MODIFIES:
* System.out, id, status, time, x, y, reqID, reqSet, posSet;
* @EFFECTS:
* Initial the position and state of a special taxi;
*/
(4)
/**
* @REQUIRES: (0<=x1<80) && (0<=y1<80) && (0<=x2<80) && (0<=y2<80) && (count>0);
* @MODIFIES: flow, initial, System.out;
* @EFFECTS:
*count>=0 ==> flow[x1*80+y1][x2*80+y2]== count;
*count>=0 ==> flow[x2*80+y2][x1*80+y1]== count;
*count>=0 ==> initial.contains(x1);
*count>=0 ==> initial.contains(y1);
*count>=0 ==> initial.contains(x2);
*count>=0 ==> initial.contains(y2);
*count>=0 ==> initial.contains(count);
改进写法：在这里Requires和Effects中count的取值产生了冲突，其实count是否为0并不影响程序正确执行，但是为了JSF的一致，还是要把Requires改进为：
/**
* @REQUIRES: (0<=x1<80) && (0<=y1<80) && (0<=x2<80) && (0<=y2<80) && (count>=0);
* @MODIFIES: flow, initial, System.out;
* @EFFECTS:
*count>=0 ==> flow[x1*80+y1][x2*80+y2]== count;
*count>=0 ==> flow[x2*80+y2][x1*80+y1]== count;
*count>=0 ==> initial.contains(x1);
*count>=0 ==> initial.contains(y1);
*count>=0 ==> initial.contains(x2);
*count>=0 ==> initial.contains(y2);
*count>=0 ==> initial.contains(count);
(5)
/**
* @REQUIRES: x!=null;
* @MODIFIES: queue;
* @EFFECTS:
*queue.contains(x);
改进写法：这个函数是把请求x加入到队列中，在这里还需要对请求的类别进行判断，即只把乘客请求加入到队列中，不用管开关路请求，将其修改为：
/**
* @REQUIRES: (x!=null)&&(x.gettype()==0);
* @MODIFIES: queue;
* @EFFECTS:
*queue.contains(x);
2. 后置条件
(1)
/**
* @REQUIRES: None;
* @MODIFIES: None;
* @EFFECTS: /result == map;
*/
改进写法：这个函数是返回地图数组，由于地图在程序中是共享资源，因此这个方法是加了synchronized关键字的，所以还要写Thread_requires和Thread_effects。
/**
* @REQUIRES: None;
* @MODIFIES: None;
* @EFFECTS: /result == map;
* @THREAD_REQUIRES: \locked(this);
* @THREAD_EFFECTS: \locked();
*/
(2)
/**
* @REQUIRES: (x!=null)&&(x.gettype()==0);
* @MODIFIES: queue;
* @EFFECTS: Append the request to the queue;
改进写法：这个函数是把用户请求x加入到队列中，Effects是比较容易使用布尔表达式的，因此最好把自然语言写为布尔表达式，将其修改为：
/**
* @REQUIRES: (x!=null)&&(x.gettype()==0);
* @MODIFIES: queue;
* @EFFECTS:
* ! (\old(queue).contains(x)) ==> queue.contains(x);
* queue.size() == \old(queue).size()+1;
(3)
/**
* @REQUIRES: new File(s).isFile() ;
* @MODIFIES: map;
* @EFFECTS:
* Parse the map and check it;
改进写法：这个函数接收一个文件的路径，然后从该文件中提取地图信息，当地图信息发生错误，抛出异常，因此在Effects中要有关于异常的Effects：
/**
* @REQUIRES: (x!=null)&&(x.gettype()==0);
* @MODIFIES: queue;
* @EFFECTS:
* Parse the map and check it;
* (\exist int i; 0<=i<=map.length,0<=j<=map[i].length; map[i][j]<0) ==> exceptional_behavior(InvalidException);
功能BUG与规格BUG的内聚关系：
心得体会：
个人写规格的基本思路就是，先写方法再写规格，至于为什么这么做，在下文有说。首先根据方法对参数的要求来写Requires，再从方法中找到会被改变的类属性，以此来写Modifies，最后用自然语言或者布尔表达式（尽可能用布尔表达式）来写方法的Effects。除此之外还要注意同步方法和抛出异常方法的规格书写。
这三次作业给我最大的感受就是写代码的难度比前几次作业要简单，但是相应地要花部分时间在写规格上面。写规格这个作业的出发点是好的，就是为了让我们养成良好的写代码的习惯，增强代码的可读性和维护性等。但是在现阶段的作业来说，在测试别人的代码时，读规格除了检查JSF是否有BUG之外个人感觉作用不大。对于那些行数比较少的方法，读规格和读代码的时间是差不多的，不如直接读代码，完全弄清楚这个方法的含义。而对于那些行数比较多的方法，写的规格根本不能完全地、详细地体现出这个方法做了什么，归根结底还是要去读代码。
除此之外个人感觉“先写规格再写方法”的这个要求对于这三次作业来说不太合理，因为规格是我们在写了出租车的基本框架之后才要求添加的。这几次的作业我都是在写完方法之后才为方法添加规格，事实上这的确比先写规格再写方法节约时间。
总之，写规格的出发点是好的，但是在实现过程中可能因为其他的一些原因让人觉得这个东西没什么用，还浪费许多时间。希望OO课在以后发展的过程中能够解决这些困扰的问题，让学生不再有那么多怨言吧。
标签：end 结构化 jsf lock 增强 img 思路 jpg 设计者
原文地址：https://www.cnblogs.com/pyroti/p/9108003.html
