java - java中的合约

Question

我正在尝试了解更多有关 java 中契约的含义。

这是 Java 中两个合约的示例:

*/
* @pre  arr != null
* @pre  occurrences(4,arr) == occurrences(5, arr)
* @pre  arr[arr.length – 1] != 4
* @pre  forall 0 <= i < arr.length-2, arr[i] == 4 ==> arr[i+1] != 4
* @post forall 0 <= i < arr.length-1, $prev(arr[i]) == arr[i]
* @post $ret != arr
* @post permutation(arr, $ret)
* @post forall 0 <= i < arr.length-1, arr[i] == 4 ==> $ret[i] == 4
* @post forall 0 <= i < $ret.length-2, $ret[i] == 4 ==> $ret[i+1] == 5
/

第二个:

*/
* @post (arr != null AND
*        occurrences(4,arr) == occurrences(5, arr) AND
*       arr[arr.length – 1] != 4 AND
*       forall 0 <= i < arr.length-2, arr[i] == 4 ==> arr[i+1] != 4)
<==        *
*       (forall 0 <= i < arr.length-1, $prev(arr[i]) == arr[i] AND
*        $ret != arr AND
*        permutation(arr, $ret) AND
*  $ret.length == arr.length AND
*        forall 0 <= i < arr.length-1, arr[i] == 4 ==> $ret[i] == 4 AND
*        forall 0 <= i < $ret.length-2, $ret[i]==4 ==> $ret[i+1] == 5)
/

任务是在这些前提条件下更改给定的数组，以便在出现任何 4 后都会出现 5。 例如:

fix45({5,4,9,4,9,5}) -> {9,4,5,4,5,9}

fix45({1,4,1,5}) -> {1,4,5,1}

这是我写的(有效):

public static  int pos (int[] arr, int k){

    while (arr[k]!=5){
        k=k+1;
        }
    return k;
}

public static  int[] fix45(int[] arr){
    int k=0;
    for(int i = 0; i<=arr.length-1; i++){
        if (arr[i] == 4){
            int place= pos(arr,k);
            arr[place]=arr[i+1];
            arr[i+1]=5;
            k=k+3;


        }

    }
    return arr;
}

我的任务: 1. 两个契约(Contract)有什么区别？ 2.我真的应该检查先决条件吗？ 3. 这个“和”是什么意思？ 4.我的代码应该如何根据第二份契约(Contract)进行更改？

谢谢大家。

Answer 1

1. What is the difference between the two contracts?

第一个方法将参数限制为必须满足给定的先决条件。例如arr参数不能为空，否则会出错。然而，在第二个示例中，您可以传递所需的任何参数，但是:当参数具有某些特定布局/结构(不为空，具有相同数量的 4 和 5，...)时，它必须返回/更改数组这样才能符合结论(我相信<== *处的箭头一定要转向)。

2. should I actually check the pre-conditions

是的，特别是如果你这么说的话。此外，它应该在 javadoc 注释中提及，并且应该说明如果没有提及会发生什么。 Javadoc 获得 @throws的关键字。类似的东西

/**
 * (...)
 * @throws NullPointerException If the argument is <code>null</code>.
 * @throws IllegalArgumentException If the number of 4's and 5's is not the same.
 */

3. what this "And" means?

AND是 logical conjunction 。其计算结果为true如果两个参数/语句都是 true .

4. how my code should change according the second contract?

您不应抛出异常或以任何方式更改数组，除非它与假设匹配( ==> 之前的部分)。在这种情况下，必须根据结论更改数组(和/或返回值)。