THE PRINCIPAL TECHNICAL OBJECTIVE IN THIS PROJECT IS TO SHOWTHE FEASIBILITY OF BUILDING TOOLS TO SUPPORT THE FORMAL VERIFICATION OF MATHEMATICAL SOFTWARE.

THE PRINCIPAL TECHNICAL OBJECTIVE IN THIS PROJECT IS TO SHOWTHE FEASIBILITY OF BUILDING TOOLS TO SUPPORT THE FORMAL VERIFICATION OF MATHEMATICAL SOFTWARE. NO EXISTING VERIFICATION ENVIRONMENT SUPPORTS PROOF OF CORRECTNESS OF PROGRAMS EXECUTING OVER THE DATA STRUCTURE OF THE REAL NUMBER SYSTEM. THERE ARE ALSO VERY FEW INFORMAL COREECTNESS PROOFS OR EVEN THEORETICAL WORK IN THIS AREA. THIS APPROACH IS MULT-TASKED. IT EXAMINES PROOFS OVER THE ABSTRACT MATHEMATICAL REAL NUMBERS AND CLASSIFIES SOFTWARE AS TO THE AMOUNT OF KNOWLEDGE OF THE THEORY OF THE REAL NUMBERS NECESSARY FOR CORRECTNESS PROOFS. THIS STUDY IS PARTICULARLY INTERESTED IN FRAGMENTS OF ANLYSIS WHICH HAVE FAST LOGICAL DECISION PROCEDURES. IT THEN DEVELOPS MODELS AXIOMS FOR THE MACHINE REPRESENTABLE REAL NUMBERS. THE AXIOMS ARE REFLECTIVE OF THE PHENOMENA OF ROUNDOFF, UNDERFLOW AND OVERFLOW. THEN BEGINS THE STUDY OF PROOFS OF CORRECTNESS OF PROGRAMS WITH RESPECT TO THESE NEW AND MORE REALISTIC AXIOMS. IN ADDITION WE BEGIN THE DEVELOPMENT OF A METHODOLOGY BASED ON INCREMENTAL CONCSTRUCTION OF PROGRAMS AND ATTACHED ASSERTIONS. SUCH AN APPROACH, IF SUCCESSFUL, ERASES THE BURDEN ON A NON-EXPERT USER.