当代码遇到数理逻辑——面向对象设计与构造第三章总结

在面向对象课程中的第三章，我尝试了基于JML语言的规格化设计，按照AppRunner中的接口文件实现了Path类和PathContainer, Graph, RailWaySystem迭代类。JML语言是一种规格化语言，完全建立于数理逻辑上，既能够为开发者实现类与方法时提供准确的功能参考，也能够在特定工具支持下充当assert的功能和辅助自动生成测试样例。

本篇博客将从以下几方面对第三章进行总结：

  1. JML的基本语法与工具链
  2. 基于JmlUnitNg的自动测试方法尝试
  3. 三次作业架构
  4. 程序Bug分析
  5. 有关规格撰写的心得与体会

1. JML基本语法与工具链

1.1 JML基本语法

常用原子表达式

\result
\old(expr)
\assignable
\nonnullelements
\not_assigned(x,y,...) \not_modified(x,y,...)

常用量化表达式

\forall         \\ 给定元素；前提范围；后置约束（张三  在学校里面  一定不玩游戏）
\exist          \\ 给定元素；前提范围；后置约束
\sum            \\ 给定元素；前提背景；累加对象
\product        \\ 给定元素；前提背景；累乘对象
\max \min \num_of

常用集合表达式

new JMLObjectSet {Integer i | s.contains(i) && 0 < i.intValue() }

操作符

A <: B                  \\ A是B的子类时为真
A <==> B ; A <=!=> B    \\ 与==和！=相同效果，但优先级更低
A ==> B                 \\ 推理
\nothing; \everything   \\ 空集；当下作用域能够访问的所有变量。
                        \\常用assignable \nothing来表示pure类方法

类型规格

  1. invariant 不变式（约束当前状态）：所有可见状态下必须满足，用法invariant P（P是谓词，最后整个P应该可以被替换为一个逻辑真值）。
  2. constraint 变化约束（约束前序状态与当前状态之间的关系）：用法同invariant。

1.2 JML工具链

在尝试编写JML规格和根据JML规格填充代码时，主要使用了VS-Code、OpenJML和JMLUnitNg，在本部分我将主要介绍前面两者，最后者放在第2章节具体介绍。

VS-Code

VS-Code主要提供了Java+Jml的语法插件支持，从而对注释中的JML语言进行了高亮，便于在撰写规格时的语法检查和实现规格时的阅读清晰。

OpenJML

根据OpenJML相关文档，OpenJML提供三种类型的检查：

  1. 形式化检查（Type Checking）：

    1. 目前我也不清楚将Type翻译为“形式化”是否合适，根据网络资料查阅，Type Checking是编译器基于Abstract Syntax Tree —— 抽象语法树进行代码检查的一种形式，检查例如3 + True运算不匹配等各类问题，属于静态检查——Static Checking的一部分。
    2. 根据官网样例和实际尝试，我认为形式化检查的重点应该是规格中各个变量类型的正确性和匹配性，例如void类方法结果有\result、不符合类型的赋值和比较等……
    3. 执行命令：java -jar openjml.jar Student.java
    1. The resulting AST may then be subjected to various checks to ensure that certain obvious errors are avoided (static analysis).One common form of static analysis is type-checking.
    2. After this, the AST will be fed to an evaluator or interpreter to execute the program—or else to a compiler to translate it into executable low-level code.
    3. https://www.inf.ed.ac.uk/teaching/courses/inf2a/slides2017/inf2a_L14_slides.pdf
  2. 静态检查（Static Checking）：
    1. 静态检查是根据撰写的JML规格，检测实现的方法和类中是否有与规格定义相违背的地方，在这里似乎有多种Solver可以配置使用，以实现不同的检查。
    2. 执行命令：java -jar openjml.jar -esc -exec Solvers-windows/z3-4.7.1.exe B.java，这里遇到了奇怪的问题，如果不使用-exec指定相应的证明器，则不能运行成功，并且三个证明器也仅有z3-4.7.1的版本能够运行成功，目前猜测可能是遇到了windows版本的运行环境的问题。 
      public class B {

    static /*@ spec_public*/ int j,k;

    //@ requires i >= 0;
    //@ modifies j;
    //@ ensures j == i;
    public static void setj(int i) {
      k = i;
      return;
    }

    //@ ensures j == 1;
    public static void main(String[] args) {
      setj(3);
      return;
    }

  }

