Accession Number : ADA274966

Title :   Deductive Computer Programming.

Descriptive Note : Final technical rept. 1 Nov 89-31 Dec 92,

Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Manna, Zohar

Report Date : 23 MAR 1993

Pagination or Media Count : 14

Abstract : Research has been conducted on the following related topics: Automated Deduction - new inference rules have been developed to facilitate reasoning about ordering relations, which pervade all software-development applications. Program Synthesis - a deductive approach to program synthesis has been developed, cased on the application of theorem-providing techniques, Auto Planning the deductive Tableau system, extended to situational logic, has been applied to the formation of robotic and engineering plans, Temporal Logic - research into the foundational questions of temporal logic has yielded several techniques for reasoning about temporal concepts, Reactive Systems - a methodology based on temporal based logic was developed for the specification and verification of reactive systems, i.e., system whose role is to maintain an ongoing interaction with their environment. Real-Time System - the temporal methodology ha s been extended to deal with real-time systems by introducing a time parameter into the state and Hybrid Systems - the temporal methodology, the specification language, and the proof system have been extended to deal with hybrid systems

Descriptors :   *COMPUTER PROGRAMMING, REASONING, HYBRID SYSTEMS, REAL TIME, COMPUTER LOGIC, ROBOTICS.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE