The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

At first glance, I suggest to take a look at Why3 [1].

The translation from your code to Why3ML should be fairly easy, and then you get the benefit of proof automation -- and it also supports Coq as backend..

However, since you ask about putting proof in Latex format, then maybe you should avoid using automated provers and only stick with discharging proof obligations with Coq.

Hope it helps.

[1] http://why3.lri.fr/

On Thu, May 21, 2015 at 11:26 AM, FOURNIER Laurent <laurent.fournier AT irt-saintexupery.com> wrote:

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.