| Text Generation: The State of the Art and the Literature |
DEC 1981 |
|
| Authors:
William C. Mann; Madeline Bates; Barbara J. Grosz; David D. McDonald; Kathleen R. McKeown; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
 | This report consists of two documents describing the state of the art of computer generation of natural language text. Both were prepared by a panel of individuals who are active in research on text generation. The first document assesses the state of the art, identifying four kinds of technical developments which will shape the art in the coming decade: linguistically justified grammars, knowledge representation methods, models of the reader, and ... |
|
| DARPA Internet Program. Internet and Transmission Control Specifications |
SEP 1981 |
|
| Authors:
Jonathan B. Postel; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| These protocols are designed for use in an interconnected system of packet switched networks. The Internet Protocol is a basic universal protocol, and provides a uniform address space, as well as the mechanism for routing datagrams through the connected set of networks and for the fragmentation and reassembly of long datagrams if necessary for transmission through small packet networks. The Transmission Control Protocol is designed to be a highly reliable ... |
|
| Transmission Control Protocol, DARPA Internet Program Protocol Specification |
SEP 1981 |
88 pages |
| Authors:
UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
 | The Transmission Control Protocol (TCP) is intended for use as a highly reliable host-to-host protocol between hosts in packet-switched computer communication networks, and in interconnected systems of such networks. This document describes the functions to be performed by the Transmission Control Protocol, the program that implements it, and its interface to programs or users that require its services. (Author) |
