5
$\begingroup$

I have a verification engine where while loops are translated into functional code, like this:

def f() = ... while(c) b ...

def f() = ... fwhile() ...                        
def fwhile() = if(c){ fwhile() } 

We want for the users to be able to annotate while loops with a decreases construct which says that certain measure decreases at each iteration. This is used to prove termination as follows:

while (x > 0) {
 decreases(x)
 x = x - 1
}

The problem is that the checker of the decreases uses the hints given by the preconditions of the functions it is working with. We cannot specify that the precondition is the while loop condition since it may be false at the first call. From my side, I proposed the following translation:

def f() = ... if(c) fwhile() else ...        
def fwhile() = b if(c) fwhile() else ...

I would like to have some feedback on the correctness of my approach as well as if there are any better options, since still this will require moving in function f a part of the while which should be naturally contained in the fwhile function.

$\endgroup$
2
$\begingroup$

I recommend that you translate

while(c) b

to

def myWhile() = if (c) then (b ; myWhile())
myWhile()

With this translation, the precondition of myWhile is the loop invariant of the original while loop. So, this becomes the question of how to find the loop invariant of a loop. In general, that requires manual annotation. If you do a search, you should be able to find a lot of information on finding loop invariants.

$\endgroup$
  • $\begingroup$ @chi, oops, yes, sorry! Fixed. Thank you. $\endgroup$ – D.W. Aug 30 '18 at 18:40
  • $\begingroup$ Isn't def myWhile() = if (c) then (b ; myWhile()) a bit slicker, as then you don't have to have the outer conditional. We just do myWhile(). $\endgroup$ – Andrej Bauer Aug 31 '18 at 6:55
  • $\begingroup$ @AndrejBauer, yes, you're right. For some reason I had thought that the loop invariant for remainder() might be cleaner, but on further reflection I don't think that's the case. I like your construction better. $\endgroup$ – D.W. Aug 31 '18 at 7:20
  • $\begingroup$ however, with the translation proposed by @AndrejBauer I cannot set c as a precondition of myWhile right? $\endgroup$ – Rodrigo Sep 2 '18 at 8:03
  • 1
    $\begingroup$ @Rodrigo, no -- you couldn't do that with either version. That's unlikely to be the correct precondition. $\endgroup$ – D.W. Sep 2 '18 at 16:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.