On Jan 27, 5:03 pm, Paddy > If static typing is optional then a program written in a dynamic > language that passes such an automated static analysis of source code > would have to be a simple program written in a simplistic way, and > also in a static style.
Yes, but for safety-critical software you usually want the simplest possible solution. The last think you want is an unnecessarily "fancy" design. Unless there is a darn good reason to write a "non-static" program, you just don't do it. You might want to check into what the FAA allows in "flight-critical" code, for example. I am certainly not an expert in that area, but I've had a passing exposure to it. My understanding is that every possible branch of the code must be fully and meticulously analyzed and verified. Hence, the dynamic dispatching of ordinary object-oriented code is either prohibited or severely frowned upon. > Having used such formal tools on hardware designs that are expressed > using statically typed languages such as Verilog and VHDL, we don't > have the problem of throwing away run time typing, but we do get other > capacity problems with formal proofs that mean only parts of a design > can be formally prooved, or we can proof that an assertion holds only > as far as the engine has resources to expand the assertion. > We tend to find a lot of bugs in near complete designs by the random > generation of test cases and the automatic checking of results. In > effect, two (or more) programs are created by different people and > usually in different languages. One is written in say Verilog and can > be used to create a chip, another is written by the Verification group > in a 'higher level language' (in terms of chip testing), a tunable > randomized test generator then generates plausible test streams that > the Verification model validates. The test stream is applied to the > Verilog model and the Verilogs responses checked against the > Verification models output and any discrepancy flagged. Coverage > metrics (line coverage , statement coverage, expression coverage ...), > are gathered to indicate how well the design/program is being > exercised. > > I would rather advocate such random test generation methods as being > more appropriate for testing software in safety critical systems when > the programming language is dynamic. Random test generation methods can go a long way, and they certainly have their place, but I don't think they are a panacea. Coming up with a random set of cases that flush out every possible bug is usually very difficult if not impossible. That was the point of the quote in my original post. -- http://mail.python.org/mailman/listinfo/python-list
