Re: Cocoa newbie frustration
Re: Cocoa newbie frustration
- Subject: Re: Cocoa newbie frustration
- From: "Erik M. Buck" <email@hidden>
- Date: Mon, 8 Oct 2001 15:22:50 -0500
>
Erik,
>
>
>>>>>> Erik M. Buck (EMB) wrote at Mon, 8 Oct 2001 13:45:03 -0500:
>
EMB> ...It is sometimes necessary to PROVE that a solution is correct
>
EMB> in all cases...
>
>
IIRC my theoretical cybernetics, that is quite impossible even in theory
and
>
with a plain Turing Machine. Therefore, I doubt whether C++ or Ada or Logo
>
;))) or any other language would really help ;)
>
---
It is not impossible. It is merely very hard as long as the application is
constrained appropriately. Software is "verified" all of the time for use
in avionics. Even the CPU's microcode is verified. Only deterministic
parts of the CPU are used. In some cases, this may prevent use of Cache and
may forbid branch prediction. Special electronics are used to assure that a
CPU has achieved a deterministic state at some fixed time interval after
power is applied. Power is conditioned and monitored. Every possible path
through the software is executed and verified. Every possible data value is
validated in combination with every possible path through the code. Math
proofs are sometimes used. The object code is compared to the source code
to assure that compilers have not introduced errors. Applications can not
contain any code that is never called. There is a long list of rules. The
FAA requires "certification" which requires avionics makers to "prove" that
the software is correct.
It is also possible to use statistical methods to almost prove correctness.
The standard for avionics is one error in 10 to the 9th calculations and
that is only allowed if there is a way to detect an error. In order to
detect errors, it is common to use two or more different CPU types (so that
CPU peculiarities can not mask problems) and two different software
applications written to the same specification by different teams. If the
two different systems fail to calculate the same value, an error has
occurred.
Airplanes do not crash due to software errors, but they may crash due to
specification errors.