DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click
HERE to register or log in.
Accession Number:
ADA188791
Title:
Building Software Systems Economically with Mechanized Logic: Initial Design Proposal
Descriptive Note:
Final rept.
Corporate Author:
TEXAS UNIV AT AUSTIN INST FOR COMPUTING SCIENCE AND COMPUTER APPLICATIONS
Report Date:
1987-06-30
Pagination or Media Count:
15.0
Abstract:
Our goal is to develop an economical technology for building proved computing systems with mechanized formal logic. The unifying element of this technology is the functional language Rose which we are designing. Rose embodies a powerful formal logic, and it also is an executable, functional programming language. Thus, potentially, Rose provides a single, unified formalism that can express both hardware and software systems and their specifications and requirements. In the long term, with the development of parallel architectures and optimizing compilers that exploit theorem providing, we believe that functional programming languages will be useful across a wide variety of tasks. In the intermediate term, we intend that Rose be convenient for software applications such as encryption boxes, flow modulators, message servers, etc. The purpose of this phase of our work is to mechanize the Rose logic so that it can be used extensively and economically in all of the previous kinds of activities. We will do this by increasing the power of current Boyer-Moore logic and its theorem prover, by defining the Rose language which embodies the expanded logic and presents it in a more conventional and familiar notation, and by implementing a life-cycle support system for Rose that supports the development and maintenance of large collections of Rose functions, theorems, and proofs.
Distribution Statement:
APPROVED FOR PUBLIC RELEASE
