Program transformation as alternative for Hoare logic or temporal logic - MathOverflow

Program transformation as alternative for Hoare logic or temporal logic

2011-07-09T22:27:38Z

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.

Answer by Vijay D for Program transformation as alternative for Hoare logic or temporal logic

2011-07-21T01:32:51Z

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).

Robert Keller, 1976, Formal verification of parallel programs.
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.

David M. R. Park, 1969, Fixpoint induction and proofs of program properties.
Lawrence Flon and Norihisa Suzuki, 1975, Consistent and Complete Proof Rules for the Total Correctness of Parallel Programs.
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.

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.

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.

Answer by Andrej Bauer for Program transformation as alternative for Hoare logic or temporal logic

2011-07-21T06:42:20Z

Hoare logic and temporal logic might be "the only known techniques for proving programs correct" to you, but there are certainly others!

For example, and this list is not exhaustive:

equational reasoning about fixpoints, this works in languages like Haskell
properties of programs can be proved via denotational semantics, which in itself is a vast area including domain theory and game semantics, to name just two.
for certain kinds of programs, for example for parametrically polymorphic ones, there are techniques that go under the name "relational parametricity"
you can use various logical interpretations to get correctness of programs:
- a program extracted as a realizer via the realizability interpretation of logic automatically satisfies a certain specification
- with tools such as Coq you can use type theory to write programs as proofs, or construct programs and prove them correct all at once
- there are other ways of extracting programs from logical statements, one family of which are variants of Gödel's Dialectica interpretation that extract programs from classical logic.

Now, regarding your specific question. I think you should look at realizability, type theory, and extraction of programs from proofs. All of these are "logical" methods for developing correct programs, or proving them correct. Some randomly chosen starting points:

start with something fun and surprising, perhaps Paulo Oliva's tutorial on Programs from classical proofs via Gödel's dialectica interpretation
an accessible paper on realizability interpretation which uses logical methods in computable analysis might be Ulrich Berger's Realisability for Induction and Coinduction with Applications to Constructive Analysis
if you want to use computers to actually show correctness of programs, you could learn Coq and then proceed to Ynot (Hoare logic on steorids) or go straight to Adam Chipala's Certified Programming with Dependent Types.
cool people use Agda instead of Coq.
if you are first-order logic sort of person, you might find Minlog more palatable than Coq and Agda, as it does not throw type theory in your face.

See you in two years.