Spaces:
Sleeping
A newer version of the Gradio SDK is available:
4.36.1
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程序中、以@符号开头的注释。请看下面的例子：
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的代码都有效，例如：
//@ ensures \result == true || \result == false; public boolean isAscending (int[] arr) { /*......*/ }3分：规约有一定意义，但对于理解程序实际所做的事没有什么帮助，例如：
//@ ensures (\exists int i; 0 <= i && i < arr.length; \result == arr[i]); public int Biggest (int[] arr) { /*......*/ } //求数组中元素的最大值4分：规约能够充分描述程序中某些部分应满足的性质，但尚不足以完全描述整个程序所做的事，例如：
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分：规约能够充分描述程序整体与部分的行为，例如在上一节中所提供的样例。