Domanda Triple di Hoare sul calcolo del determinante di una matrice 2x2

[Crisger]

Buongiorno a tutti, sono uno studente di informatica e il professore ci chiede di verificare la correttezza di una porzione di codice tramite le triple di hoare. Il codice in questione è il seguente:

a= matrice[0][0] * matrice[1][1];

b= matrice[1][0] * matrice[0][1];

det = a - b;

Questa porzione di codice come si può notare calcola il determinante di una matrice 2 x 2, sto però facendo fatica a trovare una post-condizione corretta dalla quale partire.
Quello che mi è venuto in mente è di mettere la post-condizione = det < a - b + 1.
Qualcuno più esperto che mi possa dare una mano?

 

[St3ve]

Classico esercizio troppo stupido per capire che pazzo vuole

Precondizione: la matrice è quadrata.
Postcondizione: typeof(det) == typeof(a) == typeof(b).

In alternativa calcola il determinante della matrice trasposta (in realtà è quello che stai già facendo, quindi raddrizza una moltiplicazione) e verifica che sia uguale a quello calcolato nel codice. Non ho idea di cosa ti vogliano far scrivere.

 

[Crisger]

Esatto, non si capisce cosa voglia. Il discorso è questo, ci è stato assegnato un progetto da fare il quale consiste in una serie di operazioni da fare con delle matrici quadrate. Tra le varie richieste c'è anche quella di prendere una porzione di codice di almeno 3 righe che non contengano istruzioni di input/outpt e farne la tripla. Fin qui tutto bene se non fosse che tra quello che ci è stato spiegato e quello che si trova in internet sono presenti esempi semplici rispetto a quello di qui devo calcolare le triple. Perché tra le richieste c'è anche quella che la sezione di codice scelto non deve essere banale come anche la post-condizione, cosa che va assolutamente a discrezione del prof quindi e un po' una scommessa alla lotteria.

Messaggio unito automaticamente: 18 Agosto 2020

Potrei fare la tripla ad altre porzioni di codice, sinceramente non saprei da dove iniziare perché sono cose del tipo:

if(j >= colonna)   
{
    s_matrice[i][j] = matrice[i][j + 1];
}
else               
{
    s_matrice[i][j] = matrice[i][j];
}

oppure

for (i = 0; i < lato; i++)
{
    for (j = 0; j < lato; j++)
    {
        m_trasposta[j][i] = matrice[i][j];
    }
}

 

[St3ve]

Potrei fare la tripla ad altre porzioni di codice, sinceramente non saprei da dove iniziare perché sono cose del tipo:

for (i = 0; i < lato; i++)
{
    for (j = 0; j < lato; j++)
    {
        m_trasposta[j][i] = matrice[i][j];
    }
}

Postcondizione: det(matrice) == det(m_trasposta). Altrimenti, se ti è permesso farlo: trasposta(trasposta(matrice)) == matrice. Boh, magari nell'altro codice qualcosa di vagamente sensato si riesce a trovare.