10 nowrap> « back to results for ""
Below is a cache of http://www.cs.utexas.edu/users/boyer/ftp/ics-reports/cmp48.pdf. It's a snapshot of the page taken as our search engine crawled the Web.
The web site itself may have changed. You can check the current page or check for previous versions at the Internet Archive. Yahoo! is not affiliated with the authors of this page or responsible for its content.
The Gypsy 2.0 and Gypsy 2.1 differences have been removed and placed in a separate document.) The Gypsy 2.0 and Gypsy 2.1 differences have been removed and placed in a separate document.) Report on Gypsy 2.05
February 1, 1986
Donald I. Good
Robert L. Akers
Lawrence M. Smith
Institute for Computing Science
2100 Main Building
The University of Texas at Austin
Austin, Texas 78712
(512) 471-1901 Abstract
Gypsy is a collection of methods, languages, and tools for building formally verified computing systems.
Gypsy provides capabilities specifying a system, implementing it, and for using formal, logical deduction to
prove important properties about the specification and the implementation of the system. The Gypsy program
description language is a single, unified language that is used to express both the specification and the
implementation of a computing system. This report defines the Gypsy 2.05 program description language.
Gypsy 2.05 includes almost all of Gypsy 2.0 with some extensions and minor modifications. Preface
The development of Gypsy began late in 1974, and the first report on Gypsy 1.0 was issued in August 1976.
Initial attempts to use Gypsy 1.0, to define its specification and proof methods and to implement it led to a
number of significant language revisions. The report on Gypsy 2.0 was issued in September 1978. Although
Gypsy 2.0 extended Gypsy 1.0 in some significant ways, Gypsy 2.0 primarily was a simplification of Gypsy
1.0. In order to provide a stable implementation target, the definition of Gypsy 2.0 has remain fixed until this
time. Now, based on the experience of the last several years of using and implementing Gypsy 2.0, this report
describes Gypsy 2.05. Again, Gypsy 2.05 primarily is a slightly extended subset of Gypsy 2.0.
The style and organization of this report on Gypsy 2.05 is a major change from the Gypsy 2.0 report. The
reason for this change is to make the report much more concise and readable. The style of presentation is
informal, but precise, and the organization is from the simpler to the more complex parts of the language.
Chapter 1 gives a summary of the basic Gypsy concepts. Chapters 2-7 are sufficient to specify and implement
simple sequential programs. Chapters 8-11 describe the more advanced parts of Gypsy, exception conditions,
dynamic objects, concurrency, and type abstraction.
In this organization, the chapters that describe the basic facilities make forward references to the existence
of the more advanced ones.
For example, Chapter 3 on types describes the Gypsy type mechanism and
mentions all of the possible types.
However, only the simple types and the static type compositions are
described there. The others are described in later chapters. The index of this report gives the page that defines
each phrase in the language.
This report on Gypsy 2.05 immediately supersedes the report on Gypsy 2.0. There will, however, be a
period of transition during which the Gypsy Verification Environment (GVE) will continue to operate on Gypsy
2.0. Because Gypsy 2.05 consists mainly of a large subset of Gypsy 2.0, this report on Gypsy 2.05, for the
greatest part, is also a report on Gypsy 2.0. The cases where Gypsy 2.05 differs from Gypsy 2.0 are described
in a separate document, entitled "Differences in Gypsy Dialects," by Lawrence M. Smith and Robert L. Akers.
During the transition period, these two documents together may serve as a report on Gypsy 2.0. Acknowledgements
The contributions of Allen L. Ambler, Robert L. Akers, Richard E. Alterman, William R. Bevier, Woodrow
W. Bledsoe, James C. Browne, Wilhelm F. Burger, Richard M. Cohen, Carol A. David, Benedetto L. DiVito,
Dwight F. Hare, Charles G. Hoch, Gary R. Horn, John H. Howard, James C. Hsu, Lawrence W. Hunter, James
Keeton-Williams, John McHugh, Judith S. Merriam, Mark S. Moriconi, Karl Nyberg, Ann E. Siebert, Lawrence
M. Smith, Michael K. Smith, Russell A. Still, Anand V. R. Tripathi, Robert E. Wells and William D. Young to
the development, implementation and initial experimental applications of Gypsy are gratefully acknowledged.
Special acknowledgment is given to Robert L. Akers who prepared much of the material in the appendices of
this report.
Pascal was the starting point for the development of Gypsy, and there are still strong semantic similarities.
The languages Algol 60, Algol 68, Alphard, CLU, Concurrent Pascal, Euclid, Fortran, Nucleus, Simula and
Special and the structured programming principles pioneered by Edsger W. Dijkstra and C. A. R. Hoare also
have provided an assortment of fruitful ideas from which to draw.
The development, implementation and initial experimental applications of Gypsy have been sponsored
primarily by the National Computer Security Center (Contracts MDA904-80-C-0481, MDA904-82-C-0445).
Additional sponsorship has been provided by the U. S. Space and Naval Warfare Systems Command (formerly
Naval Electronic Systems Command) (Contract N00039-81-C-0074), by the U. S. Air Force Rome Air
Development Center (Contract F30602-84-C-0081), by Digital Equipment Corporation, by Digicomp Research
Corporation, and by the National Science Foundation (Grant MCS-22039). GYPSY 2.05 REPORT
FEBRUARY 1, 1986
1
Chapter 1
BASIC CONCEPTS
Gypsy is a language for specifying, implementing and proving computer programs. A specification
describes what effect is desired when a program runs, an implementation defines how the effect is caused, and a
proof verifies that the program always runs as specified.
1.1 Programs
A Gypsy program is a mechanism whose operation causes an effect on its environment. The environment
of a Gypsy program consists of data objects and exception conditions. Every data object has a name and a
value. The only ways that running a program can cause an effect on its environment are by changing the value
of a data object or by signalling a condition. A data object always has some value specified by the type of the
object. Normally, a program causes an effect on its environment by changing the value of some data object. A
program also, however, can signal an exception condition.
Normally, this is done only to indicate that
something unusual has happened.
1.2 Specification
A Gypsy specification is a declarative statement about the environment of a program. Every program must
have a environment specification, and it also may have operational specifications.
The environment specification names every data object and exception condition in the environment. It also
specifies the type of each data object and whether the object is variable or constant. The program can change
the value of a variable object, but it can not change the value of a constant object.
The environment
specification completely isolates the effects of running the program. The only objects that a program can have
access to are those that are named in its environment specification, and the only ones that it can change are its
variable objects.
The environment specification provides a very weak, but complete, description of the effect caused by
running a program. It defines completely what objects are in the environment and it identifies all those that
might be changed as a result of running the program. Operational specifications may be used to state much
stronger specifications. An operational specification gives a statement about what values the data objects may
have as the program runs. An operational specification may make a very strong statement that describes many
properties about the effect that is to be caused by a program, or it may make only a very weak statement that
describes only a few properties. The strength of a specification is matter of human choice. GYPSY 2.05 REPORT
FEBRUARY 1, 1986
2
1.3 Implementation
A Gypsy implementation of a program is an imperative statement of how the program causes its effect. A
program is implemented by describing how it is composed of pre-defined programs.
Some of these are
standard programs that are pre-defined by the Gypsy language, and others may be pre-defined by a particular
implementation of the language (for example to provide i/o support on a particular machine).
1.4 Proof
Gypsy supports proofs about specifications and proofs about programs. Specifications are stated in terms of
compositions of mathematical functions. Theorems about these functions and their compositions can be stated
directly in the Gypsy specification language, and they can be proved in the Gypsy proof system.
The specifications of a program define constraints on its implementation. The specifications of a program
can be viewed as sensors that are attached to its environment. The specification sensors are app