B.java:16: 警告: The prover cannot establish an assertion (Postcondition: B.java:13: 注: ) in method main
      return;
      ^
B.java:13: 警告: Associated declaration: B.java:16: 注:
    //@ ensures j == 1;
        ^
B.java:10: 警告: The prover cannot establish an assertion (Postcondition: B.java:7: 注: ) in method setj
      return;
      ^
B.java:7: 警告: Associated declaration: B.java:10: 注:
    //@ ensures j == i;
        ^
B.java:9: 警告: The prover cannot establish an assertion (Assignable: B.java:6: 注: ) in method setj:  k
      k = i;
        ^
B.java:6: 警告: Associated declaration: B.java:9: 注:
    //@ modifies j;
        ^
  3. 运行时检查（Runtime Assertion Checking）：
    1. 运行时检查在我看来就是基于JML规格在输入和输出时生成一系列的assert语句检查类和方法在运行过程中是否符合规定。
    2. 执行命令java -jar openjml.jar -rac Student.java + java -classpath ",;jmlruntime.jar" Student我使用了课程组JML教程中的Student类中的addCredits方法进行尝试，方法要求传入的变量为非负整数，我调用此方法并输入负数时，程序就出现了错误信息，从而帮助我定位错误：
        /*@ requires c >= 0;
    @ ensures credits == \old(credits) + c;
    @ assignable credits, master;
    @ ensures (credits > 180) ==> master;
    @*/
    public void addCredits(int c) {
        updateCredits(c);
        if (credits >= 180) {
            changeToMaster();
        }
    }

2. 基于JMLUnitNg的自动测试

此部分的内容十分感谢伦泽标同学对JMLUnitNG自动测试工具的探索与分享，在这里我使用课程组JML教程中的Student类作为被测试对象，记录相关的测试指令，浅析自动测试的相关特点。

自动测试的方法

我在运行自动测试时脚本如下：

