Best way to translate while loops to functions for software verification

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.

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.

StackExchange Computer Science Q#96678, answer score: 2