x = 12.3

s = 1
n = 1

while s <= x :
    n = n + 1
    s = s + 1/n



'''Notons C la condition C(x,s) = (s <= x)

Montrons par récurrence que le programme termine et qu'il rend bien le bon
résultat. C'est-à-dire, qu'à la sortie de la boucle, s contient bien s_n et
n correspond bien à l'entier N recherché.

Initialisaton : à l'entrée dans la boucle, donc à la première évaluation de C,
n contient 1, s contient s1=1.

Hérédité ; supposons qu'au moment de la kième évaluation de C, n contienne k
et s contienne sk, alors la condition d'arrêt (non (C)) = (s > x) est réalisée
et le programme termine, soit n est incrémenté et s subit l'affectation
s = s + 1/n. A l'évaluation suivante, n contient k+1 et s contient
sk + 1/(k+1) = s_(k+1).

En conséquence, nous avons montré que lorsque k est le nombre d'évaluations
de la condition C, n contient k et s contient s_k.

Par ailleurs si lim s_k = + infini, alors il existe un plus petit entier
k0 tel que s_(k0) > x. Le programme termine. Le contenu de n est la
valeur N attendue puisque la condition d'arrêt est vérifiée et que pour
n-1 elle ne l'était pas.

'''



''' En pratique, les nombres s_k sont stockés sous forme de flottants
et dès que 1/k est de l'ordre de 10^-7, l'arrondi de sk +1/k redonne sk. La
suite devient stationnaire. L'algorithme ne termine pas. '''