C/C++ - Problema triple di Hoare

Salve a tutti, volevo chiedermi come posso dimostrare con le triple di hoare la correttezza del seguente segmento di codice

do
	{
		n_valori = scanf("%d",
				 &scelta);


		if (n_valori != 1 && (scelta != 0 || scelta != 1))
		{
			printf("Errore!\n");
			while(getchar() != '\n');
		}
		
	} while((n_valori != 1) &&
	  	(scelta != 0 ||
		 scelta != 1));

Grazie

up

Ciao!

Sai come funziano le triple di Hoare? se <Z> è il tuo codice devi trovare una pre-condizione <N> ed una post-condizione <M> che ne garantiscano il successo. Ad esempio una pre-condizione sarebbe verificare che i dati immessi siano effettivamente numeri e non caratteri alfanumerici.
Mentre una post-condizione dovrebbe verificare che i numeri corrispondano a quelli previsti.

Bella pè te!

Grazie intanto per la risposta, si so come funziona una tripla di hoare, ma la cosa che non riesco a fare e passare dal codice ad una precondizione o postcondizione, potresti farmi un esempio?

Grazie

funzione controllavalore(valore)
       valoreRiferimento = lettera
       
       se valore non sarà uguale a lettera
                #codice qua se valore non corrisponde

        se valore sarà uguale a lettera
                 #codice qua se valore corrisponde

Questo barbarico script in pseudocodice dovrebbe darti una idea di una funzione che svolge il ruolo di pre-condizione <N>

Per "creare" il valore di riferimento puoi usare typeid cplusplus.com/reference/typeinfo/type_info/
controlli poi se il tipo di valore, del dato immesso corrisponde e fai seguire il resto del codice, altrimenti lo blocchi.

Ciao ascolta, diciamo che sto capendo meglio, volevo chiederti un'ultima cosa, prendendo questo codice:

                if (n2.forma == ALGEBRICA)
		{
			/* verifico se la parte reale o quella immaginaria sono uguali a zero, in tal caso, significa
			   che si verificherà una divisione per zero */
			if (n2.valore_t.valore_alg.parte_reale == 0 || n2.valore_t.valore_alg.parte_immaginaria == 0)
			{
				divisione_per_zero = TRUE;
			}
		}
		else
		{	
			/* verifico che il modulo se il modulo è uguale a zero, in tal caso,
			   significa che si verificherà una divsione per zero */
			if (n2.valore_t.valore_tri.modulo == 0)
			{
				divisione_per_zero = TRUE;
			}
		}

Quale sarebbe la post-conzione? Ed inoltre da quest'ultima devo risalire alla pre-condiziome, saresti in grado di farmi una dimostrazione completa?

Grazie

Beh è abbastanza difficile parlare di pre-condizioni e post-condizioni senza avere in mente il problema. Se stai cercando di controllare gli errori generati da una divisione per 0, con una pre-condizione, dovresti assicurarti che numeratore e denominatore siano diversi da 0.

Poi cosa intendi con "da quest'ultima devo risalire alla pre-condiziome"

Saluti

Grazie mille, comunque ho deciso di prendere questa parte di codice, dove devo calcolare un nuovo argomento in modo tale che sia compreso nel range [0, 2pi_greco]

double new_arg = fmod(argomento,2_PI_GRECO);
if(new_arg < 0)
{
    new_arg = 2_PI_GRECO + new_arg;
}

Ora data la tripla di hoare {P} S {Q}, dove {Q}, ovvero la postcondizione è:

{0<new_arg<2_PI_GRECO}

quindi la precondizione {2_PI_GRECO +new_arg> 0 /\ 2_PI_GRECO+new_arg > 2_PI_GRECO}
è verificata in quanto {new_arg > -2_PI_GRECO /\ new_arg < 0} e la seconda condzione è verificata dall'if mentre la prima dall'fmod prima dell'if, ore quello che chiedo come posso rappresentare questo ragionamento, con una logica migliore, ovvero scrivendo delle asserzioni corrette ?
Grazie