44 ms·

> The real value comes when you do it with the knowledge of the mathematics in hand because then it allows you to prove your Program as "Correct" (w.r.t. a spec

> The real value comes when you do it with the knowledge of the mathematics in hand because then it allows you to prove your Program as "Correct" (w.r.t. a specification). At the risk of nitpicking: Certainly it's a benefit to structure and understand code such that you can reason about it effectively, but prove goes too far. Almost no real code is proven correct, the ergonomics of formal methods are still far too poor for that.

rramadass 1y ago
It depends; the "proving" can be done at a gross high level function or fine grained at statement level. Thus in the former case one could use Meyer's Design-by-Contract (aka DbC) while in the latter case one might choose to follow a detailed Dijkstra methodology. For both of the above you don't need any special tools (eg. Z/VDM/TLA+/Coq/Lean etc.) but merely the knowledge to learn to think about a Program using Mathematical Concepts. For most "ordinary" software, DbC would be enough while for critical software one might want to go with the whole nine yards using chosen methodologies/tools. Note that usage of the methodologies/tools themselves require a knowledge of the above-mentioned Mathematics. The point was that a knowledge of the requisite Mathematics gives you a very powerful way of viewing Programs and then you get to choose how to map/implement it using any number of tools and based on the needs of the software.
- MaxBarraclough 1y ago
  Design-by-contract typically refers to runtime checking of invariants, which is not the equivalent of formal verification. It should not be referred to as proving correctness. It doesn't do so. If you want to prove your program's correctness, that's the domain of formal methods, essentially by definition.
  - rramadass 1y ago
    This argument has been made before and that is why i said it depends and put "proving" within quotes. It is a very narrow and wrong way of looking at Formal Methods (both Specification and Verification) and one of the main reasons the "ordinary" software engineer gets intimidated and overawed by formal methods and afraid to even approach the subject (as my comments to user cubefox shows). A Formal Method defined broadly is the application of Mathematical Concepts/Models and Logic to the specification/implementation/verification of Computer Programs. DbC is based on Hoare Logic where you try to "prove" the program intellectually and not necessarily tool driven. This was somewhat mechanized (though still a intellectual pursuit) by Dijkstra's technique of deriving weakest-preconditions. Because the whole process can be quite tedious, laborious and rather complex, automatic theorem prover tools were invented to do the job for you. This has resulted in the unfortunate status quo where Formal Specification/Verification have become identified with the use of tools and not the Mathematics behind them. Proving Correctness need not be fine-grained and absolute but can be good enough done partially at a gross level at specific stages in a program as needed and done either by hand and/or using tools. DbC can be considered a lightweight Formal Method with aspects of both Specification and Verification included. The Programmer plays the role of "theorem prover" when using DbC. However tools exist to map "Design-by-Contract" constructs to "Verified Design-by-Contract" constructs. See for example https://www.eschertech.com/products/verified_dbc.php https://www.eschertech.com/products/verified_dbc.php. Also Eiffel (quintessential DbC language) can be converted using AutoProof to a form which can be proven by Boogie verifier. Finally; here is a case study Design by contract formal verification for automotive embedded software robustness (abstract & pdf) - https://hal.sorbonne-universite.fr/ERTS2024/hal-05028176v1 https://hal.sorbonne-universite.fr/ERTS2024/hal-05028176v1
    - MaxBarraclough 1y ago
      > that is why i said it depends and put "proving" within quotes I feel I need to insist on this point: a design-by-contract methodology using runtime checking may be an effective means of improving software quality, but it certainly isn't proving the correctness of a program. Using the word 'prove' here is just plain wrong. Putting it in quotation marks doesn't help. It simply does not constitute a proof. > It is a very narrow and wrong way of looking at Formal Methods (both Specification and Verification) and one of the main reasons the "ordinary" software engineer gets intimidated and overawed by formal methods and afraid to even approach the subject I'm not insisting on a narrow understanding of formal methods, I'm insisting on proper use of established terminology. I'm all for practical methodologies that benefit software quality without paying the enormous costs of fully applying formal methods. Design-by-contract with runtime checking seems like a reasonable approach. (Static typing is another. Effect-oriented programming might be another.) My point was just about the proper use of the word proof. > Proving Correctness need not be fine-grained and absolute but can be good enough done partially at a gross level at specific stages in a program as needed and done either by hand and/or using tools. A program is proven correct only when the proof is absolute, which implies fine-grained. I'm not opposed to the use of partial proofs or 'good enough' proof-sketches, both of which could be useful in producing high-quality software in the real world, but we should be clear in how we refer to them. I'm not sure about the idea of proving correctness by hand, though. Manually applying a formal model of a real programming language sounds unworkable. If code is well structured, it should be possible for the programmer to reason about it somewhat precisely, like a proof-sketch, but that's not a proof of correctness. > The Programmer plays the role of "theorem prover" when using DbC I don't find this convincing. There's nothing stopping the programmer from failing to notice some error. If you aren't actually doing a proof, just say so. There is no stand-in. > tools exist to map "Design-by-Contract" constructs to "Verified Design-by-Contract" constructs. Right, I hinted at this in my previous comment. SPARK Ada does this. In that case, correctness properties of the program are indeed formally proven. That's a quite different methodology to design-by-contract with runtime checking though, to the point that it almost seems unhelpful to refer to them both by the same name. I've had to be careful to explicitly state design-by-contract using runtime checking this whole time. The deeper distinction here is between testing and formal proof, and design-by-contract can in principle refer to either. > here is a case study Design by contract formal verification for automotive embedded software robustness Have only skim-read but seems somewhat similar to this case-study about SPARK: https://www.adacore.com/tokeneer https://www.adacore.com/tokeneer

rramadass 1y ago

It depends; the "proving" can be done at a gross high level function or fine grained at statement level. Thus in the former case one could use Meyer's Design-by-Contract (aka DbC) while in the latter case one might choose to follow a detailed Dijkstra methodology. For both of the above you don't need any special tools (eg. Z/VDM/TLA+/Coq/Lean etc.) but merely the knowledge to learn to think about a Program using Mathematical Concepts. For most "ordinary" software, DbC would be enough while for critical software one might want to go with the whole nine yards using chosen methodologies/tools. Note that usage of the methodologies/tools themselves require a knowledge of the above-mentioned Mathematics. The point was that a knowledge of the requisite Mathematics gives you a very powerful way of viewing Programs and then you get to choose how to map/implement it using any number of tools and based on the needs of the software.

MaxBarraclough 1y ago
Design-by-contract typically refers to runtime checking of invariants, which is not the equivalent of formal verification. It should not be referred to as proving correctness. It doesn't do so. If you want to prove your program's correctness, that's the domain of formal methods, essentially by definition.
- rramadass 1y ago
  This argument has been made before and that is why i said it depends and put "proving" within quotes. It is a very narrow and wrong way of looking at Formal Methods (both Specification and Verification) and one of the main reasons the "ordinary" software engineer gets intimidated and overawed by formal methods and afraid to even approach the subject (as my comments to user cubefox shows). A Formal Method defined broadly is the application of Mathematical Concepts/Models and Logic to the specification/implementation/verification of Computer Programs. DbC is based on Hoare Logic where you try to "prove" the program intellectually and not necessarily tool driven. This was somewhat mechanized (though still a intellectual pursuit) by Dijkstra's technique of deriving weakest-preconditions. Because the whole process can be quite tedious, laborious and rather complex, automatic theorem prover tools were invented to do the job for you. This has resulted in the unfortunate status quo where Formal Specification/Verification have become identified with the use of tools and not the Mathematics behind them. Proving Correctness need not be fine-grained and absolute but can be good enough done partially at a gross level at specific stages in a program as needed and done either by hand and/or using tools. DbC can be considered a lightweight Formal Method with aspects of both Specification and Verification included. The Programmer plays the role of "theorem prover" when using DbC. However tools exist to map "Design-by-Contract" constructs to "Verified Design-by-Contract" constructs. See for example https://www.eschertech.com/products/verified_dbc.php https://www.eschertech.com/products/verified_dbc.php. Also Eiffel (quintessential DbC language) can be converted using AutoProof to a form which can be proven by Boogie verifier. Finally; here is a case study Design by contract formal verification for automotive embedded software robustness (abstract & pdf) - https://hal.sorbonne-universite.fr/ERTS2024/hal-05028176v1 https://hal.sorbonne-universite.fr/ERTS2024/hal-05028176v1
  - MaxBarraclough 1y ago
    > that is why i said it depends and put "proving" within quotes I feel I need to insist on this point: a design-by-contract methodology using runtime checking may be an effective means of improving software quality, but it certainly isn't proving the correctness of a program. Using the word 'prove' here is just plain wrong. Putting it in quotation marks doesn't help. It simply does not constitute a proof. > It is a very narrow and wrong way of looking at Formal Methods (both Specification and Verification) and one of the main reasons the "ordinary" software engineer gets intimidated and overawed by formal methods and afraid to even approach the subject I'm not insisting on a narrow understanding of formal methods, I'm insisting on proper use of established terminology. I'm all for practical methodologies that benefit software quality without paying the enormous costs of fully applying formal methods. Design-by-contract with runtime checking seems like a reasonable approach. (Static typing is another. Effect-oriented programming might be another.) My point was just about the proper use of the word proof. > Proving Correctness need not be fine-grained and absolute but can be good enough done partially at a gross level at specific stages in a program as needed and done either by hand and/or using tools. A program is proven correct only when the proof is absolute, which implies fine-grained. I'm not opposed to the use of partial proofs or 'good enough' proof-sketches, both of which could be useful in producing high-quality software in the real world, but we should be clear in how we refer to them. I'm not sure about the idea of proving correctness by hand, though. Manually applying a formal model of a real programming language sounds unworkable. If code is well structured, it should be possible for the programmer to reason about it somewhat precisely, like a proof-sketch, but that's not a proof of correctness. > The Programmer plays the role of "theorem prover" when using DbC I don't find this convincing. There's nothing stopping the programmer from failing to notice some error. If you aren't actually doing a proof, just say so. There is no stand-in. > tools exist to map "Design-by-Contract" constructs to "Verified Design-by-Contract" constructs. Right, I hinted at this in my previous comment. SPARK Ada does this. In that case, correctness properties of the program are indeed formally proven. That's a quite different methodology to design-by-contract with runtime checking though, to the point that it almost seems unhelpful to refer to them both by the same name. I've had to be careful to explicitly state design-by-contract using runtime checking this whole time. The deeper distinction here is between testing and formal proof, and design-by-contract can in principle refer to either. > here is a case study Design by contract formal verification for automotive embedded software robustness Have only skim-read but seems somewhat similar to this case-study about SPARK: https://www.adacore.com/tokeneer https://www.adacore.com/tokeneer