4 ms·

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?
        catnaroek 10y ago
        It's not. In DbC, you have preconditions and postconditions, but no means whatsoever to actually prove that, whenever the procedure's initial state meets the precondition, its final state will meet the postcondition.
        deleted 10y ago
        [deleted]
        deleted 10y ago
        [deleted]
        Jtsummers 10y ago
        Well, I've found the point disagreement. So design by contract, based on Hoare logic, applied in languages like SPARK Ada and Eiffel, produces statements that are unverifiable. But Hoare logic, a thing without an executable implementation, produces statements which are verifiable.
  - nickpsecurity 10y ago
    SPARK combines those intended specs with language-level details that it feeds to a prover to show conditions hold or errors are absent. How is such Design-by-Contract not formal verification of specific properties of software?
    - catnaroek 10y ago
      I didn't say anything about SPARK, because I know nothing about it. But, if SPARK actually checks that the specs are met, it's doing more than just DbC.
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.)

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?
        catnaroek 10y ago
        It's not. In DbC, you have preconditions and postconditions, but no means whatsoever to actually prove that, whenever the procedure's initial state meets the precondition, its final state will meet the postcondition.
        deleted 10y ago
        [deleted]
        deleted 10y ago
        [deleted]
        Jtsummers 10y ago
        Well, I've found the point disagreement. So design by contract, based on Hoare logic, applied in languages like SPARK Ada and Eiffel, produces statements that are unverifiable. But Hoare logic, a thing without an executable implementation, produces statements which are verifiable.
- nickpsecurity 10y ago
  SPARK combines those intended specs with language-level details that it feeds to a prover to show conditions hold or errors are absent. How is such Design-by-Contract not formal verification of specific properties of software?
  - catnaroek 10y ago
    I didn't say anything about SPARK, because I know nothing about it. But, if SPARK actually checks that the specs are met, it's doing more than just DbC.

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