java -jar jmlunitng.jar student/Student.java              # 生成自动测试源码
javac -cp jmlunitng.jar student/*.java                    # 编译自动测试源码
java -jar ../openjml.jar -rac student/Student.java        # 编译源文件为rac，用于运行时检测
echo "begin to check"
java -cp jmlunitng.jar student.Student_JML_Test           # 启动自动测试
pause
[TestNG] Running:
  Command line suite

Passed: racEnabled()
Failed: constructor Student(null)
Passed: constructor Student()
Skipped: <<[email protected]>>.addCredits(-2147483648)
Passed: <<[email protected]>>.addCredits(0)
Passed: <<[email protected]>>.addCredits(2147483647)
Passed: <<[email protected]>>.getName()
Failed: <<[email protected]>>.setName(null)
Passed: <<[email protected]>>.setName()

===============================================
Command line suite
Total tests run: 9, Failures: 2, Skips: 1
===============================================

自动测试的特点

  1. 数字类的测试：对应了上下边界和临界态。不过在这里我并不是太清楚skips类型是什么原因，可能是因为在部分编译器中存在（-2147483648 > 0）的现象。
  2. 参数为类的方法与构造函数：常规情况、null和空的情况。
  3. 被测试方法类型：没有对private私有方法（如updateCredits）进行测试。

3. 三次作业架构分析

第一次作业

第一次作业的类划分比较简单，除实现的两个接口类以外，额外引入了DoubleDirMap类基于HashMap双向映射Path和PathId，而也正是因为将功能划分地很细致和明确，作业一的代码复用率几乎以100%复用。由于基本上都是实现的接口方法，自定义方法很少，因此不再进行量化分析。

第二次作业和第三次作业

虽然有接口类指导顶层类的设计，但是内部功能的实现与性能优化则需要自行设计，本章作业中，我高兴地发现自己在Graph中所实现了架构在RailWayStation中竟然有许多的复用情况，这一点也确实说明在经过OO课程的洗礼后，对程序的功能架构有了一定的提升。

由于作业二与作业三一脉相承，在此我将主要展示第三次作业中的架构。

─subway
    │  MyRailwaySystem.java
    │
    ├─algorithm
    │  │  InfectGraph.java
    │  │
    │  └─shortest
    │          LeastTransfer.java
    │          LeastUnpleasant.java
    │          LowestTicketPrice.java
    │          ShortestPath.java
    │          ShortestPathModel.java
    │
    ├─component
    │  │  DoubleDirPathMap.java
    │  │  MyPath.java
    │  │
    │  ├─link
    │  │      Link.java
    │  │      LinkContainer.java
    │  │
    │  └─node
    │          NodeCountMap.java
    │
    └─tool
            AlgorithmFactory.java
            Constant.java
            ConvertMap.java
            Matrix.java
            VersionMark.java

在图论的问题里，图的结构和运行在图上的算法基本可以完全所有类型的图问题，因此，我的类采用结构+算法的构造，结构随着每一次路径的增删实现实时的更新，算法则内部根据缓存版本和图当前的结构类，实现相应功能。

  1. 结构类：与结构有关的类都被定义在component包内。MyPath是路径类；DoubleDirPathMap用于维护路径类与路径ID之间的关系；Link和Node是对加入图的Path具体拆分和解析后形成的相关类，分别用于维护图结构两个基本的要素——点和边的详细信息（例如点全集、某点所在的路径编号、某点所连的边、某点所连边的路径编号……），正是这些详细信息使得图上的算法成为可能。
  2. 算法类：与算法相关的类都被定义在algorithm包内。
    1. InfectGraph用于统计连通块的数量，此功能和其他功能实现算法不同，采用的是BFS+染色的方式。
    2. shortest包中包含了4种跑在不同边权图上的最短路算法，我采用的是拆点建图+最短路SPFA的方式求解此问题：将真实点拆成虚拟点，使每个虚拟点只对应一个真实点且只对应真实点所在的一条路径，探讨对应相同真实点的虚拟点间的边权，从而解决换乘成本问题。由于只是新图上的边权有4种不同的定义，因此需要重写的就只有边权的赋值方法，为此我定义了ShortestPathModel抽象类实现除边权赋值外的所有方法，并定义getEdgeValue抽象方法以要求所有的继承类必须要实现该方法。

    A = 虚拟点所对应的物理点相同

    B = 虚拟点所对应的路径相同

    A=True B=True A=True B=False A=False B=True A=False B=True
    最短路 0 0 1 -
    最小换乘 0 1 0 -
    最低票价 0 2 1 -
    0 32 $H(e_1,e_2)$ -
  3. 工具类：工具类的定义，旨在减少类和方法中声明过多成员变量的问题。
    1. Algorithm Factory：工厂模式生产算法。
    2. Constant：常量接口
    3. CovertMap：转换映射类，用于构建每种算法新图时拆点后维护真实点和虚拟点所使用。
    4. Matrix：基于HashMap的二维矩阵，形如matrix[][]，这在保存邻接图、保存最短路、保存路径和点的详细信息等多方面都有运用，因此独立出来。
    5. VersionMark：版本控制类，用于维护当前图结构版本和算法缓存版本之间的关系。

复杂度分析

根据量化指标，整个工程的复杂度还是不错的，部分类出现OCavg指标过高的主要原因是if-elseif-else条件判断分支过多，集中在抛出异常和工程模式中。

而分析了类依赖性的量化指标和依赖矩阵，说明程序对类功能划分设计得是合理的，都没有体现出过高的依赖性.

4. 程序Bug分析

在本章的三次作业中，受益架构划分得比较清晰和针对每个方法的单元测试，在强测和互测阶段都没有出现Bug，而对于其他同学的Bug，我在阅读代码中发现的Bug如下：

  1. 将路径的Hash值等价于Equal：有同学对HashMap泛型的使用不清楚，没有通过实现Path的HashCode和Equal来使Path类成为HashMap的键值，而用Path的HashCode作为HashMap的键值。这样方式在强测随机下很难翻车，但针对性的构造数据即可攻破。

5. 对规格撰写的心得与体会

经过对一些简单的JML规格填充，我对其撰写有以下三点感悟：

  1. 三个抓住

    1. 抓住情景的分类：根据输入和数据的条件产生多个behavior。
    2. 抓住方法的头和尾：require和ensure的使用
    3. 抓住成员变量的变与不变：assignable
  2. 内部逻辑的表达
    1. 对于复杂的逻辑，在JML中应该引入中间变量进行阐述，必要时直接提取成为方法。
    2. \forall, \exist的两个作用
      1. 逻辑判断作用：就像梳理逻辑中的判断真假命题一样，推出True或False的结论。
      2. 修饰作用：常用\exist并（外加\exist+\forall作为逻辑判断）定义一个带有某种性质的中间变量。
  3. \old就是拍快照
    1. \old的使用其实很像Verilog语言中的非阻塞赋值，使用old一定要明确自己要的具体是什么，最终一定细化到数字或者逻辑真值上，因为如果是给类拍快照都有被掉包的风险。

在我看来，JML语言不同于Javadoc等自然语言注释，其本身就是由纯数理逻辑所形成的，这样的规格优点是无二义性、在一定工具的支持下能够配合自动化检查。但是缺陷则是随着方法的需求变得复杂和感性，需要花费大篇幅的JML规格去阐释从人的角度很容易理解的内容，就像第三次作业中换乘条件的加入引入了大量无需程序员实现的pure方法，而且规格也容易出现很多的错误，并且由于这些方法并不需要实现，JML规格的自动检查功能实际已经丧失了。

因此，JML的应用情景我认为还是需要进一步商榷和深究的，目前认为用在系统体系结构、数论、图论等逻辑数理性强的领域更为适合，并且甚至还可能借助于已经成熟的机器证明体系以实现JML自动化生成；而对于一些实际生活应用的例子，则可以通过自然语言注释+黑/白名单特例的形式进行阐述。

原文地址：https://www.cnblogs.com/sinoyou/p/10908763.html

时间： 2024-10-14 23:13:14

当代码遇到数理逻辑——面向对象设计与构造第三章总结的相关文章

软件构造 第三章第三节 抽象数据型(ADT)

软件构造 第三章第三节 抽象数据型(ADT) Creators(构造器): 创建某个类型的新对象,?个创建者可能会接受?个对象作为参数,但是这个对象的类型不能是它创建对象对应的类型.可能实现为构造函数或静态函数.(通常称为工厂方法) t* ->  T 例子:Integer.valueOf( ) Producers(生产器): 通过接受同类型的对象创建新的对象. T+ , t* -> T 例子:String.concat( ) Observers(观察器): 获取抽象类型的对象然后返回一个不同类

软件构造 第三章第二节 软件规约

第三章第二节 软件spec 客户端无需阅读调用函数的代码,只需理解spec即可. 精确的规约,有助于区分责任,给"供需双方"确定了责任,在调用的时候双方都要遵守. @param @return @throws 例子: Behavioral equivalence (行为等价性) 根据规约判断是否行为等价 与实现无关! 如果两个函数符合这个规约,故它们等价. Specification Structure 前置条件(precondition):对客户端的约束,在使用方法时必须满足的条件.

面向对象设计与构造第四次课程总结

测试与正确性论证 用测试样例进行测试,可以直观地发现对于该测试样例,程序运行中在什么位置出现了问题.问题本身能直观地反映bug的存在.此外,一个bug的修复往往使得多个之前无法通过的测试样例得以正常通过.但是用测试样例进行测试想要进行全面的覆盖,工作量是十分庞大的.首先,要明确一个测试样例的在各个阶段的运行处理流程:然后,再根据各个阶段中的各个分支流程及其组合,构造测试样例进行测试:此外,还要结合各处数据的边界限制条件进一步加以组合并测试.随着程序规模的增长,系统复杂性的上升,组合的情况总数越来

2018-06-20 中文代码示例视频演示Python入门教程第三章 简介Python

知乎原链 Python 3.6.5官方入门教程中示例代码汉化后演示 对应在线文档: 3. An Informal Introduction to Python 不知如何合集, 请指教. 中文代码示例Python入门教程 3.1.1_哔哩哔哩 (゜-゜)つロ 干杯~-bilibili 中文代码示例Python入门教程 3.1.2 第一部分_哔哩哔哩 (゜-゜)つロ 干杯~-bilibili 中文代码示例Python入门教程 3.1.2 第二部分_哔哩哔哩 (゜-゜)つロ 干杯~-bilibili

软件构造 第三章第五节 ADT和OOP中的等价性

第三章第五节 ADT和OOP中的等价性 1.==与equals ==是引用等价性 :而equals()是对象等价性. == 比较的是索引.更准确的说,它测试的是指向相等(referential equality).如果两个索引指向同一块存储区域,那它们就是==的.对于我们之前提到过的快照图来说,==就意味着它们的箭头指向同一个对象. equals()操作比较的是对象的内容,换句话说,它测试的是对象值相等(object equality).在每一个ADT中,equals操作必须合理定义 2.等价性

大型分布式架构设计与实现-第三章互联网安全架构

本章首先介绍了一些常见的Web攻击手段. 1.XSS攻击(Cross Sites Scripting),指跨站脚本攻击.攻击者在网页中嵌入恶意脚本程序,当用户打开该网页,恶意程序在浏览器执行,会盗取用户名密码,cookie,下载执行病毒木马程序,甚至是获取客户端admin权限等. 2.CSRF攻击(Cross Site Request Forgery),指跨站请求伪造.攻击者伪装成站点内受信任的用户进行恶意的发邮件,发短信,进行交易等,甚至盗取你的账号. 3.SQL注入攻击.通过把SQL命令伪装

软件构造第三章 第五部分

ADT和OOP中的等价性 equal和== hashcode()和equals()方法总是一起被重写 “==”:引用等价性,指向相同的内存地址, equals():对象等价性,在自己定义的ADT时,需要重写Object的equals()/ "=="是对基本数据类型,而对于对象类型,使用equals(). equal的自反.传递.对称 等价的三种定义 1)若AF映射到同样的结果,则等价 2)若两个对象之间满足自反,传递.对称的关系,那么为等价关系 3)站在外部观察者角度发现二者没有区别(

2018-06-20 中文代码示例视频演示Python入门教程第四章 控制流

知乎原链 续前作: 中文代码示例视频演示Python入门教程第三章 简介Python 对应在线文档: 4. More Control Flow Tools 录制中出了不少岔子. 另外, 输入法确实是一个短板. 中文代码示例Python入门教程 4.1 if条件语句 & 4.2 for语句_哔哩哔哩 (゜-゜)つロ 干杯~-bilibili? 中文代码示例Python入门教程 4.3 range函数_哔哩哔哩 (゜-゜)つロ 干杯~-bilibili? 中文代码示例Python入门教程 4.4 b

面向对象设计的11个原则

单一职责原则(The Single Responsibility Principle,简称SRP) 开放-封闭原则(The Open-Close Principle,简称OCP) Liskov替换原则(The Liskov Substitution,简称LSP) 依赖倒置原则(The Dependency Inversion Principle,简称DIP) 接口隔离原则(The Interface Segregation Principle,简称ISP) 重用发布等价原则(The Reuse-