7 ms·

Very cool. I've long that that having formal program verification built in to a language and run as part of the compiler is the way forward. Giving the pre and

Very cool. I've long that that having formal program verification built in to a language and run as part of the compiler is the way forward. Giving the pre and post-conditions for a function is much more reasonable than dropping down to a verification tool like Coq or TLA+. I know that AWS uses TLA+ to reason about the correctness of algorithms.

Jtsummers 10y ago
Design by Contract: http://c2.com/cgi/wiki?DesignByContract http://c2.com/cgi/wiki?DesignByContract Which is a key element of the Eiffel language ( https://en.wikipedia.org/wiki/Eiffel_(programming_language) https://en.wikipedia.org/wiki/Eiffel_(programming_language) ). SPARK Ada also includes this concept of pre/post conditions: https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) I haven't programmed in the latter, but I'd like to. Since I'm often in the maintenance end of the software cycle I don't have much opportunity (professionally) to introduce new languages (new tools, yes, but not new languages). I have a coworker who thinks we do this with asserts (in C and C++), but it's only half the battle. The asserts only tell us that our exercised version of the program (through our non-comprehensive testing) hasn't failed pre/post-conditions. It's helpful, but not sufficient.
- catnaroek 10y ago
  Design by contract has nothing to do with formal verification, though.
  - Jtsummers 10y ago
    Respectfully, I have to disagree. Design by contract is, or can be, a component of formal verification. If it's all you've got, it's probably better than nothing. Design by contract brings the concept of using preconditions, postconditions, invariants, and other contractual objects into the design and implementation of the software. These are able (depending on implementation) to be analyzed statically by machine or by hand, or dynamically during testing (with some systems the tests can be automatically generated to exercise the contracts). This may not be the limit or ideal of formal verification, but it is certainly a part of it and a good measure forward compared to the typical approaches used in our industry. EDIT: Let's settle a pertinent question first: Is Hoare logic a tool/approach for formal verification? If it is, then design by contract (being largely based on the concept of Hoare logic) is also a tool/approach for formal verification. The potential points of disagreement, as I see them, are that Hoare logic is not a tool for formal verification, or that design by contract is not based on Hoare logic. Is there something else that I've missed or are these the points of disagreement?
    - catnaroek 10y ago
      Design by contract forces you to be explicit about your intended preconditions and postconditions. But “intended” isn't the same thing as “actual”. Verification is making sure that the preconditions and postconditions actually hold, in every possible case where the statement (or procedure or whatever) could be reached. EDIT: Hoare logic is a tool for formal verification, indeed. DbC is not, though.
      - Jtsummers 10y ago
        We're talking around each other. What is your definition of formal verification?
        catnaroek 10y ago
        Proving that a program meets its specification.
        Jtsummers 10y ago
        Is Hoare logic a tool in that process?
        catnaroek 10y ago
        Yes. Hoare logic's inference rules define which Hoare triples can be “legally” derived. The programmer's task isn't only to provide a Hoare triple (which by itself is just an assertion that a program meets a specification), but also to provide a derivation of that triple (the actual proof of the assertion). Design by contract is akin to giving a Hoare triple, but never giving its derivation.
        Jtsummers 10y ago
        Design by contract, is it based or not based on Hoare logic?
  - Jtsummers 10y ago
    My last statement, since you've edited several of your comments without marking them as edited which makes this conversation, well, not an accurate account of our dialogue. Thanks for that. You state that design by contract has nothing to do with formal verification. You also later said that Hoare logic is a tool for formal verification. Design by contract is an implementation/application of Hoare logic. Ergo, it has something to do with formal verification. I've never said it is formal verification, I've only said that it is part of it. It requires tooling and proper application for it to be useful/correct/effective. But that's true of everything in formal verification.
  - paulddraper 10y ago
    Design by contact is more or less a prerequisite to formal verification. If you don't have a well-defined contact, you won't be able to verify that context is adhered to.
    - Animats 10y ago
      Exactly. The way this works in practice is that functions have ENTRY and EXIT conditions. When verifying the function in isolation, the ENTRY conditions are assumed true, and the verification process attempts to verify that the EXIT conditions will then hold. When verifying a caller, the verification system must verify at each call that the ENTRY conditions hold, and can then assume, after the call, that the EXIT conditions are true. You can extend this to objects. Objects have invariants, which must be true whenever control is outside the function. So an object invariant is both an ENTRY and and an EXIT invariant for all exported functions. (This is the source of the idea that objects should have "getters" and "setters", rather than exporting fields for external access. You need some place to check the object invariant.) (When is control inside an object? It's complicated. A strict language on this would have public and private functions, and you wouldn't be allowed to call public functions from private ones, because that's a re-entry. There's also the problem of calling "out the bottom" of an object and eventually re-entering the object. Classic source of bugs in GUIs, which are collections of objects that call each other up, down, and sideways. And if you block inside an object, is it unlocked? Spec# addressed all this, with difficultly.)
- wyldfire 10y ago
  Well, there's a great aside in this thread as to whether or no DbC applies here in a discussion of formal verification and that's good stuff. But I figured it was relevant to mention that there are both an RFC [1] on adding DbC as a language feature and a library [2]. [1] https://github.com/rust-lang/rfcs/issues/1077 https://github.com/rust-lang/rfcs/issues/1077 [2] https://github.com/nrc/libhoare https://github.com/nrc/libhoare
pron 10y ago
> Giving the pre and post-conditions for a function is much more reasonable than dropping down to a verification tool like Coq or TLA+ Reasonable for what? The design hypothesis behind a high-level specification/verification tool like TLA+ is that no language is currently capable of being reasoned-about in such a way that large, complex applications can be verified affordably. So far, this hypothesis holds. Language-level verification is therefore valuable when you either need to verify very local properties (pre/post conditions of a single subroutine, that is very important and/or tricky) or you need to do full end-to-end verification, in which case you will be able to verify only relatively small and simplified programs (like seL4 or CompCert) and at a very high cost (reasonable for high-assurance software only). So language-level verification and high-level specification and verification are currently useful for very different things.

Jtsummers 10y ago

Design by Contract: http://c2.com/cgi/wiki?DesignByContract http://c2.com/cgi/wiki?DesignByContract Which is a key element of the Eiffel language ( https://en.wikipedia.org/wiki/Eiffel_(programming_language) https://en.wikipedia.org/wiki/Eiffel_(programming_language) ). SPARK Ada also includes this concept of pre/post conditions: https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) I haven't programmed in the latter, but I'd like to. Since I'm often in the maintenance end of the software cycle I don't have much opportunity (professionally) to introduce new languages (new tools, yes, but not new languages). I have a coworker who thinks we do this with asserts (in C and C++), but it's only half the battle. The asserts only tell us that our exercised version of the program (through our non-comprehensive testing) hasn't failed pre/post-conditions. It's helpful, but not sufficient.

catnaroek 10y ago
Design by contract has nothing to do with formal verification, though.
- Jtsummers 10y ago
  Respectfully, I have to disagree. Design by contract is, or can be, a component of formal verification. If it's all you've got, it's probably better than nothing. Design by contract brings the concept of using preconditions, postconditions, invariants, and other contractual objects into the design and implementation of the software. These are able (depending on implementation) to be analyzed statically by machine or by hand, or dynamically during testing (with some systems the tests can be automatically generated to exercise the contracts). This may not be the limit or ideal of formal verification, but it is certainly a part of it and a good measure forward compared to the typical approaches used in our industry. EDIT: Let's settle a pertinent question first: Is Hoare logic a tool/approach for formal verification? If it is, then design by contract (being largely based on the concept of Hoare logic) is also a tool/approach for formal verification. The potential points of disagreement, as I see them, are that Hoare logic is not a tool for formal verification, or that design by contract is not based on Hoare logic. Is there something else that I've missed or are these the points of disagreement?
  - catnaroek 10y ago
    Design by contract forces you to be explicit about your intended preconditions and postconditions. But “intended” isn't the same thing as “actual”. Verification is making sure that the preconditions and postconditions actually hold, in every possible case where the statement (or procedure or whatever) could be reached. EDIT: Hoare logic is a tool for formal verification, indeed. DbC is not, though.
    - Jtsummers 10y ago
      We're talking around each other. What is your definition of formal verification?
      - catnaroek 10y ago
        Proving that a program meets its specification.
        Jtsummers 10y ago
        Is Hoare logic a tool in that process?
        catnaroek 10y ago
        Yes. Hoare logic's inference rules define which Hoare triples can be “legally” derived. The programmer's task isn't only to provide a Hoare triple (which by itself is just an assertion that a program meets a specification), but also to provide a derivation of that triple (the actual proof of the assertion). Design by contract is akin to giving a Hoare triple, but never giving its derivation.
        Jtsummers 10y ago
        Design by contract, is it based or not based on Hoare logic?
- Jtsummers 10y ago
  My last statement, since you've edited several of your comments without marking them as edited which makes this conversation, well, not an accurate account of our dialogue. Thanks for that. You state that design by contract has nothing to do with formal verification. You also later said that Hoare logic is a tool for formal verification. Design by contract is an implementation/application of Hoare logic. Ergo, it has something to do with formal verification. I've never said it is formal verification, I've only said that it is part of it. It requires tooling and proper application for it to be useful/correct/effective. But that's true of everything in formal verification.
- paulddraper 10y ago
  Design by contact is more or less a prerequisite to formal verification. If you don't have a well-defined contact, you won't be able to verify that context is adhered to.
  - Animats 10y ago
    Exactly. The way this works in practice is that functions have ENTRY and EXIT conditions. When verifying the function in isolation, the ENTRY conditions are assumed true, and the verification process attempts to verify that the EXIT conditions will then hold. When verifying a caller, the verification system must verify at each call that the ENTRY conditions hold, and can then assume, after the call, that the EXIT conditions are true. You can extend this to objects. Objects have invariants, which must be true whenever control is outside the function. So an object invariant is both an ENTRY and and an EXIT invariant for all exported functions. (This is the source of the idea that objects should have "getters" and "setters", rather than exporting fields for external access. You need some place to check the object invariant.) (When is control inside an object? It's complicated. A strict language on this would have public and private functions, and you wouldn't be allowed to call public functions from private ones, because that's a re-entry. There's also the problem of calling "out the bottom" of an object and eventually re-entering the object. Classic source of bugs in GUIs, which are collections of objects that call each other up, down, and sideways. And if you block inside an object, is it unlocked? Spec# addressed all this, with difficultly.)
wyldfire 10y ago
Well, there's a great aside in this thread as to whether or no DbC applies here in a discussion of formal verification and that's good stuff. But I figured it was relevant to mention that there are both an RFC [1] on adding DbC as a language feature and a library [2]. [1] https://github.com/rust-lang/rfcs/issues/1077 https://github.com/rust-lang/rfcs/issues/1077 [2] https://github.com/nrc/libhoare https://github.com/nrc/libhoare

pron 10y ago

> Giving the pre and post-conditions for a function is much more reasonable than dropping down to a verification tool like Coq or TLA+ Reasonable for what? The design hypothesis behind a high-level specification/verification tool like TLA+ is that no language is currently capable of being reasoned-about in such a way that large, complex applications can be verified affordably. So far, this hypothesis holds. Language-level verification is therefore valuable when you either need to verify very local properties (pre/post conditions of a single subroutine, that is very important and/or tricky) or you need to do full end-to-end verification, in which case you will be able to verify only relatively small and simplified programs (like seL4 or CompCert) and at a very high cost (reasonable for high-assurance software only). So language-level verification and high-level specification and verification are currently useful for very different things.