java中的合同
我试图在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)
/
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;
}
没有找到相关结果
已邀请:
2 个回复
箩冀娥
两份合同有什么区别？ 第一个将参数限制为方法，它们必须满足给定的前提条件。例如，参数不能为空，否则为错误。在第二个例子中，你可以传递你想要的任何参数，但是：当参数是某个特定的布局/结构（不是null，得到相同数量的4和5，...）时，它必须返回/更改数组这样一种方式来匹配结论（我相信必须转动的箭头）。我应该实际检查前提条件 是的，特别是如果你这样说的话。另外，它应该在javadoc注释中提及它应该说明什么时候发生的事情。 Javadoc获得了关键字。就像是这个“和”是什么意思？是一个逻辑联合。如果两个参数/陈述都是，则评估为。我的代码应如何根据第二份合同进行更改？ 除非符合假设（之前的部分），否则不应以任何方式抛出和异常或更改数组。在这种情况下，必须根据结论更改数组（和/或返回值）。禽兢玫坞劲
和条件。 因为这两个条件都要求你不要改变arr（通过后置条件，并且第一个中的所有条件（前置和后置）都是第二个中的后置条件，所以合同是相同的。如果先决条件，则第一个要求抛出错误如果为空或无效，则第二种意思是你应该简单地返回一些东西（例如或或任何其他值）。 当违反前提条件时，您可能应该抛出非法的参数异常（但也许您应该与给予您合同的人谈谈）。 我假设逻辑上和条件一起，就好像它们已被单独描述（但可以与s一起使用以获得更大的灵活性） 它不应该。当不满足前提条件时，不要扔掉，而是返回编辑评论： 我相信意味着返回值不能与相同。也就是说，你必须在你的函数中的某个地方创建一个新的并返回它。表示的每个元素（由于某种原因除了最后一个元素）必须与之前（在调用函数之前）相同。即你不能改变它（很多）。这与要求创建和返回全新数组一致。