CODEWITHSUNDEEP
clogichoare-logic
Porchetta17
Porchetta17

Reputation: 13

How to verify that function with Hoare Triple?

As the title says, how can I verify the function below with the Hoare Triple? I read various lectures about it but I can't figure out how to do it.

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);
}

Upvotes: 1

Views: 290

Answers (1)

Paul Ogilvie
Paul Ogilvie

Reputation: 25286

To prevent a long discussion in comments, I'll try to write some pre- and post conditions.

As it is not possible to test inside the function whether it is called with pointers to valid list objects, that falls to the parent/the caller:

// 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);
}

I hope this is something that you and you professor can work with.

{P}: The function must be called with pointers that are either null or point to valid list elements.

C: uguaglianza_insiemi( *A, *B)

{Q}: function result reflects equality of the lists

Inside the function, this continues with the if statement using the rule of composition.

Upvotes: 3

Related Questions