When trying to prove something about a program, the known techniques are Hoare logic and temporal logics.

An alternative is to transform a program in a mathematical (logical) expression. So, rather that mathematics is used to prove some properties of the program, the program itself is a piece of mathematics.

Loops become transitive reflexive closures. Example, if one has a program that calculates a Fibonacci number. If the program keeps the last two numbers of the Fibonacci sequence in variables, then this be converted by taking the transitive reflexive closure of the relation P, that is true (and only true) for the following situation:

$$ P((x,\space y, \space z), \space (x+1, \space z, \space y+z)) $$

In the original program, the right value is chosen within the loop. In the transitive reflexive closure, the right value must be selected outside the closure (loop). The transformed program is more like a non-deterministic program.

The transformation of a program in a logical expression, can be done automatically.

Although, this is not rocket science, I can not find any reference for this approach. I am busy with writing an article, where this is a part of (it is not the main subject). But I want to refer to the right articles and look if there is interesting material.

Does someone has interesting references?

Many thanks,

Lucas

Edit: Given the comment of Andreas, some clarification. The goal is to make formal reasoning about the program possible. So, transforming the program in a declarative language is insufficient, because the declarative language may not have means to make conclusions about a program, although the language itself might precisely defined. I was thinking in transforming the program in a FOL + PA expression. After such transformation, formal (that is why I tagged with lo.logic) reasoning can be done about the program. As far to my knowledge, I haven't seen this approach (the methods are always more in the direction of Hoare and temporal logics), although it is not very complicated. In my question I didn't want to restrict to FOL + PA.