|
| Internet Protocol, DARPA Internet Program Protocol Specification |
SEP 1981 |
|
| Authors:
UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| The Internet Protocol is designed for use in interconnected systems of packet-switched computer communication networks. Such a system has been called a catenet 1. The internet protocol provides for transmitting blocks of data called datagrams from sources to destinations, where sources and destinations are hosts identified by fixed length addresses. The internet protocol also provides for fragmentation and reassembly of long datagrams, if necessary, for transmission through small packet networks. ... |
|
| Internet Protocol. DARPA Internet Program Protocol Specification |
SEP 1981 |
|
| Authors:
UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
|
| Internet Protocol. DARPA Internet Program Protocol Specification |
SEP 1981 |
|
| Authors:
UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This memo describes the relationship between the Internet Protocol (IP) 1 Type of Service and the service parameters of specific networks; including AUTODIN II, ARPANET, PRNET and SATNET. (Author) |
|
| A Research Program in Computer Technology, Volume 2 |
AUG 1981 |
25 pages |
| Authors:
Keith W. Uncapher; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This report summarizes the research performed by USC/Information Sciences Institute from December 1, 1979, to September 30, 1980, for the Defense Advanced Research Projects Agency under contract MDA903-80-C-0523. The ISI program covered by this contract consisted of three research areas: VLSI development of a low-cost, fast turnaround LSI/VLSI device fabrication service to support VLSI research, and research on the VLSI design problem; Strategic C3 System Experiment Support - development of ... |
|
| A Research Program in Computer Technology. Volume 1 |
AUG 1981 |
148 pages |
| Authors:
Keith W. Uncapher; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This report summarizes the research performed by USC/Information Sciences Institute from October 1, 1979, to September 30, 1980, for the Defense Advanced Research Projects Agency. The research applies computer science and technology to areas of high DoD/military impact. The ISI program consists of fourteen research areas: Specification Acquisition From Experts study of acquiring and using program knowledge for making informal program specifications more precise; Program Verification - logical proof of ... |
|
| Design Specification Validation |
JUN 1981 |
|
| Authors:
Robert M. Blazer; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This report documents research concerning the feasibility of validating formal software specification. The one year effort attempted to show that with a suitable formal software specification language, specifications could be validated in the same manner as computer designs are currently tested. |
|
| Transformational Implementation: An Example |
MAY 1981 |
|
| Authors:
Robert Balzer; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| Program Manipulation Systems have been proposed as an alternative programming paradigm in which the PROCESSES of design and implementation are themselves the subject of study. These processes are captured and recorded to provide documentation of the program, the basis for its validation, and the framework within which future maintenance will occur. This extension of the conventional programming paradigm to include the development of the program as a computer processable object ... |
|
| Formal Specification and Verification of a Connection-Establishment Protocol |
APR 1981 |
|
| Authors:
Daniel Schwabe; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| A specification language named SPEX, tailored to the needs of communications protocols, is proposed, and its relation to a semi-automated verification system, Affirm, is discussed. This language is then used to specify a connection protocol currently being used. Certain errors are uncovered by analysis using the verification system. However, the major portion of the protocol's operation is shown to be correct. (Author) |
|
| Specification and Verification of Communication Protocols in AFFIRM Using State Transition Models. |
MAR 1981 |
|
| Authors:
David H. Thompson; Carl A. Sunshine; Roddy W. Erickson; Susan L. Gerhart; Daniel Schwabe; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| It is becoming increasingly important that communication protocols be formally specified and verified. This report describes a particular approach--the state transition model--using a collection of mechanically supported specification nd verification tools incorporated in a running system called Affirm. Although developed for the specification of abstract data types and the verification of their properties, the formalism embodied in Affirm can also express the concepts underlying state transition machines. Such models easily ... |
|
| Formal Modeling of Communication Protocols. |
MAR 1981 |
|
| Authors:
Carl A. Sunshine; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| Interest in more rigorous definition and analysis of communication protocols is increasing. This report surveys the current state of the art in protocol specifications and verification. Methods for specification such as abstract machines, Petri nets, formal languages, abstract data types, and programs are described and compared. Verification methods including state exploration, symbolic execution, structural induction, and program proof are discussed. Work is progressing rapidly in many of these areas, and ... |
|
| A Database Foundation for Process Specifications. |
OCT 1980 |
|
| Authors:
Neil M. Goldman; David S. Wile; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| A language suitable for system specification should allow a specification to be based on a cognitive model of the process being described. In part, such a language can be obtained by properly combining certain conceptual abstractions of data models with reference and control concepts designed for programming languages. Augmenting the resulting language with formal versions of several natural language constructs further decreases the cognitive distance between specifications of large systems ... |
|
| Graphics Language (Version 2.1). |
JUL 1980 |
|
| Authors:
Richard Bisbey II; Dennis Hollingworth; Benjamin Britt; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This document defines the language interface to Version 2.1 of a device-independent graphics system intended to facilitate the use of graphics in the command and control environment. The system homogeneously supports graphics terminals of widely varying capability, configured with one or more different program running on separate computers connected via a C2 communications network. These include both calligraphic and bit-map displays as well as plotters. The set of graphics primitives ... |
|
| A Distributable, Display-Device-Independent Vector Graphics System for Command and Control. |
JUL 1980 |
42 pages |
| Authors:
Richard Bisbey II; Dennis Hollingworth; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This report documents a distributable, device-independent vector graphics system developed by ISI for the Defense Advanced Research Projects Agency. It describes the system architecture, communications elements, and a phased implementation strategy. The system supports graphics-based command and control applications in distributed computational environments such as the ARPANET. The system has been in use at ISI and at the Naval Ocean Systems Center (NOSC) in the Advanced Command and Control Architectural ... |
|
| Microcode Verification Project. |
MAY 1980 |
|
| Authors:
Stephen D. Crocker; Leo Marcus; Dono van-Mierop; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| Within the scope of this project, a formalism for representing state transitions in a computationally tractable way has been invented, and a proof system based on this formalism has been designed and implemented. The representations of state transitions are called 'state deltas'. The basic proof system has been specialized for proofs about machine language and microcode by the addition of simplification rules for bitstring arithmetic, and by the addition of ... |
|
| Toward a Speech Act Theory for Natural Language Processing. |
MAR 1980 |
|
| Authors:
William C. Mann; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| THIS REPORT EXPLORES THE PROSPECTS FOR USING CONCEPTS FROM Speech Act Theory in the design of processes that operate on natural language. The potential benefits of creating processes to identify the illocutionary force of utterances in text are particularly significant. These benefits include systematic derivation of implicit communication, identification of relations between text and prior text, and the possibility of applying existing action-oriented knowledge within Al to new natural language ... |
|
| DoD Standard Transmission Control Protocol, |
JAN 1980 |
|
| Authors:
Jon Postel; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| The Transmission Control Protocol (TCP) is intended for use as a highly reliable host-to-host protocol between hosts in packet-switched computer communication networks, and especially in interconnected systems of such networks. This document describes the functions to be performed by the Transmission Control Protocol, the program that implements it, and its interface to programs or users that require its services. Computer communication systems are playing an increasingly important role in military, ... |
|
| Microcode Verification Project. |
JAN 1980 |
|
| Authors:
Stephen D. Crocker; Leo Marcus; Dono van-Mierop; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| The goal of the microcode verification project at ISI is the development of both the theory and tools for verification of microcode. The strategy has been to push the development of a working system, letting the theoretical issues and the human engineering questions emerge during system development. The ISPS language is used for encoding our machine descriptions. The State Delta formalism is used for reasoning about the course of the ... |
|
| Computer as Author -- Results and Prospects. |
JAN 1980 |
|
| Authors:
William C. Mann; James A. Moore; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| For a computer program to be able to compose text is interesting both intellectually and practically. Artificial Intelligence research has only recently begun to address the task of creating coherent texts containing more than one sentence. One recent research has produced a new paradigm for organizing and expressing information in text. This paradigm, called Fragment-and-Compose, has been used in a pilot project to create texts from semantic nets. The method ... |
|
| DoD Standard Internet Protocol, |
JAN 1980 |
|
| Authors:
Jon Postel; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| The Internet Protocol is designed for use in interconnected systems of packet-switched computer communication networks. Such as system has been called a 'catenet'. The internet protocol provides for transmitting blocks of data called datagrams from sources to destinations, where sources and destinations are hosts identified by fixed length addresses. The internet protocol also provides for fragmentation and reassembly of long datagrams, if necessary, for transmission through 'small packet' networks. This ... |
|
| A Formal Definition of AMDL. |
OCT 1979 |
|
| Authors:
Peter W. Alfvin; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| Since the introduction of ISP, the use of hardware description languages (HDLs) has increased dramatically. Used originally to describe at the programming level the instruction sets of digital computers, hardware descriptions are now being used in applications such as design automation, emulation, compiler generation, and program verification - to name only a few. This surge of activity has put the existing HDLs to the thorough test, with each application area ... |
|
| Dialogue Games. |
OCT 1979 |
|
| Authors:
William C. Mann; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| Natural dialogue does not proceed haphazardly; it has an easily recognized 'episodic' structure and coherence that conform to a well developed set of conventions. This report represents these conventions formally in terms related to speech act theory and to a theory of action. The major formal unit, the Dialogue Game, specifies aspects of the communication of both participants in a dialogue. We define the formal notion of Dialogue Games and ... |
|
| SIGMA Message Service: Reference Manual. Version 2.3. |
JUN 1979 |
|
| Authors:
Jeff Rothenberg; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| The SIGMA Message Service is an automated message processing service provided for a test of automated military message processing. Through the service, procedures that are presently both manual and semi-automated are completely automated; these include everything from message composition through message receipt. The SIGMA Message Service allows work on four kinds of objects: messages, files of messages, text times, and selectors. Each of the four types is explained, and instructions ... |
|
| An Experiment in Distributed Interpretation. |
MAY 1979 |
|
| Authors:
Victor R. Lesser; Lee D. Erman; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| The range of application areas to which distributed processing has been applied is limited. In order to extend this range, new models for organizing distributed systems must be developed. We present a new model, in which the distributed system is able to function effectively even though processing nodes have inconsistent and incomplete views of the data bases necessary for their computations. This model differs from conventional approaches in its emphasis ... |
|
| The Joy of TENEX and TOPS-20. Part One. |
MAR 1979 |
|
| Authors:
Chloe Holg; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This is a basic manual discussing the operation of the ARPANET, the TENEX and TOPS-20 operating systems, and the following mail handling programs: SNDMSG, MSG, Hermes, and MAILSTAT. |
|
| SIGMA Message Service: Reference Manual Version 2.2. |
MAR 1979 |
|
| Authors:
Jeff Rothenberg; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| The SIGMA Message Service is an automated message processing service provided for a test of automated military message processing. Through the service, procedures that are presently both manual and semi-automated are completely automated; these include everything from message composition through message receipt. The SIGMA Message Service allows work on four kinds of objects: messages, files of messages, text items, and selectors. Each of the four types is explained, and instructions ... |
|
| A Research Program in Computer Technology. |
FEB 1979 |
166 pages |
| Authors:
Keith W. Uncapher; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This program is aimed at applying comptuer science and technology to areas of high DoD/military impact. Research areas include: Specification Acquisition from Experts--study of acquiring and using program knowledge for making informal program specifications more precise; Military Message Experiment--development of an experimental user-oriented message service for potential large-scale military use; Program Verification--logical proof of program validity; Network Secure Communication--work on low-bandwidth, secure voice transmission using an asynchronous packet-switched network; Command ... |
|
| The JOY of TENEX and TOPS-20: Part II. |
JAN 1979 |
113 pages |
| Authors:
Chloe Sommers Holg; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This is a basic manual discussing the operation of the ARPANET, the TENEX and TOPS-20 operating systems, and the following programs: XED, TECO, DCOPY, XOFF, RUNFIL, FTP, TELNET, and RSEXEC. (Author) |
|
| A Research Program in Computer Technology |
79 |
190 pages |
| Authors:
K. W. Uncapher; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This report summarizes the research performed by USC/Information Sciences Institute from October 1, 1978, to September 30, 1979. The research applies computer science and technology to areas of high DoD/Military impact. The ISI program consists of twelve research areas: Program Verification; Military Message Experiment; Command and Control Graphics; Specification Acquisition From Experts; Network Secure Communication; Internetwork Concepts; Distributed Sensor Networks; Autopsy; Packet Radio Terminal System Evaluation; MAST; User-Dedicated Resource; and ... |
|
| DSN (Distributed Sensors Networks) Problems -- An Overview, |
DEC 1978 |
|
| Authors:
J. A. Barnett; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This article is concerned with the particular problem of constructing a world picture from sensor data. The world of interest contains craft capable of motion (e.g., airplanes, water vessels, and land forces) and the terrain. The important terrain features are target locations and geographic data that may affect the operation and behavior of sensors and craft. The world picture comprises descriptions of craft behavior and location with respect to the ... |
|
| Distributed Sensors Networks (DSN): An Attempt to Define the Issues, |
DEC 1978 |
|
| Authors:
Y. Yemini; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| It seems appropriate at this early stage of research to take a global view of the DSN problem. This paper presents an initial attempt to obtain this goal; it should be read as a working paper whose main purpose is to trigger responses and focus attention on some of the issues. The method chosen to help define the issues centers on identifying the potential functions of DSN. These issues include ... |
|
| The Positioning Problem - A Draft of an Intermediate Summary |
DEC 1978 |
9 pages |
| Authors:
Yechiam Yemini; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| The positioning problem arises when it is necessary to locate a set of geographically-distributed objects using measurements of the distances between some object pairs. In a Packet Radio Network, for instance, any two network members that can talk to each other may use a simple time-stamping mechanism to measure the distance between them; a distance measurement protocol may then be developed. The problem is whether and how the distance measurements ... |
|
| Mathematical Approach to Computational Networks. |
NOV 1978 |
|
| Authors:
Danny Cohen; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This report deals with design principles for iterative computational networks. Such computational networks are used for performing repetitive computations which typically are not data-dependent. Most of the signal processing algorithms, like FFT and filtering, belong to this class. The main idea in this report is the development of mathematical notation for expressing such designs. This notation captures the important features and properties of these computational networks, and can be used ... |
|
| Process Models of Reference in Context. |
OCT 1978 |
|
| Authors:
James A. Levin; Neil M. Goldman; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| Reference is a central issue for language comprehension and generation. After reviewing existing process models for comprehending and generating referring expressions, we present a general framework for context and reference processing. The context for reference processing is represented as a Public Workspace. Reference processes access Public Workspace and modify its content, which is the set of concepts currently on the table as far as the current language interaction is concerned. ... |
|
| Program Verification in the 1980s: Problems, Perspectives, and Opportunities. |
AUG 1978 |
|
| Authors:
Susan L. Gerhart; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| Properties of programs can be mathematically proved. This report concerns the use of such mathematical proofs as a means of verifying that programs satisfy their specifications and other expectations of proper behavior. Moreover, the theory by means of which programs are proved can be used in the formal reasoning needed to construct and maintain programs. The primary current needs are: (1) expansion of the theory to encompass more aspects of ... |
|
| Multi-Microprocessor Emulation: Annual Report for 1977. |
APR 1978 |
|
| Authors:
Charles Hayden; Peter W. Alfvin; Stephen D. Crocker; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| The goal of the Multi-Microprocessor Emulation (MMPE) project is to develop modeling and emulation techniques for assemblies of microprocessors. An extension to an existing computer description language (ISPS) is proposed for representing the architecture of multi-microprocessor systems, and the results of some preliminary studies on the design of an emulation facility are described. This effort will eventually lead to a high-speed emulation facility based on the QPRIM system. The emulation ... |
|
| Protection Errors in Operating Systems: Serialization. |
APR 1978 |
|
| Authors:
Jim Carlstedt; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This document describes a class of protection errors found in current computer operating systems. It is intended primarily for persons responsible for improving security aspects of existing operating system software. The term 'protection evaluation' here denotes a search for errors based only on static information about a target operating system, primarily program listings but possibly other system documentation as well. These static methods are intended to complement dynamic methods such ... |
|
| SIGMA Message Service Reference Manual. Version 1.75. |
MAR 1978 |
|
| Authors:
Jeff Rothenberg; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| The Sigma message service is an automated message processing service provided for a test of automated military message processing. Through the service, procedures that are presently both manual and semi-automated are completely automated; these include everything from message composition through message receipt. The Sigma message service allows work on four kinds of objects: messages, files of messages, text items, and selectors. Each of the four types is explained, and instructions ... |
|
| HP/MME Terminal: Application Specification. |
MAR 1978 |
|
| Authors:
Don Oestreicher; Paul Raveling; Rob Stotz; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This document describes the black box characteristics of the modified HP2649A terminal that ISI has developed for the Military Message Experiment (HP/MME). The communication interface between the terminal and the host computer is described, both in terms of the syntax and the semantics. The communication line discipline (protocol) is also described. (Author) |
|
| Protection Errors in Operating Systems: A Selected Annotated Bibliography and Index to Terminology. |
MAR 1978 |
48 pages |
| Authors:
Jim Carlstedt; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This report represents the current state of a bibliography on the subject of protection in computer operating systems. 'Current state' means that the bibliography is incomplete; it is a byproduct of a research project in the field of protection, recently completed. The bibliography is being published in the belief that it may be useful as is, and that it might serve as the basis of a continuing effort to collect, ... |
|
| PRIM System: Tool Builders Manual and User Reference Manual. |
JAN 1978 |
|
| Authors:
Louis Gallenson; Alvin Cooperband; Joel Goldberg; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| PRIM is an interactive microprogrammable environment used for creating and running emulators of existing or newly specified computers, with major emphasis on debugging tools that can be operated by the user in the language of the original system. This document serves as a manual for programmers interested in writing emulation tools to run under PRIM. It covers an overview of the PRIM system design, requirements for emulators that are to ... |
|
| A System for Incrementally Designing and Verifying Programs. Volume II. |
JAN 1978 |
|
| Authors:
Mark S. Moriconi; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This appendix contains a transcript of a session with SID in which a simple message switching network that allows secure, asynchronous message transfer among a fixed number of users is incrementally developed. (Author) |
|
| A System for Incrementally Designing and Verifying Programs, Volume I. |
JAN 1978 |
|
| Authors:
Mark S. Moriconi; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| SID (System for Incremental Development) is a computer system for incrementally designing and verifying large, complex programs. It executes commands, proposes actions, answers questions, and accepts and reasons about new or changed information. SID has three main, distinctive characteristics: (1) it provides several useful incremental capabilities, including the ability to respond to changes by ensuring that the final problem solution is consistent and by keeping intact still-valid work without complete ... |
|
| Interactive Compiler Proving Using Hoare Proof Rules. |
JAN 1978 |
|
| Authors:
Donald Scott Lynn; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This report demonstrates the proofs by structural induction of two compilers. The larger is a compiler from a subset of pure LISP into a machine language, and is similar to a compiler proved by London. The smaller is the compiler proved by McCarthy and Painter. In addition a portion of another compiler is proved. It is the compiler given by Wirth to compile a simple Pascal-like language (PL/0) into code ... |
|
| Meta-Evaluation as a Tool for Program Understanding. |
JAN 1978 |
|
| Authors:
Robert Balzer; Neil Goldman; David Wile; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This report describes the technology used in a running system that embodies theories of program well-formedness and informality resolution established by symbolically executing the program to systematically discover the intended meaning of each informal construct within an informal specification. |
|
| ARPANET Transition Opportunities and Gateway Considerations. |
21 DEC 1977 |
44 pages |
| Authors:
Jonathan B. Postel; Stephen D. Crocker; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| Issues in the transition of the ARPANET are discussed and a plan is outlined. The use of gateways is suggested, and issues related to them are discussed. The appendices include comparisons between alternate designs for three families of higher level protocols, host-to-host, terminal access, and file transfer. (Author) |
|
| The Military Message Experiment SIGMA Primer. |
NOV 1977 |
|
| Authors:
Chloe Holg; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| The purpose of this primer is to provide basic instruction to military personnel in the use of the SIGMA message service designed for use in the Military Message Experiment. By following the instructions presented in this primer, military personnel without previous computer or terminal experience may easily and quickly become familiar with MME-SIGMA and its use. |
|
| PRIM System. U1050 User Guide and User Reference Manual. |
OCT 1977 |
|
| Authors:
Louis Gallenson; Alvin Cooperband; Joel Goldberg; UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
|
| This is a two-part manual for users of the PRIM-based U1050 emulator. The manual demonstrates as well as describes the capabilities of PRIM, running and debugging of object code, and the emulated computer system. (Author) |
|
Reports by Corporate Author
