5
$\begingroup$

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.

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ What you describe, expressing programs in a logical formalism, is extremely broad and the associated literature is immense. You're more likely to get relevant answers if you give a narrower description of what you're interested in. For example, how does it differ from just "write programs in declarative languages"? How does it differ from denotational semantics of programming languages? For that matter, how does it differ from descriptive complexity theory? Each of these is a huge area, and you surely don't want references for all of them (and more). $\endgroup$
    – Andreas Blass
    Commented Jul 10, 2011 at 1:32
  • 1
    $\begingroup$ As Andreas points out, the known techniques are hardly exhausted by Hoare and temporal logic! However, given the thrust of your question, I would suggest looking at "refinement calculus" (see the book of Beck and von Wright: amazon.com/dp/0387984178). The idea in it is to view both programs and specifications as predicate transformers, with programs being a realizable subclass of the predicate transformers. Back also maintains a bibliography at users.abo.fi/backrj/… $\endgroup$
    – Neel Krishnaswami
    Commented Jul 10, 2011 at 8:02
  • $\begingroup$ @Andreas, I edited the question. If you wish, you can fully narrow it down in transforming a program in a FOL + PA expression. Using Hoare logic or transforming it in a FOL + PA expression, is quite a different approach (although at the end it might not be that different). The first approach you find in the standard books and in the Wikipedia, the second not. $\endgroup$
    – Lucas K.
    Commented Jul 10, 2011 at 11:19

2 Answers 2

Reset to default
2
$\begingroup$

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
  2. Pex
Improve this answer
$\endgroup$
12
  • $\begingroup$ Thanks for the answer. The idea that I have is to make a FOL extended with transitive closure, with some axioms for it. The advantage is that it stays rather simple. You don't need an induction axiom anymore, because that can be derived from the axioms of the closure (similar to the Axiom of Infinity). By the way, if you represent graphs as (Godel) numbers, then you can define reachability in FOL + PA. Of course, the graphs must be finite in such case. But you are right, that you can't define reachability if the graph is represented as predicate. $\endgroup$
    – Lucas K.
    Commented Jul 29, 2011 at 21:33
  • $\begingroup$ I'm glad if you found it useful. One should distinguish between a reasoning technique that is sufficient in purely logical terms, one that humans can use, and one that machines can use. I personally think using Goedel numbers is sufficient only in purely logical terms. Various techniques works for humans and machines. Fixed points in particular fit well to automated techniques. The axiom of closure is a special instance of fixed point induction and in that form is widely used in practice. $\endgroup$
    – Vijay D
    Commented Aug 1, 2011 at 0:07
  • $\begingroup$ Vijay. Thanks for your comments. But I don't agree with your second sentence. In my opinion, modern logic should be automatically verified. Otherwise, I call it just mathematics (nothing wrong with that). There are still plenty of possibilities to make automatic verifiable logic better suitable for humans. Goedel numbers are just the bits in the computer. You don't need to confront humans with it. $\endgroup$
    – Lucas K.
    Commented Aug 1, 2011 at 22:21
  • $\begingroup$ Hello Lukas. Just to clarify, I'm talking about machine-generated proofs of program correctness, as opposed to machine-checked proofs. I agree that humans need not confront the gory details of a machine generated proof. Nonetheless, we don't usually want to know a program is correct, we often want some information why, such as invariants. Also, computational complexity and ease of implementation are important concerns in developing a program verifier. I do not know about the ease of implementing a Goedel numbering based verifier. Fixed-point and graph-based methods work well for simple cases. $\endgroup$
    – Vijay D
    Commented Aug 1, 2011 at 23:04
  • $\begingroup$ Ah! I see now the difference. Thanks, I learned something again. The disadvantage of rewriting it in a fixed point, is that you need to use higher order logic. The Functor is a second order logical element. While the method I intended in my question stays within first order logic. The loops can be converted to FOL + PA, while you can't do that with fixed point induction. $\endgroup$
    – Lucas K.
    Commented Aug 1, 2011 at 23:04
4
$\begingroup$

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:

See you in two years.

Improve this answer
$\endgroup$
5
  • $\begingroup$ Thanks for the answer. But the other answer was more the answer I was looking for. Basically, I am looking for methods that are simpler and better accessible for people that are not expert in logic. For those people I think it is interesting to understand the relation between loops and closures. Where the loop is more about programming, the closure is more mathematical. So, this is the bridge between those 2. Coq is for non-logicians too complex. I will take a look at Minlog. $\endgroup$
    – Lucas K.
    Commented Jul 29, 2011 at 21:27
  • $\begingroup$ Andrej, I am reading the tutorial of Minlog. On page 12, they do add-global-assumption. These kind of things you want to avoid, because this way you can introduce inconsistencies in your system. The way I define the predicate in my question is 'safe', because it is a single definition. Taking the transitive reflexive closure is also 'safe'. So, I define the Fibonacci numbers in a safe way, while the tutorial in Minlog isn't. $\endgroup$
    – Lucas K.
    Commented Jul 29, 2011 at 21:47
  • $\begingroup$ I was just commenting on your sweeping statement that "the known techniques are Hoare logic and temporal logics". There are many others. If you are going to educate people about loops, you should show them fixed points and explain how loops are a form of fixed points equations. That in my opinion is much more illuminating, and it is just stanard math (order theory). $\endgroup$
    – Andrej Bauer
    Commented Jul 30, 2011 at 10:26
  • $\begingroup$ Sort of like this: cstheory.stackexchange.com/questions/7029/… $\endgroup$
    – Andrej Bauer
    Commented Jul 30, 2011 at 10:27
  • $\begingroup$ Andreas, I am not familiar with Coq, but I know a little ZFC and HOL Light. As far I know, if one has to transform a computerprogram with a loop to a logical expression in one of those systems, then you end up in making a closure operator somewhere. So, when explaining how programs and systems like ZFC and HOL light are related, then I think you have to start that. From there, one can go to fixed point theorems. I am an outsider, because I do not work on an university. But graduates that start to work in my company, are not capable of defining a mathematical problem in a formal system. $\endgroup$
    – Lucas K.
    Commented Jul 31, 2011 at 20:10

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .