Mathematical Theory of Computation

1991-08

This project was concerned with the development of correct and reusable software through the use of higher order abstractions (function, control, assignment, process) and reflection. A semantic framework for these notions will be the basis of an experimental system for manipulating and reasoning about programs. The goals of this project were the development of logical formalisms for reasoning about programs that use abstractions and reflection, and the application of these theoretical results to selected software problems. Example applications include (1) clarification of existing programming paradigms, (2) analysis of existing and proposed languages used in the DARPA community for specifying, writing, and transforming programs, and (3) development and implementation of tools for computer aided reasoning about and operating on programs. The accomplishments of this project fit into four categories: (1) logics for reasoning about function and control abstractions; (2) logics for reasoning about data mutation; (3) logics for reasoning about function and control abstractions in the presence of mutable data; and (4) applying methodology for reasoning about programs to the mechanical verification of hardware.

Computer Programming and Software; COMPUTER PROGRAMS; COMPUTATIONS; COMPUTER AIDED DESIGN; VERIFICATION; MODELS; REUSABLE EQUIPMENT; THEORY; COMPUTER PROGRAMMING; MUTATIONS; MATHEMATICS; LOGIC; MECHANICAL PROPERTIES; REASONING; SOFTWARE ENGINEERING; REUSABLE EQUIPMENT.; Text

Open access content. Open access content
Approved for public release; distribution is unlimited.

text/html
English

DTICE ADA239419
832036436

From OAIster®, provided by the OCLC Cooperative.

edsoai.ocn832036436