学不会OO的第三单无反思（JML爪8

Posted 2020-11-30 kongyou

JML理论基础：

　　在大一的离散结构课程中，我们学习叻关于谓词逻辑的相关知识。作为一名周六还得补考离散二的菜鸡，我只能爬。我个人理解上JML语法格式是谓词逻辑和java的生动结合，让读者在理解与讨论的过程中收获极大的欢乐，并基于契约化编程的思想来解放程序员于bug之中->如果完全按照规格实现，那么WA就可以甩锅给写规格的了（

　　总体来说，JML是从上层来解决程序需求不具体明确和bug的易产生的一种（应该是）重要的工具（不过好像搜到的都是贵系人的资料）

JML知识点总结：

• pure：
  纯粹查询，无任何副作用。
• 数组：
  仅仅是规格层次的描述，不一定要数组实现
• no_null:
  该对象不能为空。
• esult：
  该方法的返回值。
• require：
  前置条件，即调用该方法时参数以及成员变量需要满足的条件。
• assaignable：
  副作用范围，列出所有可能会被修改的成员变量。
• othing：
  空
• ensure：
  后置条件，即调用该方法之后参数和成员变量需要满足的条件。
• old()：
  表示调用该方法前的该对象或表达式的值。
• ype()：
  表示该类(type)的类型(class)。
• ypeof()：
  表示该表达式的类型。
• forall()：
  相当于离散数学中的"任意"符号。
• exits()：
  相当于离散数学中的"存在"符号。
• <=, =>, <=>：
  离散数学中的蕴含，等价等
• public_normal_behavior：
  正常功能规格。
• public_exceptional_behavior:
  异常功能规格。
• also：
  分开正常和异常两种规格。
• signals () ___ :
  满足条件抛出异常

JMLUnitNG/JMLUnit：

　　由于本人最近都在用mac，所以没有找到成型的完整工具链。经过两周多的努力，依旧没有整好，于是??放弃叻（希望有朝一日有时间仔细整理一下）

 

JUnit单元测试！！！！：

　　这单元我对单元测试有较大感悟。回头单开一个博客再施工（https://www.cnblogs.com/kongyou/p/12940427.html）

　　总体来说，单元测试能够较有效的解决如wa等问题。在解决tle等问题上有局限性，但不是不能。配合本人魔改runner，基本能够做到准确定位。