---
title: JMLGPT User Study
emoji: 🔥
colorFrom: indigo
colorTo: blue
sdk: gradio
sdk_version: 4.3.0
app_file: app.py
pinned: false
license: unknown
---

# 程序规约有效性评估——用户调研

感谢您在百忙之中抽出时间帮助我们完成课题！在本次调研中，您需要对约30个带形式语言规约的Java程序进行打分，以评估这些规约的语义是否足够有效且用户友好。调研总共需耗时约20分钟。



## 背景知识：JML

JML（Java Modeling Language）是一种对Java程序的行为进行描述的规约语言，其形式是写在Java程序中、以`@`符号开头的注释。请看下面的例子：

```java
public class IsAscending {
    //@ requires arr != null;
    //@ ensures \result == true <==> (\forall int i; 0 <= i && i < arr.length-1; arr[i] < arr[i+1]);
    public boolean isAscending (int[] arr) {
        int n = arr.length;
        if (n < 2) {
            return true;
        }
        //@ maintaining 0 <= i && i <= n-1;
        //@ maintaining (\forall int j; 0 <= j && j < i; arr[j] < arr[j+1]);
        //@ decreases n - i;
        for (int i = 0; i < n-1; i++) {
            //@ assume 0 <= i && i < arr.length;
            if(arr[i] >= arr[i+1])
                return false;
        }
        return true;
    }
}

```

拥有超强代码能力的您不难看出，该程序可以判断整型数组`arr`是否是单调递增的。该程序中的注释即为描述程序行为的JML，每个JML语句占据一行单行注释，以分号作为结尾。在该样例中：

+ `requires`语句描述某方法的参数应当满足的条件；
+ `ensures`语句描述某方法在满足`requires`语句所描述的条件时，其返回值`\result`与各个参数应当满足的关系；
+ `maintaining`语句描述`while`、`for`等语句应当满足的循环不变式。由该语句所描述的规约应当在进入循环时、每次循环体执行前以及（因循环条件不满足）退出循环时均成立；
+ `decreases`语句是一种细分的循环不变式，其含义是表达式的取值在每次循环后都会变小；
+ `assume`语句用于辅助JML验证器对JML的正确性进行验证，其含义是显式告诉验证器，相应的布尔表达式在该程序点必然为真。

大多数JML语句中都会包含一个表达式。表达式的形式与Java中常见的表达式基本一致，但为了充分表达程序可能满足的性质，JML对表达式中能够出现的谓词与操作符都进行了一定扩展，包括表示蕴含的逻辑操作符`==>`、`<==`以及`<==>`、与$\forall$与$\exists$相对应的谓词`\forall`与`\exists`等。例如，表达式`\result == true <==> (\forall int i; 0 <= i && i < arr.length-1; arr[i] < arr[i+1])`的含义为：方法返回值为真，当且仅当对于从`0`到`arr.length-2`的每个整数`i`，都有`arr[i] < arr[i+1]`。

除此之外，JML还提供了表示连加与连乘的谓词`\sum`与`\product`、表示取最大或最小值的谓词`\max`与`\min`、表示求符合条件的元素个数的谓词`\num_of`等。由于实验所用的验证器没有实现对上述谓词的支持，待评价的JML注释中不会出现这些谓词。



## 调研内容

经过上文的简单介绍，相信您已经对JML有了一个基础的了解。在本次调研中，您需要阅读一系列含JML规约的Java源代码，并评估这些规约的语义是否能够涵盖足够多的有效信息。

#### 注意事项

+ 调研将采用五分量表法进行，您需要对每个样例给出1~5分之间的评分。参考评分标准见下文。
+ 您需要对约30个样例进行打分，每个样例的有效长度不超过50行。
+ 您并不需要读懂整个代码，只需要评估其中的规约涵盖的有效信息如何，是否能帮助您增进对代码的理解。
+ 每个样例中都会包含多条JML规约，您需要对所有规约的语义做综合评价，可以考虑取其中所有规约中得分最高的一个作为最终评价。
+ 每个样例中的JML规约均已通过验证，您可以认为它们~~基本~~都是正确无误的。~~如果有错就是verifier的锅~~
+ 部分样例中可能会出现`main()`方法，请无视它以及描述它的规约，无需对描述它的规约做出评价。
+ 部分样例中可能会出现类似`__Loop_Invariant_Dummy()`的无内容方法，这是由于部分生成JML规约的工具无法自发生成`maintaining`等循环不变式，因而需要采取这种方式~~曲线救国~~。您可以将描述这些方法的规约视为相应调用点的循环不变式。

#### 参考评分标准

+ 1分：根本没有表达规约的注释。

+ 2分：有规约，但其意义过于trivial，对于任何类似pattern的代码都有效，例如：

  ```java
  //@ ensures \result == true || \result == false;
  public boolean isAscending (int[] arr) { /*......*/ }
  ```

+ 3分：规约有一定意义，但对于理解程序实际所做的事没有什么帮助，例如：

  ```java
  //@ ensures (\exists int i; 0 <= i && i < arr.length; \result == arr[i]);
  public int Biggest (int[] arr) { /*......*/ } //求数组中元素的最大值
  ```

+ 4分：规约能够充分描述程序中某些部分应满足的性质，但尚不足以完全描述整个程序所做的事，例如：

  ```java
  public class IsAscending {
      public boolean isAscending (int[] arr) {  //未能给出描述该方法整体行为的规约
          int n = arr.length;
          if (n < 2) {
              return true;
          }
          //@ maintaining 0 <= i && i <= n-1;
          //@ maintaining (\forall int j; 0 <= j && j < i; arr[j] < arr[j+1]);
          //@ decreases n - i;
          for (int i = 0; i < n-1; i++) {
              if(arr[i] >= arr[i+1])
                  return false;
          }
          return true;
      }
  }
  ```

+ 5分：规约能够充分描述程序整体与部分的行为，例如在上一节中所提供的样例。



## 再次感谢您对本课题做出的贡献！