调研规格化设计

　　1950年代，第一次分离，主程序和子程序的分离程序结构模型是树状模型，子程序可先于主程序编写。通过使用库函数来简化编程，实现最初的代码重用。产生基本的软件开发过程：分析—设计—编码—测试，使大型软件系统的开发成为可能

1975—1980年代，第二次分离，规格说明（Spec）和体（body）的分离说明是类型定义和操作描述，体是操作的具体实现。（具体的例子就是C++,Java等面向对象语言的类说明与类实现的分离。）解决方案设计只关注说明，实现时引用或者设计体。体的更改、置换不影响规格说明，保证了可移植性。支持多机系统，但要同样环境。此时产生了划时代的面向对象技术。

　　从1991年开始，面向对象的形式规格说明语言开始发展，例如，Object-Z, VDM++, CafeOBJ等语言。

1995—2000年代，第三次分离，对象使用和对象实现的分离基于构件开发：标准化的软件构件如同硬件IC，可插拔，使用者只用外特性，不计内部实现。Web Services：软件就是服务。分布式，跨平台，松耦合。

bug统计及分析

	功能bug	规格bug
第9次作业	0	0
第10次作业	0	1
第11次作业	1	0

分析：

　　第十次作业的规格bug是由于复制了之前gui里对地图文件的处理方法，但未对已有的jsf格式进行修改导致的。

　　第十一次作业的功能bug是由于之前未仔细阅读issue，未对滴滴打鬼的情况进行处理。

规格举例

1.未考虑异常情况

/**
* @ Requires: None;
*
* @ Modifies: System.out, id, credit, pos, pre, state, Main.gui, ma, chn, road,
* wait_start, now_t;
*
* @ Effects: normal behavior 进行车的运动；
*
* @ THREAD_REQUIRES: \locked(this);
*
* @ THREAD_EFFECTS: \locked();
*/

改进后：

/**
* @ Requires: None;
* 
* @ Modifies: System.out, id, credit, pos, pre, state, Main.gui, ma, chn, road,
* wait_start, now_t;
* 
* @ Effects: normal behavior 进行车的运动 sleep出现异常 ==> exceptional_behavior (e);
* 
* @ THREAD_REQUIRES: \locked(this);
* 
* @ THREAD_EFFECTS: \locked();
*/

2.effect直接为代码

/**
* @ REQUIRES: None;
*
* @ MODIFIES: None;
*
* @ Effects: pos != null;
*/

改进后：

/**
* @ REQUIRES: None;
* 
* @ MODIFIES: None;
* 
* @ Effects: pos != null ==> \result == true;otherwise==>\result==false;

*/

3.写法不太好

/**

* @ Effects: \result == (graph+1>=0 && graph+1<=MAXNUM) ==> true;
(graph+1 <0 ||graph+1>MAXNUM) ==> false;
*/

改进后：

/**

* @ Effects:  (graph+1>=0 && graph+1<=MAXNUM)==>\result == true;

*   　　　　  (graph+1 <0 ||graph+1>MAXNUM)==>\result == false;
*/

基本思路和体会

　　jsf还是应该在写方法之前先写好，作为方法的思路引导，现在这样方法写好了再去补全jsf实在会出现很多意料之外的问题。然后jsf的布尔表达式伟业应用的不熟练，还需实践。