prouver l'exactitude d'un programme

Question

La fonction trouve de manière récursive et retourne le plus petit élément à partir d'une matrice qui a des éléments entiers

Min(A, b, e) 
if (b=e) 
    return A[b] 
m = (b+e)/2 // floor is taken 
x = Min(A, b, m) 
y = Min(A, m +1, e) 
If(x < y) 
    return x 
else 
    return y 

Ma condition est: b et e sont des nombres entiers supérieurs à zéro

Mon poste condition est: retourner un entier x ou y (pas sûr à ce sujet)

Alors, comment puis-je prouver cela est exact en montrant que le pré et l'état de poste sont inductifs

Désolé pour le format, nouveau pour cela.

Answer 1

Preuve: la preuve est par induction mathématique.

Cas de base: considérons le cas où b = e. Nous examinons une partie de la liste A avec la taille 1; l'élément minimum d'une liste avec un élément est le seul élément de la liste, que l'algorithme renvoie dans ce cas. Hypothèse d'induction: Supposons maintenant que l'algorithme renvoie correctement l'élément minimum pour toutes les listes de taille jusqu'à et y compris k. Pour prouver: il renvoie la valeur minimale pour les listes jusqu'à la taille k + 1.

Pas d'induction: On a e = b + k + 1 et on veut montrer qu'on retourne l'élément minimum. Nous savons que m sera égal à (e + b)/2 = (2b + k + 1)/2 = b + (k + 1)/2. Cela va diviser la liste de taille k + 1 en deux parties de taille plancher ((k + 1)/2) et cieling ((k + 1)/2). Ces deux valeurs sont inférieures ou égales à k pour toutes les valeurs de k supérieures à zéro (notre scénario de base commence à k = 1, ce qui signifie que nous sommes bons). Ainsi, par l'hypothèse d'induction, x est la valeur minimale de la moitié inférieure de la liste, et y est la valeur minimale de la moitié supérieure de la liste. L'algorithme renvoie x s'il est inférieur à y et y sinon. Puisque la valeur minimale dans la liste A doit apparaître dans la moitié de la liste, et que nous renvoyons la moindre des valeurs minimales des deux moitiés de A, nous savons que nous retournons la valeur minimale dans A. Cela conclut la démonstration.