What every C Programmer should know about undefined behavior #2/3
What every C Programmer should know about undefined behavior #2/3
Posted May 16, 2011 22:17 UTC (Mon) by HelloWorld (guest, #56129)In reply to: What every C Programmer should know about undefined behavior #2/3 by cmccabe
Parent article: What every C Programmer should know about undefined behavior #2/3
> Similarly, if you try to prove that your browser will successfully display a web page, you slam head-on into a mountain of difficulties.
Of course it's not currently feasible to prove the correctness of a complex program like a web browser, already because there is no formal mathematical specification for how HTML documents should be rendered. But it'd already be a success if certain properties of a program could be proven automatically. Properties such as "every file descriptor opened is also closed at some point" or "every array index is within the bounds of the array".
Of course it's not currently feasible to prove the correctness of a complex program like a web browser, already because there is no formal mathematical specification for how HTML documents should be rendered. But it'd already be a success if certain properties of a program could be proven automatically. Properties such as "every file descriptor opened is also closed at some point" or "every array index is within the bounds of the array".
> What if the RAM is bad? How about the hard disk?
Bad RAM is not a software bug, thus it's out of scope for software developers. It's like saying that you can't prove anything in math because your axiom or logic may be "broken". You just have to assume something. In Peano numerals, it's the existence of the number 0, and if you want to prove stuff about programs, you have to assume that the machine you run it on works.