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.



Program transformation as alternative for Hoare logic or temporal logic
It appears to me that the gist of your suggestion is to translate a program into a relation and reason about the transitive closure of that relation. It is orthogonal that this relation is definable in first order arithmetic. 


The idea of translating a program into a relation is rather old and I doubt there is a unique reference for it. I will share what I know, but in each case, there are surely older papers. The first paper below suggests modelling programs as transition systems and reasoning about them. Plotkin's paper provides a way to inductively derive a transition system from program text (though the idea is much older, I'm sure).


1. Robert Keller, 1976, *Formal verification of parallel programs*.
2. Gordon Plotkin, 1981. *Structural Operational Semantics.*


The transition system is essentially the relation you describe. The transitive closure is a fixed point over this relation. It is one of several objects that can be defined by fixed points. Reasoning about properties of programs using fixed points is very old too.


1. David M. R. Park, 1969, *Fixpoint induction and proofs of program properties*.
2. Lawrence Flon and Norihisa Suzuki, 1975, *Consistent and Complete Proof Rules for the Total Correctness of Parallel Programs*.
3. Patrick Cousot and Radhia Cousot, 1977, *Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints*.


Finally, there is a precise mathematical sense in which the fixed point (or transitive closure) approach is not significantly different from Floyd/Hoare logic. 


1. Edmund M. Clarke Jr., 1977, *Program Invariants as Fixed Points*.


To quote from the abstract of the paper:



> 
> We argue that soundness and relative completeness theorems for Floyd-Hoare Axiom Systems ([3], [5], [18]) are really fixedpoint theorems. We give a characterization of program invariants as fixedpoints of functionals which may be obtained in a natural manner from the text of a program. We show that within the framework of this fixedpoint theory, soundness and relative completeness results have a particularly simple interpretation. Completeness of a Floyd-Hoare Axiom System is equivalent to the existence of a fixedpoint for an appropriate functional, and soundness follows from the maximality of this fixedpoint. 
> 
> 
> 


Reasoning about programs by computing fixed points is extremely standard in practice. Rather than relations, we tend to deal with a transformer defined by a relation, such as a predicate or state transformer. If you are genuinely committed to reasoning over relations in a logic, you will require transitive closure logics because properties like graph reachability are not first order definable. I can point to this recent paper, but you will have to dig around for older ones.


1. Neil Immerman, Alexander Rabinovich, Thomas W. Reps, Mooly Sagiv, and Greta Yorsh, 2004, *The Boundary Between Decidability and Undecidability for Transitive Closure Logics*.


Edit: Adding a link.


You might want to try the following verifiers that use a combination of automated reasoning and fixed point techniques. Though they may fail on harder examples, they can still discover useful invariants and errors.


1. [Interproc](http://pop-art.inrialpes.fr/interproc/interprocweb.cgi)
2. [Pex](http://www.pexforfun.com/Default.aspx?language=CSharp&sample=AbsVerified)


