"break" statements (Really Re computer science)
Antony Williams
asw at rlvd.UUCP
Fri Nov 8 04:35:06 AEST 1985
In article <402 at graffiti.UUCP> peter at graffiti.UUCP (Peter da Silva) writes:
>Generally because it's not practical to prove code correct in large
>scale applications.
I think what you really mean is that it is not YET practical to prove
large scale applications wholly correct. It is certainly practical to prove
correctness for smallish modules, and this is extremely beneficial:
it means that you should look elsewhere for the bug, even if the symptom
occurs in the verified module. The total program remains unproved, as the
verification relies on the assumption that the module has not been interfered
with by some other part of the program. The ubiquity of this phenomenon in
C programs does not imply that formal verification has no benefit.
> In fact it's hard to apply many computer science
^^^^^^^^^^^^^^^^
>techniques in large scale applications. This is extremely unfortunate,
^^^^^^^^^^
I tend to think of things like searching techniques as computer science
techniques because one expects computer science graduates to have learned
about them. You must have a different idea, or else I feel sorry for those
who use/support/pay for your code :-)
--
---------------------------------------------------------------------------
Tony Williams |Informatics Division
UK JANET: asw at uk.ac.rl.vd |Rutherford Appleton Lab
Usenet: {... | mcvax}!ukc!rlvd!asw |Chilton, Didcot
ARPAnet: asw%rl.vd at ucl-cs.arpa |Oxon OX11 0QX, UK
More information about the Comp.lang.c
mailing list