The Coq mailing list

[FOURNIER Laurent <laurent.fournier AT irt-saintexupery.com>]

Hello everyone,

I’m new on this mailing list…I do not know if posts can be in French or should be in English !

 

My concern is about the following Python code (can be translated in any language !)

________________________________________________

def value(d, f, i, p, k, x):

    assert d>0 and f>=d and x>=0 and x<=100 and i>0 and p>=0 and k>=0 #PRECOND

    if i == 1: return d, 1

    r, s = p if k==i-1 else p-1, 1 if p==1 else 0

    u, v = (i-1)*(p-1)+k+s, (i-1)*(p-1)+k+r

    if v > f: v = f

    t = ((100-x)*u+x*v)//100

    q = (t-1)//i

    return 1+q, t-i*q

 

def simu(d, f, x):

    print ('init:%d final:%d speed:%d' % (d, f, x))

    po, ko, to = d, 0, 0

    for i in range(1, f+10):

        p, k = value(d, f, i, po, ko, x)

        t, po, ko = k*p +(i-k)*(p-1), p, k

        assert p>0 and k>0                  #POST0

        if p == po: assert k<=ko         #POST1

        else: assert p<po and t>=to #POST2

        to = t

        print ('%d: %d*%d+%d*%d=%d' % (i, k, p, i-k, p-1, t))

 

if __name__ == '__main__':

    for j in range (1, 200): # for instance !

        for s in range(101):

            simu(d=j, f=679, x=s)

 

A simple simulation shows that the assertions in POST0,1,2 never raise, but I need a FORMAL PROOF that I can remove those 3 lines and be sure that the post-conditions will always be verified. (All parameters are integers and // means “integer division”)

 

I also need to put the proof in a LaTeX formatted paper if not too long.

 

Question: Is COQ the right tool to get this proof ?

(consider I do not know COQ and do not expect to spend 2 years in training for that)

If the answer is YES, which lab could be able to do the job (get the proof) ?

 

Merci d’avance pour votre aide,

 

Laurent Fournier, PhD.