Timeline for How can developers be assured that their software is fault free?
Current License: CC BY-SA 3.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 23, 2017 at 12:41 | history | edited | CommunityBot |
replaced http://stackoverflow.com/ with https://stackoverflow.com/
|
|
| Mar 21, 2016 at 10:03 | comment | added | Graham | @otakucode I only half agree with you on that, because there are good standards for life-critical systems, and environments where systems are life-critical include adherence to those standards (and auditing to demonstrate adherence to those standards) as a prerequisite for projects. Or in off-the-shelf products, failing to follow those standards is a case for punitive damages. If they followed all the right procedures though and something still slipped through, that's kind of tolerated with complex engineering, in the same way as all the retrofitted fixes that happen to any new car. | |
| Mar 20, 2016 at 4:31 | comment | added | otakucode | @Graham - Unfortunately the majority of people who work in software also do not understand that it is engineering. Nor do the courts, who should be levying the same kinds of decisions for negligence as they do in civil engineering. Software engineering is the only field I know where you can build life-critical systems with inexperienced people, denying them adequate tools, avoiding sensible well-known practices, and doing anything to cut cost and accelerate schedules in defiance of any concerned engineers, and the courts will just look the other way. | |
| Mar 19, 2016 at 16:32 | comment | added | Polygnome | I just need to use the collatz function and you can not longer prove that it even terminates. | |
| Mar 18, 2016 at 16:52 | comment | added | Noah Sussman | @PeterMasiar the computers Dijkstra was working with were many orders of magnitude less complex than the systems that exist today. Of course you can trivially prove a program correct if it's small enough and if its specification is small enough. But there is no general way to prove that any program is correct, again because there is no general way to prove that the specification is correct. Not that I'm calling Dijkstra's work trivial, but what was exciting to awards committees 40 years ago doesn't have any relevance to modern software engineering. | |
| Mar 18, 2016 at 9:28 | comment | added | Graham | @PeterMasiar Why do you think it matters what the physical representation is? Civil engineering happens at the logic stage without material representation. By the time someone's laying bricks, it's too late to change it. Civil engineering accepts that sometimes metal fatigues, bolts are badly made, panels don't quite fit, etc., and applies sensible tolerances so that the project still works. Software engineering does the same - see MISRA, DO178-B, and all the other similar standards. And when bridges are actually built, yes, it's not unknown for them to have bugs in the design. | |
| Mar 17, 2016 at 21:10 | comment | added | Noah Sussman | While you can use formal verification to prove that the program conforms to the specification, you cannot prove by any formal method that the specification does not contain any errors. You can prove conformance but you cannot prove correctness. | |
| Mar 17, 2016 at 15:18 | comment | added | Peter M. - stands for Monica | @Peteris - Did you had experience in college to prove program? Possibly using a language optimized for that? I did, and it changed my understanding of programming. I do agree with you that is is lot of work, but I disagree that it is not possible, because I did it. | |
| Mar 17, 2016 at 15:14 | comment | added | Peter M. - stands for Monica | @Graham - Bridge is made out of matter, bricks or steel. Program is made out of logic, has no material representations. And while you may think that Dijkstra is ivory-tower academician with no idea of the real world, Turing prize commission disagree with you. Did you bothered to follows links in my answer? And let me tell you that i do work in software for few decades now. | |
| Mar 17, 2016 at 10:51 | comment | added | Graham | A civil engineer can't prove that his bridge won't fall down either - all he can show is that it passes tests for a range of scenarios. Failing to grasp that software engineering is engineering, and applying the same standards to it, is a common failure amongst people who don't themselves work in software. Yes, there's a body of work on formal proof - and it is a classic example of ivory-tower academics losing track of the real world to produce a lovely theory which is unuseable in practise. | |
| Mar 17, 2016 at 10:08 | comment | added | Peteris | If your requirements are detailed enough to allow deriving final code, then the form of those requirements is essentially just a high-level programming language. For a nontrivial system, the size and complexity of any somewhat detailed requirements will be huge, comparable to the resulting codebase, and the process of developing it is as bug-prone as developing normal code. | |
| Mar 16, 2016 at 22:23 | comment | added | Peter M. - stands for Monica | If you have bug in requirement, you "just" fix that, and then "just" derive bug-free code from fixed requirements. :-) | |
| Mar 16, 2016 at 22:22 | comment | added | Mark | "Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth | |
| Mar 16, 2016 at 20:17 | comment | added | Peteris | Formal program verification and proving properties can only verify that a program matches some particular formal requirements. This doesn't in any way ensure that this program is bug free, as a large class of real world bugs is program behavior that does exactly match the specified requirements, but in some particular situation these requirements don't match the actual business needs or user expectation - thus the system is buggy, broken and needs to be fixed despite theoretically being "correct". In essence, you simply go from worrying about bugs in code to bugs in the formal requirements. | |
| Mar 16, 2016 at 19:19 | history | answered | Peter M. - stands for Monica | CC BY-SA 3.0 |