ASE2 CARD CATALOG ENTRY
This report describes the results of an exercise in formal program verification conducted at ORA. In this exercise, we started with code written by students at Syracuse University as part of work conducted by Professor Amrit Goel on program development methods. The code was an implementation of the routines of the Launch Interceptor Program (LIP), a specification of a protocol for launching an interceptor missile.
The exercise consisted of specifying the routines using the asymptotic method and verifying a number of them using Penelope. The asymptotic method is a relatively simple approach to specification and verification of numerical programs that takes account of numerical error without quantifying it. It is important to take account of numerical error, even if it is small, because even a small error can change the result of a numerical program if it is a discontinuous function of the input. All non-constant discrete-valued (integer or Boolean) functions of real number arguments are discontinuous, and many real-valued functions appearing in geometry are discontinuous at certain degenerate configurations. When a specification, like the LIP specification, does not say anything quantitative about permissible error, the asymptotic method is the appropriate way to formalize that specification. The asymptotic method exposes problems of this kind, without requiring any more work than is necessary for that purpose. Classical error analysis will expose similar problems and give quantitative measures of how bad they are, but also requires more effort and expertise.
This verification exercise had the following results.
STARS-AC-A023/006/00 1 June 94 Initial release to the PAL
Approved for public release; Distribution unlimited
This documentation is provided "AS IS" and without any expressed or implied warranties whatsoever. No warranties as to performance, merchantability, or fitness for a particular purpose exist. The user must assume the entire risk and liability of using this document. In no event shall any person or organization of people be held responsible for any direct, indirect, consequential or inconsequential damages or lost profits.
Powered by the Generic Web-Based Reuse Library (GWRL)