4 ms·

Floyd–Hoare logic

36 points by iamcurious 11y ago

deleted 11y ago
[deleted]
drdeca 11y ago
This is a cool thing. I've been thinking about this with functions, and trying to think of a way to make a programming language have support for a proof checker for this sort of thing built in, with functions having pre and postconditions, and function bodies that prove the postcondition is true after the function is run, given that the precondition was true before it was run, but I've encountered a problem when one allows first class functions. If one allows first class functions, it seems that it would allow one to make tricks like "if this statement is true, 2+2=5". I'm not sure how to get around it. It's possible that if one actually tried what I am thinking would be the problem, the preprocessor-thing (the thing that validates all the proofs before the program is actually run as a program) might just get into an infinite loop (through infinite recursion). But it doesn't look like that would necessarily happen. And I'm not sure what thing in what I've written should be something that the proof validator should accept, but it certainly does not seem like the proof validator should accept all of it (because it can be used to "prove" anything that can be expressed in the language)
- ahelwer 11y ago
  Look at the Dafny language from MSR: http://research.microsoft.com/en-us/projects/dafny/ http://research.microsoft.com/en-us/projects/dafny/ Your problem is, I think, assuming programs have correctness as an intrinsic property. This is not so. Programs can only be correct with respect to something - some idea born in a human mind, transcribed into something the checker understands (here, pre- and post-conditions). If the human mind wants 2+2 to equal 5 in their program, all power to them - they must only ensure this does not cause inconsistency.
  - mcguire 11y ago
    Should I be concerned that the Dafny tutorial (http://rise4fun.com/Dafny/tutorial/guide http://rise4fun.com/Dafny/tutorial/guide) seems kind of...odd? Getting Started with Dafny: A Guide 1. undefined 2. undefined 3. undefined ...
- tikhonj 11y ago
  You might be interested in the YNot[1] project, which is a library implementing Hoare-style axiomatic semantics in Coq. Just using Coq as the proof language answers a lot of your questions since Coq has well-understood limitations designed to make it useful for automatic proofs. If you're not familiar with the idea of dependent types, it's definitely worth learning about them (and Coq is a good place to start) because they formalize the idea of arbitrary functions at the type level by letting types depend on values, giving you the ability to verify whatever invariants you like. A good place to start would be Benjamin Pierce's free Software Foundations[2] book. There's a really rich theory here with a lot of both theoretical and practical problems worked out but, at the same time, lots of room to develop new ideas and approaches if this is something you're interested in. [1]: http://ynot.cs.harvard.edu/ http://ynot.cs.harvard.edu/ [2]: http://www.cis.upenn.edu/~bcpierce/sf/current/index.html http://www.cis.upenn.edu/~bcpierce/sf/current/index.html
codelion 11y ago
If you are interested in this sort of thing you can also have a look at HIP/SLEEK Verification System - http://loris-7.ddns.comp.nus.edu.sg/~project/TeachHIP/ http://loris-7.ddns.comp.nus.edu.sg/~project/TeachHIP/ It uses separation logic which is an extension of Hoare logic for programs that manipulate the heap.
mcguire 11y ago
Coming from the land of Dijkstra (UTAustin, by the way), pre- and post-conditions were how I learned to think about programs. Things like denotational semantics and what-not seem odd and somehow magical to me, even after a lot of experience with languages like Haskell that incorporate that kind of thinking. I'm not going to get this right because I haven't even thought it out to my own satisfaction, but the fundamental difference seems to me to be that the those things treat a program as a mathematical object in itself, which is one of the reasons they focus on functional languages and immutability. Floyd-Hoare treats the program as a text; it assigns states to the spaces between statements. As a result, it's pretty darn happy with imperative programming, although it has its own limits. (As an aside (Did I mention that I once worked in the same building as Dijkstra, although I never took a class from him.), I find it very amusing that the article has the sentence "There are rules for concurrency, procedures, jumps, and pointers." although neither it nor the linked "Branch" article actually describe Knuth's revelation of Hoare's axioms for goto.)
- AdieuToLogic 11y ago
  Your background immediately reminded me of Betrand Meyer and Design by Contract[1]. I wonder how much of Hoare's work influenced Meyer. Do you care to opine? :-) 1 - http://www.artima.com/intv/contracts.html http://www.artima.com/intv/contracts.html
  - mcguire 11y ago
    I don't know much about Meyer's history and the history of Design by Contract, but I'm going to go out on a limb and say, "quite a bit." The major difference that I can see, with my limited experience, is that DbC seems to be focused on the boundaries between functions and is more closely related to assertions (which are probably also related to Hoare).
- solidangle 11y ago
  Coming from the land of Dijkstra (the Netherlands), I was taught about this in college and it was very cool to use this to prove that post-conditions of a function are actually true (although finding good loop invariants was sometimes a bit annoying. Denotational semantics are horrible in my opinion, but I really like operational semantics (especially structural operational semantics and natural semantics), they still consider a program as a single mathematical object, but like Hoare logic it also tracks the state before and after each statement. It's really easy to work to with (just apply rules), but sadly it's a bit less powerful than Hoare logic, as you can't infer things that hold in general, you can only reason about specific begin states.
techbio 11y ago
Is this not immediately obviously useless?
- ht_th 11y ago
  No. Given a formal specification of a problem, one could use this logic to derive a correct program. In theory, that's great because it is proven error-free. In practice, of course, implementing a "correct program" can introduce bugs and running it on a non-ideal machine (i.e. any physical computer), introduces uncertainties. Furthermore, it is expensive to do: you need people with a strong understanding of mathematics/computer science, it is time intensive, and for most applications, just writing a program is good enough. But, to be honest, that goes for most formal methods. Well, unless they're completely automated, of course.
- pgcosta 11y ago
  Nope. If you want to develop software for critical system(medical appliances, satellites), this should be a must. The only problem is the cost of implementation. On top of that you also have to account that there are non deterministic problems in Hoare logic, like finding the cycle invariant.
- detaro 11y ago
  Why would it be useless?

36 points by iamcurious 11y ago

deleted 11y ago

[deleted]

This is a cool thing. I've been thinking about this with functions, and trying to think of a way to make a programming language have support for a proof checker for this sort of thing built in, with functions having pre and postconditions, and function bodies that prove the postcondition is true after the function is run, given that the precondition was true before it was run, but I've encountered a problem when one allows first class functions. If one allows first class functions, it seems that it would allow one to make tricks like "if this statement is true, 2+2=5". I'm not sure how to get around it. It's possible that if one actually tried what I am thinking would be the problem, the preprocessor-thing (the thing that validates all the proofs before the program is actually run as a program) might just get into an infinite loop (through infinite recursion). But it doesn't look like that would necessarily happen. And I'm not sure what thing in what I've written should be something that the proof validator should accept, but it certainly does not seem like the proof validator should accept all of it (because it can be used to "prove" anything that can be expressed in the language)

ahelwer 11y ago
Look at the Dafny language from MSR: http://research.microsoft.com/en-us/projects/dafny/ http://research.microsoft.com/en-us/projects/dafny/ Your problem is, I think, assuming programs have correctness as an intrinsic property. This is not so. Programs can only be correct with respect to something - some idea born in a human mind, transcribed into something the checker understands (here, pre- and post-conditions). If the human mind wants 2+2 to equal 5 in their program, all power to them - they must only ensure this does not cause inconsistency.
- mcguire 11y ago
  Should I be concerned that the Dafny tutorial (http://rise4fun.com/Dafny/tutorial/guide http://rise4fun.com/Dafny/tutorial/guide) seems kind of...odd? Getting Started with Dafny: A Guide 1. undefined 2. undefined 3. undefined ...
tikhonj 11y ago
You might be interested in the YNot[1] project, which is a library implementing Hoare-style axiomatic semantics in Coq. Just using Coq as the proof language answers a lot of your questions since Coq has well-understood limitations designed to make it useful for automatic proofs. If you're not familiar with the idea of dependent types, it's definitely worth learning about them (and Coq is a good place to start) because they formalize the idea of arbitrary functions at the type level by letting types depend on values, giving you the ability to verify whatever invariants you like. A good place to start would be Benjamin Pierce's free Software Foundations[2] book. There's a really rich theory here with a lot of both theoretical and practical problems worked out but, at the same time, lots of room to develop new ideas and approaches if this is something you're interested in. [1]: http://ynot.cs.harvard.edu/ http://ynot.cs.harvard.edu/ [2]: http://www.cis.upenn.edu/~bcpierce/sf/current/index.html http://www.cis.upenn.edu/~bcpierce/sf/current/index.html

codelion 11y ago

If you are interested in this sort of thing you can also have a look at HIP/SLEEK Verification System - http://loris-7.ddns.comp.nus.edu.sg/~project/TeachHIP/ http://loris-7.ddns.comp.nus.edu.sg/~project/TeachHIP/ It uses separation logic which is an extension of Hoare logic for programs that manipulate the heap.

mcguire 11y ago

Coming from the land of Dijkstra (UTAustin, by the way), pre- and post-conditions were how I learned to think about programs. Things like denotational semantics and what-not seem odd and somehow magical to me, even after a lot of experience with languages like Haskell that incorporate that kind of thinking. I'm not going to get this right because I haven't even thought it out to my own satisfaction, but the fundamental difference seems to me to be that the those things treat a program as a mathematical object in itself, which is one of the reasons they focus on functional languages and immutability. Floyd-Hoare treats the program as a text; it assigns states to the spaces between statements. As a result, it's pretty darn happy with imperative programming, although it has its own limits. (As an aside (Did I mention that I once worked in the same building as Dijkstra, although I never took a class from him.), I find it very amusing that the article has the sentence "There are rules for concurrency, procedures, jumps, and pointers." although neither it nor the linked "Branch" article actually describe Knuth's revelation of Hoare's axioms for goto.)

AdieuToLogic 11y ago
Your background immediately reminded me of Betrand Meyer and Design by Contract[1]. I wonder how much of Hoare's work influenced Meyer. Do you care to opine? :-) 1 - http://www.artima.com/intv/contracts.html http://www.artima.com/intv/contracts.html
- mcguire 11y ago
  I don't know much about Meyer's history and the history of Design by Contract, but I'm going to go out on a limb and say, "quite a bit." The major difference that I can see, with my limited experience, is that DbC seems to be focused on the boundaries between functions and is more closely related to assertions (which are probably also related to Hoare).
solidangle 11y ago
Coming from the land of Dijkstra (the Netherlands), I was taught about this in college and it was very cool to use this to prove that post-conditions of a function are actually true (although finding good loop invariants was sometimes a bit annoying. Denotational semantics are horrible in my opinion, but I really like operational semantics (especially structural operational semantics and natural semantics), they still consider a program as a single mathematical object, but like Hoare logic it also tracks the state before and after each statement. It's really easy to work to with (just apply rules), but sadly it's a bit less powerful than Hoare logic, as you can't infer things that hold in general, you can only reason about specific begin states.

techbio 11y ago

Is this not immediately obviously useless?

ht_th 11y ago
No. Given a formal specification of a problem, one could use this logic to derive a correct program. In theory, that's great because it is proven error-free. In practice, of course, implementing a "correct program" can introduce bugs and running it on a non-ideal machine (i.e. any physical computer), introduces uncertainties. Furthermore, it is expensive to do: you need people with a strong understanding of mathematics/computer science, it is time intensive, and for most applications, just writing a program is good enough. But, to be honest, that goes for most formal methods. Well, unless they're completely automated, of course.
pgcosta 11y ago
Nope. If you want to develop software for critical system(medical appliances, satellites), this should be a must. The only problem is the cost of implementation. On top of that you also have to account that there are non deterministic problems in Hoare logic, like finding the cycle invariant.
detaro 11y ago
Why would it be useless?