3 ms·
Proving that a program meets its specification.
by catnaroek 10y ago
Proving that a program meets its specification.
- Jtsummers 10y agoIs Hoare logic a tool in that process?
- catnaroek 10y agoYes. 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 agoDesign by contract, is it based or not based on Hoare logic?
- catnaroek 10y agoIt'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 agoWell, 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.
- naasking 10y ago> 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. Except many implementations of design by contract execute the postcondition check and raise an exception if it's not satisfied, so I don't think your statement is correct.
- catnaroek 10y agoThe very reason why you need to raise the exception is because the postcondition doesn't hold. The point to verification is to make sure the postcondition holds. So I stand by my original assertion: DbC isn't verification.
- nickpsecurity 10y agoIf I were to categorize it, I'd call DbC formal specification that, combined with Eiffel or SPARK tools, can be used to verify that interfaces or code maintain those specific properties. It's a partial form of formal specification and verification that's still useful. It doesn't have to be fully specified or proven to count as formal verification. Partial verification is a thriving field.
- catnaroek 10y agoYep, that's perfectly reasonable.