C/C++ - C - conferme asserzioni e ricerca binaria

#include<stdio.h>
#define N 5
main(){
int a[N]={1,2,8,4,5};
int i=0;int somma=0;
for(i=0;i<N-1;i++){
somma=somma+a[i];}
printf("somma %d",somma);}

in questo codice ass. iniziale non c'è
ass. finale che somma=somma el. vettori
invariante 0<=somma<=somma+a[i]
Sono giuste queste affermazioni?

Vorrei sapere inoltre se (cambiando radicalmente argomento) è corretto questo procedimento per cercare il valore tramite ricarca binaria (es. cercare 8)
1 <-
2
3
4
5 <-
6
7
8
9 <-

8 diverso e maggiore di 5,si cerca nella seconda parte,
5 <-
6
7 <-
8
9 <-

diverso da 7,ma maggiore di 7
7 <-
8 <-
9 <-
= 8 ,è presente e si ritorna i=7;

è corretto?
Grazie in anticipo

il ragionamento per la ricerca binaria è corretto...per l'inviariante del ciclo per la somma è sbagliata dato che fare somma + a con a un vettore significa sommare alla variabile somma sempre e solo il primo valore del vettore. Quindi

somma è = 0 se il primo valore di a è uguale a 0
somma però non è sempre <= somma + a dato che anche solo in questo caso abbiamo che somma alla fine arriva a contenere il valore 5, che è > e non <= di 0 + 1.

se ho detto qualche cavolata mi scuso dato che vado di fretta!

intanto grazie di avermi risposto,
quindi devo scrivere che 0<=somma<=somma[0....N-1]?

mah secondo me l'invariante è somma >= 0 e basta

va bene,grazie

non vorrei dire ma facendo somma = somma + a non si ottiene somma più il primo elemento del vettore a, ma si ottiene somma più l'indirizzo al quale è memorizzato il primo elemento del vettore a.

quindi per sommare ogni elemento del vettore si deve fare

int i;
int a[3] = {1, 4, 5};
int somma = 0;

for(i = 0; i < 3; i++)
    somma = somma + a[i];

spero di essere stato chiaro e di aiuto.

in effetti non avevo fatto caso alla mancanza dell'operatore * davanti alla 'a'

grazie 1000 a entrambi,è stata una mia svista nello scrivere il codice,vedendo che funzionava non ho riguardato,grazie ancora