我试图找出有关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.根据第二份合同，我的代码应如何更改？
感谢大伙们。
最佳答案
1.这两个合同有什么区别？
第一个以必须满足给定先决条件的方式将参数限制为方法。例如，arr参数不能为null，否则为错误。但是，在第二个示例中，您可以传递所需的任何参数，但是：当参数具有某些特定的布局/结构（不为null，具有相同数量的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.这个“与”是什么意思？AND是logical conjunction。如果两个参数/语句均为true，则结果为true。4.根据第二份合同，我的代码应如何更改？除非它与假设（
==>之前的部分）匹配，否则您不应该抛出异常和异常或以任何方式更改数组。在这种情况下，必须根据结论更改数组（和/或返回值）。