unit3_log
Pre
- 第三单元的主题是规格化设计，需要我们学会理解与使用JML语言对于java程序进行建模，从而实现对于需求的形式化。
- 形式化有许多好处：
- 逻辑明确，没有二义性，具有可靠性。
- 能够形式化的东西一定能够自动化，所以有利于自动化的测试。
- 规格上的形式化是一种契约式编程，架构层面是不需要关注实现的。
- 但也因为不需要关注实现，所以关注实现的应该是实现规格的我，所以这一章很重视算法的考察，需要特别注意代码运行时的效率。
- 另外，jml语言本身用来逻辑严密的表示需求也是比较困难的，此外，我们去分析需求也会有一定的困难。
- 我在这几周确实也忙于应付各种事情，疲于oo，所以也确实发现自己没有前两单元时那么有激情了，没有花大心思去琢磨算法与优化策略了，中测都是敷衍了事，自己也没有弄评测机，互测也没有再兴奋的去挨个嗅探了。
总体的架构
- 这单元作业总体的架构非常简单，是课程组给定的，也没有什么层次
- （其实我觉得挺无聊的，虽说为了难度考虑，但是这单元确实抛去了前两单元oo最好玩的架构设计。
整体架构如图：
主要就是Run（课程组给定）给NetWork发出指令，然后Network做出反应，更进一步的是，方法都定死了，你只需要根据JML来完成具体的实现就可以了。
- 所以我认为，在这一单元中，我们充当的角色变了，前两单元中我们是独立的软件开发者，从架构到实现到测试整套流程是我们自己打下来的。但这一单元我们好像是一个底层码农（这里没有歧视的意思），我们不需要去关心整体的架构了，我们看到的只是框架定好的函数，我们需要做的，也只是想方设法提高自己要实现的方法的效率罢了。
- 而JML，只是一种架构师与码农之间的形式化规范化的契约，至于这个契约怎么样，我们后面专有一节，谈谈对于JML的认识。
对于测试
测试的门类
- 而对于测试，虽然说我这单元并没有心力去实现评测机与实现junit的测试（这里特别感谢hpy们的评测数据与评测机），前两单元的时候有实现评测机，所以浅浅谈谈对于测试的认识吧
- 首先是从总体上来分可以分为两大类，黑箱测试与白箱测试
- 黑箱测试是不关注于具体，但是关注于整体，给输入，得到输出，看看输出是否正确。
- 白箱测试中具体实现是透明的，你可以看着具体实现针对性的进行测试。
但这只是泛泛的分类，具体还有许多种测试方法，比如单元测试、集成测试、回归测试等等
- 单元测试是对每个小的设计单元的验证测试，测试单个的方法是否可以达到要求，这通常是一种白箱测试。
- 集成测试是测试对于不同模块之间的接口，测试他们之间的协同配合工作是否正常，一般是由黑盒测试与静态白盒测试相结合。
- 系统测试层次又要更高些，是对于整个系统的测试，这个时候一般就是黑盒测试了，白盒的话一整个系统看不下来。
- 系统测试的方式有很多种，我们常说的回归测试与冒烟测试是属于系统测试的。
- 一般部署一个软件还会有一个验收测试，是用户或者甲方来做，这也是最全面的，也就是我们经常看到的软件的Alpha版与Beta版测试软件。
值得一提的是，这些测试的方法一般作为软件测试的不同阶段该干的事，我们可以看到这些测试的层次是由小到大的，也就是说，一个合格的软件应该要一整套流程都过完的。
- 然后还有一种分类的方式就是分为功能测试与压力测试，具体该干什么，顾名思义，大致可以理解为中测和强测的关系。
具体测试的门道
- 具体设计测试数据以及验证的方式也可以谈一谈：
- 静态的“肉眼”测试手段：手动构造数据的话讲究的是一个覆盖度和边界值测试
- 如何保证覆盖？
- 至少说对于每个分支都要覆盖到，对于数据不同的条件，想想它有什么不同的分支，然后将这个分支构成一棵语法树，根据这棵树来构造。
- 而边界值呢，就是对于某些东西针对性的构造数据，比如在数据范围上下死手，比如有的实现方法可能无法应对某种结构的数据。
- 自动化的测试：什么东西可以自动化？一切可以形式化的东西都可以自动化！
- 所以其实自动化数据是一个解析数据文法的过程。
- 所以我们结合JML语言，这是一个高度形式化的语言，所以我们可以通过JML对方法进行自动化的验证。
- 前置条件是对于数据构造的约束。
- 后置条件用来验证结果的正确性。
- 课程组为此也提出了OKtest的验证方式，所以我们具体来谈谈对于Oktest。
对于OKtest
- 我理解的oktest其实就是一种单元测试了，是在方法级的测试，但是课程组的oktest测试方法与我直观想到的有点不一样。
- 课程组的oktest似乎与我的方法的实现无关，我认为这是不太对的，因此也提出一点建议叭
- 比较单纯的将自己输入的两组数据做一个比较和验证，这不是只能验证自己的数据构造的正确性吗？
- 当然我还能想到的一点合理性是将输入oktest的数据变成一组数据输入，然后来将afterdata与得到的结果对拍。
- 所以我的建议是可以将oktest输入的数据载入到程序中，然后调用方法，得到结果再来验证其正确性。
对于JML的理解
- 然后来谈谈对于JML的理解叭，大家对于它的评价挺多元的。
先谈谈对于规格与实现分离的这样一种做法，我认为确实需要，而且对于大的工程来讲很必要
- 首先的一点优点就是前面提到的，形式化的东西能够自动化。
- 其次就是规格这种契约式的编程，在团队合作编程时可以统一表述需要。
- 然后就是确实在做大型软件的时候，架构师与实现者之间的分离，需要用规格来写作。这样，实现者就可以聚焦于具体方法的实现，来提高方法的性能。
但是JML这一种高度形式化的规格表述，确实就有利有弊了。
- 利的话在一开始已经提到了，没有二义性，可靠，有利于自动化。
- 但是这无疑会也会加大规格设计者（架构师）与程序员的负担（特别是程序员。
- 对于架构师来讲，本身JML的编写就比较的复杂，要验证JML这种形式化与需求的非形式化之间的一致性比较的困难。
- 但是我们也能往好的方面想一点点，毕竟复杂的方法JML会写的比较的复杂，这也一定程度上逼迫了架构师去做降低方法复杂度的设计。
但是对于程序员来讲，我觉得JML很大程度上，并不是程序员友好的。
- 虽然它没有二义性，但是程序员不是机器，很容易看错，这是一种损失了易读性换来的确定性，能不能够提高程序员的理解准确性，很难说。
- 然后就是JML也为了确定性规避了太多太多已有的抽象，包括说用JML来表示一个图论结论的抽象，JML用纯粹的数理逻辑的表述会写的又臭又长！远不如其他的形式化的表述来的直观！
- 最后就是我觉得，程序员看懂了一个JML以后，实现的时候，脑子里也不一定会装着JML去实现，所以，为什么不在一开始就把需求明确一点告诉这个可怜的程序员呢？
- 比如，有一个规格，很长很长，它就为了表达一个需要弄一个最小生成树，然后我是一个程序员，我花了很多根头发把它看懂了，“哦，原来要实现最小生成树啊”，然后我开始实现最小生成树了，在网上找板子抄，这个实现过程跟JML一点关系都没有了！
- 我认为是要寻求规格与实现的分离，但是分离和语言上的需求我都可以知道啊，我在知道这玩意是要做最小生成树之后再去看JML是不是都会清秀许多哇。
所以说到这，我也有两点建议叭。
- JML的形式化似乎有点太极端了，能不能有中和一点的形式化的方案。
- 如果它太过于极端，那也可以留下JML，但是同时给出自然语言的描述，两种规格，一种极端形式化，一种极端非形式化。这样程序员可以按照自己的需要，在用自然语言大致理解需求之后，用JML来消除掉自己的一些疑虑。
单元总结
- 这单元整体来讲还是有不少收获的，包括对于这种契约式编程的初体验，对于各种测试方式的认识。
- 但是由于自己这几周也确实心力憔悴，没有好好花心思，整体来讲还是有些遗憾的。
- 而有一些对于课程本身的建议也相当于是激发自己和大家的思考了，欢迎大家来讨论！
