eli@spdcc.COM (Steve Elias) (08/21/89)
cyrus@hpmcaa.mcm.hp.com (Judy Cyrus) writes: > >The document you are looking for is the UK Ministry of Defense Standard >MoD-Std-0055. >It requires the use of formal methods and mathematical >verification on all safety-critical software. It bans the use of >assembly language, limits high-level languages like Ada to "safe" subsets, bans concurrent processes, interrupts (except for fixed interval timer), >floating-point arithmetic, and recursion. these requirements sound awfully restrictive. do you agree that the requirements for high speed realtime operation defy mathematical verification? a 60 line subroutine can require 6000 pages of proof, if a proof can be obtained. high speed operation can require assembler level code, or microcoding. one reference on the subject of formal methods and programming is: David Gries, _The Science of Programming_. -- ... Steve Elias (eli@spdcc.com);6178906844;6178591389; {} /* */