контракты в Яве - PullRequest
Новая
       46

контракты в Яве

2 голосов
/ 31 марта 2011

Я пытаюсь узнать больше о значении контрактов в 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. как мой код должен измениться согласно второму контракту?

Спасибо, ребята.

Ответы [ 2 ]

4 голосов
/ 31 марта 2011

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. что означает это "И"?

AND является логическим соединением .Он оценивает true, если оба аргумента / утверждения true.

4. как мой код должен измениться согласно второму контракту?

Вы не должныбросить и исключения или изменить массив любым способом, если он не соответствует гипотезе (часть до ==>).В этом случае массив (и / или возвращаемое значение) должен быть изменен в соответствии с заключением.

2 голосов
/ 31 марта 2011

Я не могу утверждать, что знаю, но вот мое толкование данных условий.

Прежде всего, ваш код фактически не соответствует ни одному из контрактов.Это нарушает условия $ret != arr и forall 0 <= i < arr.length-1, $prev(arr[i]) == arr[i].

  1. Поскольку оба условия требуют, чтобы вы не мутировали arr (через постусловие forall 0 <= i < arr.length-1, $prev(arr[i]) == arr[i] и все условия (pre и post) в первом - условия post во втором, контракты одинаковы Первый требует броска ошибок, если предварительные условия не выполнены. Второй означает, что вы должны просто что-то вернуть (например, nullили arr или любое другое значение), если arr является нулевым или иным образом недействительным.

  2. Вы , вероятно, должны выдать исключение недопустимого аргумента, когда предусловиянарушил (но, возможно, вам следует поговорить об этом с человеком, который дает вам контракт).

  3. Я предполагаю AND логически и сопоставляет условия вместе, как если бы они были описаны отдельно (но может использоваться вместе с OR s для большей гибкости)

  4. Это не нужно. Вместо броска IllegalArgumentException, когда преконДостижения не выполнены, возврат null

Редактировать для комментариев:

Я считаю, $ret != arr означает, что возвращаемое значение не может относиться к тому же int[]как arr.То есть вы должны создать новый int[] где-нибудь в вашей функции и вернуть его.

forall 0 <= i < arr.length-1, $prev(arr[i]) == arr[i] означает, что каждый элемент arr (кроме последнего по некоторым причинам) должен быть таким же, какэто было ранее (до вызова функции).то есть вы не можете изменить его (много).Это согласуется с требованием создания и возврата совершенно нового массива.

...