Как проверить эту функцию с помощью Hoare Triple?

Как следует из названия, как я могу проверить приведенную ниже функцию с помощью Hoare Triple? Я читал различные лекции об этом, но я не могу понять, как это сделать.

int uguaglianza_insiemi(elem_lista_t *insieme_A,
                        elem_lista_t *insieme_B)
{
    int esito;  

    if ((insieme_A == NULL) && 
        (insieme_B == NULL))
        esito = 1;

    else if (insieme_A == NULL ||
            insieme_B == NULL)
            esito = 0;

    else if (insieme_A->valore != insieme_B->valore) 
            esito = 0;

    else esito = uguaglianza_insiemi(insieme_A->succ_p,
                                     insieme_B->succ_p);

    return (esito);
}

c logic hoare-logic
person Porchetta17    schedule 27.05.2019    source источник
comment
Вам нужно написать предусловия P и постусловия Q и доказать, что если предусловия выполняются, постусловие будет выполнено после обработки. Например, предварительным условием является то, что insiema_A и B либо равны нулю, либо указывают на допустимый элемент списка.   -  person Paul Ogilvie    schedule 27.05.2019
comment
Итак, мне нужно написать и установить предварительные условия и постусловия? В своей лекции я прочитал, что если функция рекурсивная, я также могу решить ее с помощью метода индукции, я немного запутался   -  person Porchetta17    schedule 27.05.2019
comment
Индукция здесь, вероятно, означает, что если первый вызов был правильным, и программа (функция) верна, то и каждый следующий вызов будет правильным. Но вам все равно нужно написать эти предварительные и последующие условия.   -  person Paul Ogilvie    schedule 27.05.2019
comment
Вы можете написать операторы или assert() для проверки условий до и после. Единственное, что функция не может проверить, это то, что при первом вызове она была вызвана с указателями, если они не нулевые, на объекты, которые являются допустимыми элементами списка. C позволяет с помощью приведений вызывать функцию с указателями на мусор.   -  person Paul Ogilvie    schedule 27.05.2019
comment
Хорошо, спасибо за подсказку, мне нужно только понять, как написать эти условия, например, если я возьму это предварительное условие, которое вы написали: insieme_A и B либо равны нулю, либо указывают на допустимый элемент списка. , я должен написать пост-условие, связанное с этим предварительным условием?   -  person Porchetta17    schedule 27.05.2019
comment
Вы можете написать предварительные и последующие условия либо на естественном языке, либо на каком-то формальном языке, либо с помощью операторов C.   -  person Paul Ogilvie    schedule 27.05.2019
comment
Я хотел бы спросить вас, можете ли вы представить несколько примеров моего кода! Вы могли бы это сделать?   -  person Porchetta17    schedule 27.05.2019

Ответы (1)


arrow_upward
2
arrow_downward

Чтобы не было долгих дискуссий в комментариях, попробую написать некоторые пре- и пост-условия.

Поскольку внутри функции невозможно проверить, вызывается ли она с указателями на действительные объекты списка, это относится к родителю/вызывающему:

// The following function must be called with pointers that are either null
// or point to valid list elements. The lists must be correct (no malloc bugs etc).
// The compiler must have checked that it is called with pointers to the proper types,
// as C has no typeof operator.
//
int uguaglianza_insiemi(elem_lista_t *insieme_A,
                        elem_lista_t *insieme_B)
{
    int esito;  

    if ((insieme_A == NULL) && 
        (insieme_B == NULL))
        esito = 1;    // both pointers are null: equal

    // not both pointes are null
    else if (insieme_A == NULL ||
            insieme_B == NULL)
            esito = 0;    // not both pointers are null, but one is: not equal

    // neither pointer is null and so they may be dereferenced
    else if (insieme_A->valore != insieme_B->valore) 
            esito = 0;    // neither pointer is null, but their element values aer not equal: not equal


    // the function can be called recursively now because its precondition has been met,
    // that both successor pointers are null or point to valid list elements (induction).
    else esito = uguaglianza_insiemi(insieme_A->succ_p,
                                     insieme_B->succ_p);
    // the post condition is that esito reflects equality of both (partial) lists                    
    return (esito);
}

Я надеюсь, что это то, с чем вы и ваш профессор сможете работать.

{P}: функция должна вызываться с указателями, которые либо являются нулевыми, либо указывают на допустимые элементы списка.

C: uguaglianza_insiemi( *A, *B)

{Q}: результат функции отражает равенство списков

Внутри функции это продолжается оператором if с использованием правила композиции.

person Paul Ogilvie    schedule 27.05.2019
comment
@Porchetta17, если вы считаете ответ полезным, вы должны принять его, см. stackoverflow.com/help/someone-answers - person alinsoar; 05.06.2019