2

我试图更多地了解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. 两份合同有什么区别？2.我真的应该检查前置条件吗？3. 这个“和”是什么意思？4. 我的代码应该如何根据第二份合同进行更改？

感谢你们。

4

2 回答 2

4

1.两个合同有什么区别？

第一个以必须满足给定前提条件的方式限制方法的参数。例如，arr参数不能为空，否则会出错。然而，在第二个示例中，您可以传递您想要的任何参数，但是：当参数具有某些特定的布局/结构（不为空，获得相同数量的 4 和 5，...）时，它必须返回/更改数组这样的方式来匹配结论（我相信<== *必须转动箭头）。

2.我真的应该检查前置条件吗

是的，特别是如果你这么说。此外，它应该在 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.这个“和”是什么意思？

theAND是一个逻辑连词。它评估true是否两个参数/语句都是true.

4.我的代码应该如何根据第二份合同进行更改？

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

于 2011-03-30T21:01:28.263 回答
2

我不能声称知道，但这是我对给定条件的解释。

首先，您的代码实际上似乎并不遵循任何一个合同。它违反了$ret != arrandforall 0 <= i < arr.length-1, $prev(arr[i]) == arr[i]条件。

  1. 因为这两个条件都要求您不改变 arr （通过forall 0 <= i < arr.length-1, $prev(arr[i]) == arr[i]后置条件，并且第一个条件中的所有条件（前置和后置）都是第二个中的后置条件，所以合同是相同的，如果前置条件是，第一个要求抛出错误未满足。第二个意味着如果为 null 或其他无效，您应该简单地返回一些东西（例如nullorarr或任何其他值） 。arr

  2. 当违反先决条件时，您可能应该抛出一个非法参数异常（但也许您应该与给您合同的人谈谈）。

  3. 我AND在逻辑上将条件和 s 一起假设，就好像它们已单独描述一样（但可以与ORs 结合使用以获得更大的灵活性）

  4. 它不应该。IllegalArgumentException当不满足先决条件时，不要抛出一个，而是返回null

编辑评论：

我相信$ret != arr意味着返回值不能引用相同int[]的arr。也就是说，你必须int[]在你的函数中创建一个新的地方并返回它。

forall 0 <= i < arr.length-1, $prev(arr[i]) == arr[i]意味着arr（由于某种原因最后一个除外）的每个元素都必须与以前（在调用函数之前）相同。即你不能改变它（很多）。这与要求创建并返回一个全新的数组是一致的。

于 2011-03-30T20:53:31.250 回答