如果写规格的人和写代码的人不是同一个人，这个结论应该就很显然了。

我们常常做测试时，就对方法单独的测试，只要输入满足规格的requires，检查输出是否满足effects就好了。如果测试通过，且modifies正确，那么就较大概率没bug（因为并未进行完备的测试）。这样单独的方法对了，才是对的。

设计规格和撰写规格的思路和体会

先说体会吧！首先感谢课程组让我们训练设计和撰写规格。

老师课上总是强调设计规格的重要性，虽然大家写得很累，但是我觉得老师说得很对。设计规格确实是最重要的。尤其是在团队协作中。

所有的程序开发手册都包含了各种规则。我们可能对这些规则很不适应，但是在多个开发人员共同协作的情况下，这些规则是必须的。这不仅仅是为了开发效率来考虑，也是为了后期维护考虑。所以我觉得老师说的很对。

关于设计规格和撰写规格。我的思路如下：

首先，我们要根据设计需求，进行架构，做数据抽象，总结出几个类，弄清楚各个类的定义，弄清楚各个类之间如何交互，弄清楚各个类如何相互合作最终把这些设计需求来实现。

其次，根据数据抽象，弄清楚各个类需要哪些属性。

再然后，根据设计需求，弄清楚类需要哪些方法，而这些方法需要被哪个或哪些类调用。又或者它仅仅只是一个内部方法。弄清楚这个方法要实现什么样的功能。这里我想起来老师上课常常讲的话，就是写JSF时千万别去想算法。所以，这一步，先不考虑算法怎么实现，只考虑这个方法的功能。另外这一步要保证代码的逻辑是正确的。

再之后，开始写设计规格。根据上一布自己所想的，写好设计规格。注意require effect的正确性。

再之后，开始写代码，就实现那些方法。这里要注意算法的正确性，注意，如果有modify，可能还需要修改一下设计规格。

最后，测试程序，检查代码功能是否正确。如果功能错误，可能是在设计规格时逻辑错误，也可能是代码在具体实现时算法错误或者编码错误。要从这两个方向来找bug，最终得到正确的程序。

最后谢谢老师们谢谢助教们谢谢同学们！