REPORT ON THE LANGUAGE GYPSY Version 2.0 Donald I. Good Richard M. Cohen Charles G. Hoch Lawrence W. Hunter Dwight F. Hare September, 1978 ICSCA-CMP-10 Revision 1 CERTIFIABLE MINICOMPUTER PROJECT Institute for Computing Science and Computer Applications The University of Texas at Austin Austin, Texas 78712 TABLE OF CONTENTS Chapter 1 INTRODUCTION . . . . . . . . . . . . . . . . . . 1-1 1.1 LANGUAGE SUMMARY . . . . . . . . . . . . . . . 1-3 1.1.1 Common Concepts . . . . . . . . . . . . 1-3 1.1.2 Programs . . . . . . . . . . . . . . . . 1-7 1.1.3 Specifications . . . . . . . . . . . . . 1-9 1.2 PROGRAM DEVELOPMENT . . . . . . . . . . . . . . 1-11 1.3 REPORT SUMMARY . . . . . . . . . . . . . . . . 1-12 1.3.1 Syntax . . . . . . . . . . . . . . . . . 1-13 1.3.2 Semantics . . . . . . . . . . . . . . . 1-14 Chapter 2 LEXICAL STRUCTURE . . . . . . . . . . . . . . . . 2-1 2.1 IDENTIFIERS . . . . . . . . . . . . . . . . . . 2-2 2.2 LITERAL CONSTANTS . . . . . . . . . . . . . . . 2-3 2.2.1 Characters . . . . . . . . . . . . . . . 2-3 2.2.2 Strings . . . . . . . . . . . . . . . . 2-3 2.2.3 Numbers . . . . . . . . . . . . . . . . 2-4 2.3 COMMENTS . . . . . . . . . . . . . . . . . . . 2-4 2.4 UPPER/LOWER CASE CONVENTION . . . . . . . . . . 2-5 2.5 BRACKETING CONVENTION . . . . . . . . . . . . . 2-5 2.6 PENDING . . . . . . . . . . . . . . . . . . . . 2-5 Chapter 3 PROGRAM DESCRIPTIONS . . . . . . . . . . . . . . 3-1 3.1 SCOPE DECLARATIONS . . . . . . . . . . . . . . 3-2 3.2 UNIT DECLARATIONS . . . . . . . . . . . . . . . 3-4 3.3 NAME DECLARATIONS . . . . . . . . . . . . . . . 3-5 3.4 ACCESS LISTS . . . . . . . . . . . . . . . . . 3-6 3.5 NAME SCOPES . . . . . . . . . . . . . . . . . . 3-6 3.6 IMPLEMENTATION DEFINED UNITS . . . . . . . . . 3-7 3.7 UNIT INDEPENDENCE . . . . . . . . . . . . . . . 3-8 Chapter 4 ROUTINE DECLARATIONS . . . . . . . . . . . . . . 4-1 4.1 PROCEDURE HEADER . . . . . . . . . . . . . . . 4-3 4.2 FUNCTION HEADER . . . . . . . . . . . . . . . . 4-5 4.3 FORMAL DATA PARAMETERS . . . . . . . . . . . . 4-6 4.4 FORMAL CONDITION PARAMETERS . . . . . . . . . . 4-8 4.5 ROUTINE BODY . . . . . . . . . . . . . . . . . 4-9 4.6 DYNAMIC EXTERNAL SPECIFICATIONS . . . . . . . . 4-11 4.7 LOCAL DECLARATIONS . . . . . . . . . . . . . . 4-14 4.8 INTERNAL SPECIFICATIONS . . . . . . . . . . . . 4-15 Chapter 5 CONSTANT DECLARATIONS . . . . . . . . . . . . . . 5-1 Chapter 6 LEMMA DECLARATIONS . . . . . . . . . . . . . . . 6-1 Chapter 7 TYPES . . . . . . . . . . . . . . . . . . . . . . 7-1 7.1 THE CONCEPT OF TYPE . . . . . . . . . . . . . . 7-2 7.2 TYPE CONSISTENCY . . . . . . . . . . . . . . . 7-2 7.3 TYPE DECLARATIONS . . . . . . . . . . . . . . . 7-4 7.4 DATA ABSTRACTION . . . . . . . . . . . . . . . 7-6 7.5 TYPE DEFINITIONS . . . . . . . . . . . . . . . 7-9 7.6 TYPE REFERENCES . . . . . . . . . . . . . . . . 7-10 7.7 SIMPLE TYPES . . . . . . . . . . . . . . . . . 7-13 7.7.1 Scalar Types . . . . . . . . . . . . . . 7-15 7.7.2 Scalar Type Character . . . . . . . . . 7-16 7.7.3 Boolean Type . . . . . . . . . . . . . . 7-17 7.7.4 Integer Type . . . . . . . . . . . . . . 7-18 7.7.5 Rational Type . . . . . . . . . . . . . 7-19 7.7.6 Properties Of Numeric Types . . . . . . 7-20 7.7.7 Subrange Types . . . . . . . . . . . . . 7-21 7.8 STRUCTURED TYPES . . . . . . . . . . . . . . . 7-21 7.9 STATIC STRUCTURED TYPES . . . . . . . . . . . . 7-22 7.9.1 Records . . . . . . . . . . . . . . . . 7-22 7.9.2 Arrays . . . . . . . . . . . . . . . . . 7-25 7.10 DYNAMIC STRUCTURED TYPES . . . . . . . . . . . 7-27 7.10.1 Sets . . . . . . . . . . . . . . . . . 7-27 7.10.2 Mappings . . . . . . . . . . . . . . . 7-30 7.10.3 Sequences . . . . . . . . . . . . . . . 7-34 7.11 OTHER TYPES . . . . . . . . . . . . . . . . . 7-36 7.11.1 Activationid Types . . . . . . . . . . 7-36 7.11.2 Buffer Types . . . . . . . . . . . . . 7-37 Chapter 8 ROUTINE CALLS . . . . . . . . . . . . . . . . . . 8-1 8.1 ACTUAL DATA PARAMETERS . . . . . . . . . . . . 8-2 8.2 ACTUAL CONDITION PARAMETERS . . . . . . . . . . 8-4 8.3 MAIN PROGRAM, INPUT AND OUTPUT . . . . . . . . 8-5 Chapter 9 EXPRESSIONS . . . . . . . . . . . . . . . . . . . 9-1 9.1 SPECIFICATION EXPRESSIONS . . . . . . . . . . . 9-1 9.2 SIMPLE EXPRESSIONS . . . . . . . . . . . . . . 9-3 9.3 OPERATORS . . . . . . . . . . . . . . . . . . . 9-4 9.3.1 Function Composition . . . . . . . . . . 9-5 9.3.2 Operator Axioms . . . . . . . . . . . . 9-7 9.4 VALUE REFERENCES . . . . . . . . . . . . . . . 9-10 9.4.1 Selector Clauses And Lists . . . . . . . 9-12 9.4.2 Alteration Clauses . . . . . . . . . . . 9-15 9.5 IF EXPRESSIONS . . . . . . . . . . . . . . . . 9-18 9.6 QUANTIFIED EXPRESSIONS . . . . . . . . . . . . 9-19 9.7 SET AND SEQUENCE CONSTRUCTORS . . . . . . . . . 9-21 Chapter 10 STATEMENT LISTS . . . . . . . . . . . . . . . . 10-1 10.1 ASSERT SPECIFICATION . . . . . . . . . . . . . 10-2 10.2 PROCEDURAL STATEMENTS . . . . . . . . . . . . 10-3 10.2.1 Procedure Call Statement . . . . . . . 10-3 10.2.2 Assignment Statement . . . . . . . . . 10-4 10.2.3 Remove Statements . . . . . . . . . . . 10-6 10.2.4 Move Statements . . . . . . . . . . . . 10-7 10.2.5 Send Statement . . . . . . . . . . . . 10-8 10.2.6 Give Statement . . . . . . . . . . . . 10-9 10.2.7 Receive Statement . . . . . . . . . . . 10-9 10.3 SEQUENTIAL CONTROL STATEMENTS . . . . . . . . 10-9 10.3.1 If Statements . . . . . . . . . . . . . 10-9 10.3.2 Case Statements . . . . . . . . . . . . 10-9 10.3.3 Loop Statements . . . . . . . . . . . . 10-9 10.3.4 Begin Statements . . . . . . . . . . . 10-9 10.3.5 Leave Statement . . . . . . . . . . . . 10-9 10.3.6 Signal Statement . . . . . . . . . . . 10-9 10.4 CONCURRENT CONTROL STATEMENTS . . . . . . . . 10-9 10.4.1 Cobegin Statement . . . . . . . . . . . 10-9 10.4.2 Await Statements . . . . . . . . . . . 10-9 10.5 CONDITION HANDLING . . . . . . . . . . . . . . 10-9 REFERENCES . . . . . . . . . . . . . . . . . . . . . . . . . 11-1 Appendix A GYPSY REWRITE RULES . . . . . . . . . . . . . . A-1 Appendix B CROSS REFERENCE OF NONTERMINAL SYMBOLS . . . . . B-1 Appendix C CROSS REFERENCE OF RESERVED WORDS . . . . . . . C-1 Appendix D PREDEFINED IDENTIFIERS AND STANDARD FUNCTIONS . D-1 Appendix E PROGRAM EXAMPLES . . . . . . . . . . . . . . . . E-1 INDEX . . . . . . . . . . . . . . . . . . . . . . . . . . . I-1 ACKNOWLEDGMENTS Gypsy has been developed as the central component of a comprehensive and unified methodology for developing verified communications processing systems of practical interest [Good, 77]. The development of the methodology began in September, 1974, and work on the actual language began in the Spring of 1975. The first "Report on the Language Gypsy, Version 1.0" appeared in August, 1976 [Ambler, 76]. The experience gained from developing Version 1.0 and using it in a variety of applications have led to this new "Report on the Language Gypsy, Version 2.0". Throughout this period, the development of Gypsy has been the cooperative effort of many people with diverse experiences and interests. The development of Gypsy also has drawn significantly from a number of other languages. The first acknowledgement must be of Allen L. Ambler, who led the development of Version 1.0. The major concepts and directions set forth in Version 1.0 have remained unchanged. James C. Browne, Wilhelm F. Burger, John H. Howard, James Keeton-Williams, Judith S. Merriam, Mark S. Moriconi, Larry M. Smith, and Robert E. Wells also have contributed significantly to the design, development, and implementation of Gypsy. The first acknowledgement of languages must be of Pascal [Jensen, 74]. Gypsy was developed primarily from Pascal and still bears a considerable resemblance to it. The work of [Hoare, 72] also had a considerable influence on the language design. The ideas and features of Algol 60 [Naur, 63], Algol 68 [van Wijngaarden, 68], Alphard [Wulf, 77], CLU [Liskov, 76], Concurrent Pascal [Brinch Hansen, 75], Euclid [Lampson, 76], Fortran [ANSI, 66], Nucleus [Good, 73], Simula [Dahl, 66], and Special [Roubine, 76] also have influenced the design of Gypsy. We are fortunate to have had this diversity of ideas and approaches from which to draw, and have made every attempt to use this background to design a coherent and useful language that meets our goal of practical verifiability. We gratefully acknowledge the help of Carol A. David in the preparation of the program examples used in this manual and in proof reading the numerous drafts of this document. We also express our sincere thanks to Kathryn S. Richardson and Laura K. Metheny who prepared the seemingly endless versions of this report. CHAPTER 1 INTRODUCTION Gypsy is a verifiable program description language. It is a single, unified language for describing two major aspects of a computer program: the program itself, and its formal specifications. A sentence in Gypsy may describe the actual parts of a program, it may describe the formal specification of the program, or it may describe both. Sentences in the language are called program descriptions.M _______ ____________ Gypsy is fully verifiable in that formal, automatable methods for verifying the consistency of a program and its specifications exist for all program descriptions. Gypsy was developed from Pascal specifically to describe verified systems programs. The capabilities of Pascal that lead to verification difficulties have been eliminated. However, Gypsy still retains a large measure of the generality of Pascal, with its main deficiency being the absence of floating point numbers. After eliminating the verification difficulties of Pascal, other capabilities were added to enhance verification and to support systems programming and, in particular, communications processing applications. These capabilities include formal specification, data abstraction, condition handling, concurrency, and storage management without explicit pointers. The result is a verifiable program description language that can be used in general programming, systems programming, and communications processing applications. Gypsy has a number of important characteristics that collectively distinguish it from other languages. 1. Gypsy is a program description language that integrates formal specification and programming facilities into a single, unified language. This permits specification, programming, and verification to be performed within a common conceptual framework throughout the complete development cycle of a verified program. 2. The presence of specifications directly in the programming language makes possible two complementary approaches to formal verification: verification by proof, and verification by validating (evaluating) specifications at run-time. The same specification language is used with both approaches. 3. Gypsy is a fully verifiable language; formal proof methods exist for all program descriptions in the language. Many features of Gypsy have been developed directly from well established mathematical concepts specifically to satisfy the INTRODUCTION Page 1-2 requirements of complete verifiability. 4. Gypsy can be used either for actual programs or for theoretical programs. Gypsy contains a number of well-defined concepts from mathematics that are not effectively realizable on an actual implementation of the language. Examples of these theoretical concepts are the unbounded sets of integer and rational numbers. These unrealizable features, which follow directly from the specification facilities, allow Gypsy to be used as a basis for formal theoretical verification and analysis, even though a given program may not be realizable by any actual implementation. 5. Formal specifications can be expressed using the "assertion", "state machine", and "algebraic" approaches. These three approaches are integrated into a single specification language and can be used conveniently and effectively in any combination. 6. Gypsy provides facilities for general programming, systems programming, and communications processing applications. These facilities include most of the basic ones from Pascal and also data abstraction, condition handling, concurrency, and storage management without explicit pointers. 7. Gypsy is designed to support incremental, step-by-step development of program descriptions and to enhance independent verification and compilation of individual routines. The specification, programming, and verification methods are designed so that the verification of one routine is independent of the verification of any other routine, even in the presence of concurrency. The objective of a verifiable program description language is to increase program quality and, in particular, program reliability. A verification demonstrates that a program always executes according to specifications. This demonstration of consistency between a program and its specifications does not guarantee perfect program quality or reliability. It can, however, provide program quality that is much increased over the quality usually associated with unverified programs. The increased quality of a verified program comes from two sources: the formal specifications and the verification itself. The formal specifications are a precise description of the goals of the program. The program itself describes how these goals are to be attained. Thus the specifications and the program together provide two precise, but different and redundant, descriptions of the run-time behavior of the program. The first source of increased program quality, therefore, is the redundant description of the program provided by the formal specifications. The second source of improved program quality is the actual verification. Formal verifications can be performed with the same degree of rigor and precision that is used in mathematics. Therefore, INTRODUCTION Page 1-3 verification can, in principle, raise program quality to a level comparable to mathematics. Though not infallible, the quality of mathematical proofs and analyses has far exceeded that of unverified programs. Attaining this level of program quality would be a substantial step forward. The main objective of Gypsy is to provide a language in which this step can be attained in practice as well as in principle. 1.1 LANGUAGE SUMMARY The Gypsy language was designed as a unified language for expressing both a program and its formal specifications. It can be viewed as intersecting sub-languages: one for formal specification and one for programming. The sub-languages may be used individually or they may be used together to describe a verified program which is the main objective of Gypsy. Many fundamental concepts of the language are taken directly from mathematics or modeled after those in Pascal. The mathematical aspects of Gypsy provide sound and rigorous methods of analysis, and Pascal has provided a well-established foundation for a verifiable program description language. The following sections summarize the complete language and its relationship to mathematics and to Pascal. 1.1.1 Common Concepts Many Gypsy concepts are common to both the specification language and the programming language. This allows both a program and its specifications to be expressed within a common conceptual framework. Every Gypsy program is described within this framework by several different kinds of program description units: "functions", "procedures", "lemmas", "types", and "constants". The functions, procedures, types, and constants are similar to those of Pascal. Lemmas are adapted from their corresponding mathematical concept and used only for specification. Any unit except a lemma may be at least partially involved in expressing either the program or its specifications, and certain parts of a unit may be involved simultaneously in expressing both. For example, a type may be referred to only in a program, or only in a specification, or it may be referred to in both. Regardless of how it is used, the interpretation of the type is the same. The same kinds of units may appear in both specifications and programs and their interpretations are exactly the same in either case. All operations in Gypsy are performed by activations of two kinds of routines: functions and procedures. Various components of the definition of a routine may be part of either the specification or the implementation of the routine, while other parts may be both. Every routine has a "header" and may or may not have a "body". The header defines the name of the routine and its formal parameters and is always considered as a part of the formal specification of the routine. If the routine has a body, that body may include further specifications and also the implementation of the routine in the INTRODUCTION Page 1-4 1.1.1 Common Concepts programming language. If the body of the routine includes no implementation, the routine is being used strictly for specification. If the body does include an implementation, then the routine header also becomes part of the implementation because it involves parameter passage. Thus the header may serve simultaneously as specification and implementation. Routine parameters may be either data or condition parameters. Data parameters may be either "const" or "var" parameters. Both const and var parameters are passed by reference. (This differs from Pascal, where const parameters are passed by value.) The value of a var parameter, but not a const parameter, may be altered by theM ___ routine. Potential alteration of const parameters is checked syntactically. Only expressions of variables and constants may be passed as actual parameters for const and var parameters. Condition parameters are exception conditions that may be signalled into the calling environment upon abnormal termination of a routine. The actual condition parameter must be a condition in the calling environment. The only conditions that may be signalled into the calling environment are those that correspond to the formal condition parameters or the pre-defined condition "routineerror", which is interpreted uniformly as "some condition other than a condition parameter". This prevents a routine from inadvertently revealing its implementation details to the calling environment. A routine may not refer to any non-local variables, constants, orM ___ conditions except globally defined constants. This restriction provides a number of important advantages for independent processing of routines. Independent verification and compilation is enhanced and the type composition mechanisms of Gypsy minimize the need for the lengthy parameter lists that might be expected from such a restriction. Procedures may have const, var, or condition parameters. The effects of a procedure on its calling environment are strictly limited to the actual parameters that correspond to var and condition parameters. Potentially dangerous aliasing is not allowed and its presence can be detected by analyzing only the actual parameters of procedure calls. Potential satisfaction of the non-aliasing requirement is enforced statically. Those parts of the requirement that cannot be enforced statically are checked at run time. A function may have const and condition but not var parametersM ___ and it returns a value. The value returned by a function is called "result" within the function. The function result may be of any type, rather than just a simple type as in Pascal. This is necessary for functions to be used effectively in specifications and is also allowed in implementations. Because of the absence of non-local referencing and var parameters, a function cannot produce side effects in its calling environment. Its effects are strictly limited to its result value and to its condition parameters. Functions in Gypsy are intended to be equivalent to single-valued functions in mathematics, and the absence of var parameters, non-local references, and side-effects is necessary to preserve this INTRODUCTION Page 1-5 1.1.1 Common Concepts equivalence. With this equivalence preserved, Gypsy functions may be used freely in the algebraic expressions that are a central part of formal specification and verification. Unfortunately, the absence of var parameters and non-local referencing restrictions in Gypsy functions is not sufficient to maintain completely the desired equivalence with mathematics. Gypsy functions that include an implementation that has access to the concrete structure of an abstract type or that involves concurrency may be non-deterministic -- different activations of the same function on the same parameters mayM_________ ____ ____ give different results. Determinism is a property that must be provedM _________ about a Gypsy function if it is to be used algebraically. A strong type consistency is required between corresponding actual and formal parameters of all program description units. Every data object has a type which defines certain constraints on that object. The type consistency between actual and formal parameters is defined so that routines can be analyzed strictly on the basis of their formal parameters without regard to any actual parameters; the consistency rules then ensure that the type constraints of the actual parameters satisfy the type constraints of the formals. Potential satisfaction of type consistency is enforced statically; the parts that cannot be enforced statically are checked at run time. This type consistency is essential for verification and is enforced in both the specification and the implementation of a program. Gypsy has three kinds of types: simple, structured, and special types to support concurrency. The simple types are the scalar types and types "character", "boolean", "integer", and "rational". Scalar types, such as "(red, blue, green)", are analogous to those in Pascal. Character is the predefined scalar type whose values are the 7-bit ASCII characters. Boolean is the predefined scalar type "(false, true)". The integer and rational types are the complete unbounded sets of integer and rational numbers of conventional mathematics. Subranges of the simple types also may be defined. The structured types are "records", "arrays", "sets", "sequences", and "mappings". Each corresponds to a well-developed mathematical concept. Records correspond to the mathematical concept of n-tuple and are the same as in Pascal (except that variant records are not permitted). Record components are selected by the notation "r.f" where "r" is the record object and "f" the selector. Arrays correspond to the mathematical concept of vector and are similar to Pascal. Only one dimensional arrays are allowed, but arrays of arrays are permitted. Array elements are selected with the usual "a(i)" notation. Sets and sequences correspond directly to mathematical sets and sequences. The elements of a sequence are selected by "s(i)". Subsequences are selected by "s(i..j)". Mappings also correspond to the mathematical concept of mapping. A mapping is a set of ordered pairs (x,y) such that first members of the pairs are values of some domain type and second members are values of some range type. The first members of all pairs must be unique. The image of a domain element is selected by "m(x)". INTRODUCTION Page 1-6 1.1.1 Common Concepts The special types to support concurrency are the shared types and type "activationid". There is only one shared type, "buffers". Buffers are a special type for synchronizing procedures that run concurrently. A buffer is strictly a first-come, first-serve queue of elements of a given type, and is protected by a semaphore that enforces mutually exclusive access to the buffer. All communication between concurrently running procedures must be through buffers. Activationids are a special type that is used in specification and verification to identify different concurrent activations of the same procedure. Sets, sequences, mappings, and buffers are dynamic types. The number of elements of a dynamic type may vary, whereas the number of elements in a static type (records, arrays) may not. An upper bound for the number of elements of a dynamic type may be declared or the dynamic types may be unbounded. Arbitrary compositions of all non-buffer structured types are allowed. Gypsy provides a simple yet powerful mechanism for data abstraction. The declaration of a type may contain a "composition access list" that enumerates the names of all program description units that are granted knowledge of the composition of the type. A type declaration with a composition access list is an abstract type. Its primitive operations are those routines named in the composition access list. The composition access list supports most current approaches to data abstraction and also permits the same routine to have concrete access to more than one type of abstract object, if necessary. The access restrictions implied by the composition access lists can be enforced strictly by a syntactic analysis of the text of the program description. A special mechanism is provided for extending the equality operator to objects of an abstract type. The "=" operator can be used on abstract objects iff these extensions are made. The extension of the equality operator is the mechanism for defining the correspondence between abstract and concrete objects. This correspondence is defined by the mathematical concept of equivalence classes. Gypsy differs significantly from Pascal in that the declarations of program description units generally may not be nested. The only exception to this is that constants may be declared within routines. The declaration structure of program description units in Gypsy is essentially flat rather than hierarchical. With non-local referencing of variables disallowed, the only remaining effect of a hierarchical declaration structure is to control access to the names of program description units. Access to the names of units in Gypsy is controlled explicitly by name scopes and explicit reference access control lists. Declarations of program description units may be grouped together lexically in an explicit unit name "scope". Potentially, the units within a given scope may refer to each other freely and also may refer to units in other scopes through a "name declaration". This potentially free access to a unit may be restricted by a "reference access list" associated with a unit declaration. The reference access list explicitly enumerates all units that may refer to the unit being declared. These mechanisms can be used to provide a hierarchical name space control or to provide a finer degree of name space control, if necessary. The unit name scope INTRODUCTION Page 1-7 1.1.1 Common Concepts and the reference access lists provide a powerful approach to controlling the ability of one unit to refer to another, but still retain a flat declaration structure that significantly enhances independent verification and compilation of individual program description units. 1.1.2 Programs A Gypsy program may be expressed as a set of function, procedure, type, and constant units. The implementation of a routine, as expressed in its body, may refer to any of the operations and types available in the language -- e.g., integer and rational types even though the values of these types are arbitrarily large. Any particular implementation of the language, however, is not required toM ___ support all of the types and operations of the language. The onlyM ____ requirement of a language implementation is that those facilities made available be consistent with the language definition. For example, an implementation of Gypsy normally would not support types integer and rational, but would support a subrange of type integer that could be implemented efficiently on a particular machine. This subrange, however, must conform absolutely to the language concepts of integers and subranges. Thus, all Gypsy programs and specifications have an interpretation that is uniform for all language implementations. The implementation of a particular program unit, however, may or may not be "realizable" in a particular implementation of the language. The formal specification and verification methods can be applied in exactly the same way to both realizable and unrealizable programs.M_______ Thus, Gypsy is equally usable for the description and analysis of either theoretical or actual programs. The execution of a routine is defined by its body. The body may instantiate local constants and variables. Constants and variables are initialized upon instantiation to either a programmer-supplied value or default value defined by their type. As in Pascal, variables may be instantiated only upon routine activation. The basic statements that can be executed by a routine are "procedure calls", "assignment", "if", "case", "loop", and "leave". The procedure call, assignment, if, and case are similar semantically to Pascal. The Gypsy if statement has an "elif" option and the case statement has an "else" label to refer to all cases not otherwise explicitly enumerated. The loop and leave subsume the "while" and "repeat" of Pascal as well as a number of other useful loop structures. Verification methods for these basic statements are straightforward and most are well-known. The Gypsy facilities for dynamic storage management are based on the dynamic types (sets, sequences, mappings, and buffers) rather than on the explicit pointers of Pascal. The effects of manipulating objects of dynamic types are defined algebraicly in terms of structural copying, but the objects of these dynamic types actually can be allocated and deallocated dynamically. New elements may be inserted into a dynamic structure through the normal assignment statement. Objects can be deleted from a structure by a special remove statement or can be moved from one dynamic structure to INTRODUCTION Page 1-8 1.1.2 Programs another. These movements are constructed so that the same object may never appear simultaneously in more than one dynamic structure. This completely eliminates the possibility of dangling references and the difficulties of determining potentially dangerous aliasing through explicit pointers. The axiomatic properties of sequences and mappings and their corresponding verification methods are similar to those for arrays. Condition handling is a necessary requirement in systems programming. Exception conditions in Gypsy may be signalled as a result of a routine call or an explicit signal statement. The condition can be handled by a when clause that can appear at the end of any structured statement (if, case, loop, begin, cobegin, await) within the routine in which a condition is signalled. A when clause is similar in appearance and effect to a case statement whose labels are conditions. When a condition "c" is signalled, control is transferred immediately to the when clause of the most tightly enclosing structured statement. If that statement has a when clause with a case labelled "c", then the condition is handled by the statements following that label with control resuming from the end of the structured statement. If "c" is signalled, but the enclosing statement does not have a when clause with label "c", then control is transferred to the when clause of the next enclosing structured statement. If the condition is not handled by any when clause in the routine, a "routineerror" is signalled to the calling environment rather than the condition "c". Conditions and signals are a very restricted form of labels and gotos. Verification of the exception handling mechanisms is straightforward and requires only the construction of additional verification conditions that correspond to control paths that can be followed from the signalling through the handling of the condition. These extra verification conditions are strictly local to the routine that signals a condition. Gypsy has facilities for explicit concurrency. These are the only facilities in the language that are specialized for communications processing. Concurrent processes may be created by a cobegin statement that contains a number of procedure calls. When a routine enters a cobegin, it is deactivated and each activation of each called procedure becomes a separate process. The parent routine is reactivated when all processes of the cobegin terminate. This preserves a single-entry, single-exit control structure. Processes running concurrently may communicate only through buffers. Buffers are strictly first-come, first-serve queues that are manipulated by "send", "receive", and "give" statements that provide mutually exclusive access. A send statement queues an object to a buffer without changing the value of the object; give moves part of a dynamic structure from the structure to the buffer. The receive statement dequeues an object from the buffer and assigns it to some variable. A send or a give to a full buffer blocks the sending or giving process until an object is taken from the buffer; likewise, a receive from an empty buffer blocks the receiving process until some object is placed in the buffer. Another form of concurrency is provided by the await statement which behaves like a non-deterministic case statement. The "labels" of the await are simple buffer statements (send, receive, give). The await will select non-deterministically some branch whose "label" is not blocked. The verification methods for concurrency are INTRODUCTION Page 1-9 1.1.2 Programs unique to Gypsy. Their distinguishing characteristic is that they permit the verification to be factored on a routine by routine basis rather than having to consider several concurrent processes simultaneously. This factoring is essential for practical applications. 1.1.3 Specifications The Gypsy specification language unifies three major approaches to formal verification: the "assertion", "state machine", and "algebraic" approaches. The "assertion" approach has developed as a matter of necessity along with the development of formal program verification methods. Its specifications are typically stated as various forms of program annotations. The "state machine" approach refers to the "modules" introduced by Parnas and successive developments of this approach. The "algebraic" approach refers to the use of algebraic axioms to define abstract data types. Currently there is not yet enough experience with any of these approaches to identify one as clearly superior to the others. Gypsy has been designed so that these three approaches can be used individually or collectively. A formal specification in Gypsy may be expressed as a set of procedure, function, lemma, type, and constant units. The specifications of the "assertion" approach can be stated in terms of "entry", "exit", and "assert" specifications that are written within a routine. Procedures and functions can be used to express the O-functions and V-functions of the "state machine" approach, and lemmas can be used to express the axioms of the "algebraic" approach. Routines may have both external and internal specifications. External specifications are potentially visible to other routines, whereas internal specifications are not. The routine header defines the "static" external specifications. "Abstract dynamic" external specifications are expressed as the "entry" and "exit" specifications normally used in the "verification" approach. Dynamic external specifications may refer only to formal parameters and global constants and may not refer to the concrete structure of any abstract type. The entry specification must hold among routine parameters whenever the routine is activated. The exit specification is interpreted in its "weak" sense so its relation needs to hold only ifM __ the routine terminates. An exit specification may be expressed as individual cases that correspond to exiting a routine by signalling a condition. "Concrete dynamic" external specifications are expressed by "centry" and "cexit" specifications which are privileged to refer to the concrete structures of the abstract types to which the routine has composition access. These specifications are visible only to routines that also are permitted access to the concrete structures of the abstract types that can be used in the concrete specification. Special facilities are provided for stating dynamic external specifications for procedures manipulating buffers. Several standard functions are provided to record histories of transactions on buffers by processes. These functions may be used in entry and exit INTRODUCTION Page 1-10 1.1.3 Specifications specifications. Procedures that manipulate buffers, however, frequently are programmed intentionally never to terminate, making an exit specification of no practical value since it always is satisfied trivially. Dynamic external specifications for procedures, including non-terminating ones, that manipulate buffers can be expressed by a "block" specification and its concrete companion "cblock". The block specification is to hold whenever the routine is fully blocked awaiting access to a buffer. In effect, the block provides a temporary halting point similar to the final halting point of an exit specification. The block is also interpreted in a "weak" sense. It is to hold if the routine blocks; it does not specify that the routineM __ ___ must block.M____ Internal specifications of a routine can be stated in terms of "keep" and "assert" specifications. The internal specification may refer to local variables and constants in addition to formal parameters and global constants. Any number of assert specifications can be intermixed with the statements that implement the routine. Each assert is a relation that must hold whenever control reaches that point in the program. A routine may have only one keep specification; it appears immediately after the local declarations and must hold throughout the routine. The integration of specifications and programs into a single, unified language provides two complementary and powerful approaches to formal verification: formal proof and run-time validation. Formal proof methods exist for all of Gypsy, and a successful proof demonstrates that a specification always will be satisfied for all program executions. These proofs are performed by analyzing the program text and can be done prior to any actual program execution. However, they normally require substantial effort. An alternative approach to verification allowed for in Gypsy is the validation of specifications at run-time. Potentially any specification expression in the language may have a condition associated with it. If it does, the specification expression is evaluated at run-time; if it is false, its associated error condition is signalled. A recovery from this condition can be handled in the usual way by a when clause. Thus a specification can be verified either by proof or by run-time validation. A proof eliminates the run-time overhead of validation, and a validation eliminates the effort required to construct a proof. A specification expression also can simply be "assumed", that is, accepted without verification. An assumed specification therefore becomes a part of the "basis" of a verification. Assumed specification expressions normally are used to define functions that appear in other specification expressions and to describe relations among those functions. This provides an effective way of structuring specification expressions. A specification expression typically is written compactly in terms of functions. These functions then can be defined using assumed external specifications that refer to other functions. The presence of structure is just as important in specifications as it is in programs. Lemmas define a relationship that must hold among a number of functions. Lemmas are strictly specifications and are used only in proofs. They simply may be assumed as part of the basis of the INTRODUCTION Page 1-11 1.1.3 Specifications verification or they may be proved from the external specifications of the functions that appear in the lemma. A function that appears in a lemma may be granted access, through composition access lists, to the concrete structure of one or more abstract types. The concrete external specifications of the function may be used in proving the lemma iff the set of abstract types whose concrete structures are accessible to the function is a subset of the types whose concrete structures are accessible to the lemma. This provides a very simple mechanism for proving the algebraic axioms that are typically associated with data abstractions. The lemmas also can be used with functions not associated with data abstractions, in which case the lemma must be proved without reference to concrete external specifications. The lemma is also a well known mathematical concept that also provides a basis for structuring proofs. A data abstraction is defined when a composition access list appears in a type definition explicitly enumerating those units that are granted access to the concrete structure of the type. The specifications for data abstractions are stated in terms of an initial value, lemmas, and concrete invariants called "hold" specifications. The "initially" specification defines the default initial value of an abstract type. The lemmas define the algebraic properties of the abstract type. The hold specification must be satisfied by the concrete representation of an abstract object at all times except possibly during execution of the routines that are permitted concrete access to the abstract object. The hold must, therefore, be satisfied initially upon instantiation of the object and again upon completion of every routine that has access to its concrete structure. Each of the Gypsy specifications has a well-defined "extent". The extent of a specification identifies those program states on which a specification must be satisfied, thus identifying those potential places where a specification can be used in a proof. Each Gypsy specification has one of these kinds of extent: "instantaneous", "closed", and "open". An instantaneous specification (entry, centry, exit, cexit, block, cblock, assert, initially) must be satisfied on a particular instantaneous state. A closed specification (keep) must be satisfied throughout a sequence of states defined by a single routine activation. An open specification (lemma, hold) must be satisfied on all states except possibly those from a sequence of states defined by one or more routine activations. 1.2 PROGRAM DEVELOPMENT Gypsy is designed so that it can be used to describe a program throughout a complete development and maintenance cycle that includes formal specification and verification. In developing a program, it is desirable to be able to express the program description in various incomplete stages of development. Gypsy allows the keyword "pending" to appear many places in a program description for this purpose. Pending is simply a marker for text that is to be supplied in later stages of development. Gypsy has been defined to allow the option of developing and maintaining programs in a program description unit library. The library is an arbitrary collection of programM_______ INTRODUCTION Page 1-12 1.2 Program Development description units in various stages of development and may contain descriptions of one or more programs. Any given unit in the library may be referred to by any number of program descriptions. The library is maintained by a librarian that is responsible for the manipulationM _________ and processing units in the library, including adding new units and replacing pending parts of existing units. These manipulations are the responsibility of the librarian, not of the Gypsy language definition. The language definition defines the sets of program description units that are well-formed program descriptions. As a program is developed, its description units are stored in the library. Any number of language processors (parsers, verifiers, interpreters, compilers,...) can be provided by the librarian. The library also provides a central repository for the results of these processors to enable the librarian to analyze and respond to the effects of incremental program development. Gypsy is designed specifically to support independent processing of program description units, particularly independent verification and compilation of routines. The specification, programming, and verification methods are carefully balanced so that the construction of verification conditions for every routine requires reference to only the external specifications of only those routines that are referred to directly by the routine being verified. Routines can be compiled independently in the same way. 1.3 REPORT SUMMARY This report defines Version 2.0 of the language Gypsy. This language definition is a specification that must be satisfied by allM _____________ processors for the language (parsers, verification condition generators, compilers, ...). This report is a reference document and supercedes the previous report on Gypsy, Version 1.0. It is not intended as a tutorial and a thorough knowledge of programs and programming, as well as a basic understanding of formal specification and verification methods, is assumed. The definition of Gypsy is given in terms of syntax and semantics. A Gypsy program description is a sequence of tokens, and the syntax defines all those sequences that are sentences in the language. Each sentence is a program description. The definition of the Gypsy syntax is based on a context-free grammar. The semantics of the language define the run-time interpretation of each sentence in the language. Some of the semantics of Gypsy are expressed in English and large parts of the semantics are defined formally in the Gypsy specification language. The structure of the report largely parallels the structure of the Gypsy syntax. First, the report defines basic tokens of Gypsy sentences, then it follows essentially a top-down presentation of the syntax of program descriptions. This roughly parallels the way a program often would be written and helps to emphasize the overall structure and coherency of a complete program description. This approach does, however, lead to a substantial number of forward references. To minimize difficulties on a first reading, we suggest INTRODUCTION Page 1-13 1.3 Report Summary that the reader first read the introduction to each section, then preview the body of that section by reading the introductions to the next level of subsections. The rewrite rules and definitions of each section are numbered and cross referenced. The rule definitions are numbered locally within each section and again within each subsection. Thus, "[n]" refers to a definition rule within the most local subsection. References to rules and definitions outside of the most local subsection are expressed as "[m-n]", where "m" is a section number and "n" is the rule or definition number within that section (e.g, [2-1], [2.3-1]). References to an entire section (rather than just one particular rule) is written as [Section n] -- e.g., [Section 1.3]. 1.3.1 Syntax The Gypsy syntax is the complete set of rules that determine whether a given sequence of tokens is or is not a well-formed Gypsy program description. The well-formed sequences are the sentences ofM _________ the Gypsy language. More formally, the Gypsy syntax is a boolean-valued function, isgypsysentence(s), defined on sequences of tokens. A sequence s of tokens is a Gypsy sentence iff isgypsysentence(s). The complete Gypsy syntax is defined in terms of a context-free grammar and an additional set of contextual requirements that also must be met by sequences of tokens that satisfy the context-free grammar. The complete grammar, listed alphabetically by the left hand side of each rewrite rule, is given in Appendix A. This grammar is structured to provide an effective basis for explanation and understanding; it is not an SLR-1 grammar. The complete Gypsy syntax, however, also can be defined from an SLR-1 grammar that has been developed in parallel with the one given here. The context-free grammar is written in an extended form of conventional BNF rewrite rules. Nonterminal symbols are enclosed in angle brackets "<" and ">", "::=" is the rewrite operator, and "|" denotes alternate right hand sides. This conventional form also is extended to allow a right hand side to be described by an English phrase enclosed in "#" symbols or by a syntax chart. Each path through a chart defines a possible right hand side for a rewrite rule. The lines in the charts are traversed from left to right and top to bottom unless otherwise indicated. In describing the additional contextual requirements and the semantics of a token sequence, it is sometimes necessary to refer to different occurrences of the same nonterminal symbol . These occurrences are distinguished by the notation where n is a name for a particular occurrence of . The ",n" has no other significance. A context-free rewrite rule also may have associated with it a number of definitions, indicated by the word "Define", and contextual requirements, indicated by the word "Require", as in the following examples: 1. ::= INTRODUCTION Page 1-14 1.3.1 Syntax --- , <---------------------- | | v | --- cond ------------ ------------------ 1.1 Define. Each is a condition name.M ______ _________ ____ 2. ::= 2.1 Require. The must be a condition name.M _______ The definitions define terminology that is used in expressing contextual requirements and semantics. The right hand side of the rewrite rule also must satisfy all of the contextual requirements associated with that rule. 1.3.2 Semantics The semantics of Gypsy define the run-time interpretation of Gypsy sentences in terms of operations on objects. Gypsy specifications express constraints on the operations and objects; Gypsy programs express implementations of the operations and objects that meet these constraints. The semantics of the Gypsy specification language are expressed largely in English and some mathematical notation. The specification language is then used to define formally a large portion of the semantics of the programming language. A Gypsy program is semantically equivalent to a sequence of predefined and programmer-defined procedure and function calls that are embedded in various sequential and concurrent control statements. The mapping from token sequences into the equivalent predefined procedure and function calls is given as well as formal Gypsy specifications for all predefined procedures and functions. CHAPTER 2 LEXICAL STRUCTURE The Gypsy text which makes up a program description consists of a sequence of characters which are separated into a sequence of tokens. To aid in this separation, blanks, tab characters, end of line characters, etc. may be used. These characters have no effect on the semantics of the Gypsy program but only serve to delineate the tokens. Gypsy tokens are comprised of sequences of characters from the standard 7-bit ASCII character set. The set of tokens has been defined so that a Gypsy program may be written using a minimum subset of the ASCII character set. 1. ::= | | ( | ) | * | + | , | . | / | : | ; | - | < | = | > | $ 2. ::= | | " | ' | @ | [ | ] | _ | { | } | & 3. ::= | 4. ::= # any lower case ASCII letter a..z # 5. ::= # any upper case ASCII letter A..Z # 6. ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 7. ::= | | | | | 8. ::= ( | ) | * | + | , | . | - | / | : | ; | < | = | > | @ | [ | ] | & LEXICAL STRUCTURE Page 2-2 9. ::= .. | ** | := | -> | <: | :> 10. ::= adjoin | all | and | append | array | assert | assume | await | before | begin | behind | block | buffer | case | cblock | centry | cexit | cobegin | cond | const | difference | div | each | elif | else | end | entry | eq | exit | extends | fi | from | function | ge | give | gt | hold | if | iff | input | in | into | initially | intersect | is | keep | le | leave | lemma | loop | lt | mapomit | mapping | mod | move | name | ne | normal | not | of | omit | on | or | otherwise | output | pending | procedure | prove | receive | record | remove | scope | send | seq | seqomit | sequence | set | signal | some | sub | then | to | type | union | unless | var | when | with | 2.1 IDENTIFIERS s are used to name various objects in a program description. An is a sequence of s, s, and s. It must begin with a and must not end with a . There is no constraint on the number of characters making up an . 1. ::= -------------------------------------- | | v | ---> --------------------------> ---------> | | ^ | ^ ^ | |<----------| | | | | | | | | | | -- -- --- ---- | | | -------------------------------------------- 1.1 Require. The sequence of characters of an M _______ must not be the same as the sequence of characters in any . 2. ::= _ LEXICAL STRUCTURE Page 2-3 LITERAL CONSTANTS 2.2 LITERAL CONSTANTS The s are tokens that define constant values. 1. ::= | | 1.1 Define. The value of a is the valueM ______ _____ of its right hand side. 2.2.1 Characters A defines a value that is a character. 1. ::= 1.1 Define. The value of a is the . 2. ::= # any ASCII character # 3. ::= ' | $ 2.2.2 Strings A defines a value that is a sequence of characters. 1. ::= | 1.1 Define. The value of a is the value of itsM ______ _____ right hand side. 2. ::= --- --- | | v | ---- " ------------------------------- " ---- | ^ | | ------ "" ----- 2.1 Require. The must not be the quoteM _______ character ". 2.2 Define. The value of a is the sequence ofM ______ _____ s contained strictly within the opening and LEXICAL STRUCTURE Page 2-4 2.2.2 Strings closing quote character "; a double quote sequence, "", within the represents the single quote character ". 3. ::= --- --- | | v | --- ($ ------------------------------- $) --- | ^ | | ------ $$ ----- 3.1 Require. The must not be a $.M _______ 3.2 Define. The value of a is the sequenceM ______ _____ of the s contained strictly within the opening ($ and the closing $); a double $$ within the represents a single $ character. 2.2.3 Numbers A defines a value that is an integer. 1. ::= ------------------- | | v | ---------> ------------> 1.1 Define. The value of a is the integerM ______ _____ represented by its sequence of decimal s. 2.3 COMMENTS A Gypsy sentence may contain tokens. These tokens have no meaning and are ignored. 1. ::= | 2. ::= LEXICAL STRUCTURE Page 2-5 2.3 Comments --- --- | | v | ----> { -------------------------------> } ------> 2.1 Require. The must not be a }.M _______ 3. ::= --- --- | | ----> { -------------------------------> } ------> 3.1 Require. The sequence of s must notM _______ include the subsequence "*)". 2.4 UPPER/LOWER CASE CONVENTION Upper and lower case letters may be used interchangeably, except in literal constants. For example, all of the following are regarded as the same identifiers: "FIRSTNAME", "FirstName", "firstname"; and "BEGIN", "Begin", "begin" are all regarded as the same reserved word. This allows effective use of cases to enhance readability without causing excessive typographical errors. 2.5 BRACKETING CONVENTION Round brackets, "(" and ")", may be used pairwise interchangeably with square brackets, "[" and "]", except in literal constants. The forms "(...)" and "[...]" are equivalent so long as each bracketing pair is either round or square. Mismatched brackets, "[...)" orM ______ __ "(...]", are not allowed. This convention follows the similar one of mathematics. 2.6 PENDING The keyword "pending" appears at several places in the syntax. It is simply a marker that is to be replaced by a sequence of tokens at successive stages of developing the program description. CHAPTER 3 PROGRAM DESCRIPTIONS A program description is a set of program description unit declarations. The declarations of these units are grouped lexically into explicitly declared name scopes. Conceptually, these explicit scopes are contained within a predefined scope that contains the declarations of all predefined program description units. SyntaxM______ A is a sequence of explicit s, each of which may be preceded by a to restrict interscope referencing. 1. ::= ---- ; <------------------------------------------ | ^ v | --------------------------> ----------> | ^ | ^ | | | | - -- -- ; -- 1.1 Require. The scope name of each M _______ [Section 3.1-1.1] must be unique. 1.2 Define. A [Section 3.4-1] thatM ______ immediately precedes a scope S is the reference access listM _________ ______ ____ of S. 1.3 Require. If a reference access list immediately precedesM _______ a scope S, then only those scopes whose names are given in the reference access list may refer to S; otherwise, references to S are unrestricted. ExamplesM________ scope A ...; scope B ...; scope C ...; PROGRAM DESCRIPTIONS Page 3-2 scope D ...; s group together lexically sets of declarations of program description units and provide local names for these units. Potentially, any unit in one scope can name and refer to a unit in any other scope through a name declaration [Section 3.3]. The that may precede a limits access to that scope. The access list acts as a gate limiting access to only those scopes given in the list. If there is no gate, access to the scope is unrestricted. The access lists can be used to define an accessing hierarchy if desired, as in the example above. The scope hierarchy of this example is A | ------------- B C | D References to scope A are unrestricted. Scopes B and D may be referenced only internally. Scope C may be referred to internally and by D. Other kinds of referencing control also can be defined. For example, D can be added to the access list of scope B -- i.e., scope B ..., giving a referencing structure that is a graph rather than a tree. SemanticsM_________ The semantics of a are strictly the semantics of its individual units. 3.1 SCOPE DECLARATIONS A scope declaration groups together a set of program description unit declarations. Each unit declared has a local name within the scope in which it appears and a corresponding global name that is unique over all scope declarations. A name declaration allows references to units declared in any arbitrary scope. SyntaxM______ A consists of a and a . The defines the name of the scope and the contains the units and name declarations, and defines the local names associated with the scope. 1. ::= = 1.1 Define. The scope name of a is theM ______ _____ ____ in its . This is the PROGRAM DESCRIPTIONS Page 3-3 3.1 Scope Declarations defining occurrence of the scope name; it is not a referenceM ________ ___ to the scope name. Therefore, this occurrence of the is not considered in determining whether the referencing restrictions imposed by reference access lists are satisfied. 1.2 Define. A defines a new name scopeM ______ whose local names are the scope name [1.1] and the localM _____ _____ names defined by its . 2. ::= scope 3. ::= ----- ; <----------------------------------------- | | v | begin -------------------------> ------------ end -> | ^ ^ | ^ | | | | | |- - | -- ; -- | | --------------- ------------ 3.1 Define. The local names of a are the localM ______ _____ _____ names of all s [Section 3.2] and the local names of all s [Section 3.3]. 3.2 Define. The global name corresponding to a local name LM ______ ______ ____ of a is "L from S" where S is the name of the scope in which the appears. The global names corresponding to the local names of s are defined by the . 3.3 Define. A [Section 3.4-2] whichM ______ immediately precedes a unit U is the reference access list ofM _________ ______ ____ U. 3.4 Define. Any local name that appears in an or a is a pseudonym for itsM _________ corresponding global name [3.2]. 3.5 Require. If a unit U is preceded by a reference accessM _______ list, references to U are restricted; otherwise, references to U are unrestricted. If the reference access list contains a scope (unit) name, only those scopes (units) explicitly named in the list may refer to unit U. (Note: A scope may refer to a unit only through a [Section 3.3]. Local unit names that appear in the reference access list are pseudonyms for their global names [3.2].) 4. ::= 4.1 Require. The must be a scope name.M _______ PROGRAM DESCRIPTIONS Page 3-4 3.1 Scope Declarations ExamplesM________ scope A = begin type t ...; procedure p ...; function f ...; const c ...; lemma l ...; name n ...; end; Type "t" can be referred to only by function "f", lemma "l", and the unit named "n". "N" is declared in a name declaration to be a local pseudonym for a unit in some scope. The only scope that can refer (in a name declaration) to procedure "p" is scope "B". Thus, "p" can be referred to only by units in scopes "A" and "B". SemanticsM_________ The semantics of a are strictly the semantics of the units declared within it. 3.2 UNIT DECLARATIONS A unit declaration is the declaration of a function, procedure, lemma, type, or constant unit. SyntaxM______ Each declares the existence of a particular kind of unit and defines a local name for the unit. 1. ::= | | | 1.1 Define. The unit name of is eitherM ______ ____ ____ the routine name, lemma name, type name or constant name, depending on the right side of the . The unit name is the defining occurrence of the unit name; it is not a reference to the unit and therefore is not considered in determining if restrictions imposed by reference access lists are satisfied. 1.2 Define. A defines a new unit nameM ______ ____ ____ scope.M _____ 1.3 Define. The unit name is a local name of the unit nameM ______ _____ ____ scope defined by the unit. PROGRAM DESCRIPTIONS Page 3-5 3.2 Unit Declarations 2. ::= 2.1 Require. The must be a unit name.M _______ SemanticsM_________ The semantics of a are the semantics of its right side. 3.3 NAME DECLARATIONS A name declaration defines a local pseudonym for a unit declared in some arbitrary scope. SyntaxM______ A single may define any number of local names and their corresponding global names. All names defined by a given refer to units declared in the same scope. 1. ::= ---------------- , ----------------- | | v | name ------------------------ --------> from | ^ | | --- = --- 1.1 Require. The must be a local unit name withinM _______ the scope named . 1.2 Define. A local name is defined by the for each iteration through the form = . The local name is and its corresponding global name is " from ". If does not appear, the is the local name. ExamplesM________ name x = y from s; name z from s; The first example defines a local name "x" that is a pseudonym for "y from s". The second example defines a local name "z" that is a pseudonym for "z from s". PROGRAM DESCRIPTIONS Page 3-6 3.3 Name Declarations SemanticsM_________ A has no semantic effect. Its only effect is to define a local name that refers to some unit in some scope. 3.4 ACCESS LISTS Access lists may appear in various places within a program description. When they appear, they restrict access to a segment of the program that immediately follows them. If a segment is not preceded by an access list, access to the segment is unrestricted. An access list behaves like a gate. If a segment is protected by a gate, only those parts of the program whose names appear in the gate may refer to the segment protected by the gate. SyntaxM______ An access list is a list of s and s enclosed in angle brackets. 1. ::= ------- , ------- | | v | --- < ---- ---- > --- 2. ::= ------- , ------- | | v | --- < ---- ---- > --- | ^ | | - -- SemanticsM_________ An access list has no run-time interpretation; its restrictions are enforced syntactically. 3.5 NAME SCOPES A program description involves three distinct levels of name scopes. The outermost level is the predefined scope which contains the program description units that are predefined by the language. Each explicit scope declaration of a program description defines a name scope that is contained within the predefined scope, and each unit declaration defines a name scope that is contained within the PROGRAM DESCRIPTIONS Page 3-7 3.5 Name Scopes explicit scope in which it appears. This name scope structure is a three level hierarchy as shown below. -------------------------------------- | Predefined Scope | ... | | ---------------------------------- | | Scope Declaration | | | | ... | | | | ------------------------------ | | | Unit Declaration | | | | | | | | | | | ------------------------------ | | | | ... | | | ---------------------------------- | | ... | -------------------------------------- The names defined within a given name scope S are the following: 1. The names of all predefined units. The predefined units are named by the predefined identifiers [Appendix D]. 2. The names referred to by S that are local names of some name scope containing S. 3. The local names of S. All names defined within every name scope must be unique. The predefined units are defined in every scope and always name the predefined units; the predefined names may not be redefined. 3.6 IMPLEMENTATION DEFINED UNITS A particular implementation of Gypsy may introduce any number of implementation defined units into the predefined scope subject only to the constraint that the names of these units not conflict with the standard predefined identifiers. These units can be used to provide any type of implementation dependent feature that can be described as a Gypsy program description unit. Typical examples would be input and output facilities and special machine instructions that may not ordinarily be generated by a compiler. PROGRAM DESCRIPTIONS Page 3-8 UNIT INDEPENDENCE 3.7 UNIT INDEPENDENCE The program description units are defined so that the verification of a unit is independent of the verification of any other unit. The units that are potential candidates for verification are the routines [Section 4.0], lemmas [Section 6.0], and abstract types [Section 7.4]. The declarations of each of these potentially verifiable units define the specifications and the implementation of the units. In general, there are two kinds of specifications for these units, external and internal. The external specifications of a unit are accessible to other units, whereas its internal specifications are not. All Gypsy units are designed so that the verification of a unit U depends on the specifications and implementation of U and on only the external specifications of theM ____ units referred to by U. The verification of U does not depend on theM ___ implementation or the verification of the units referred to by U. The consistency demonstrated by the verification of U is, of course, contingent upon the assumption that the units referred to by U are consistent with their external specifications and this consistency eventually must be verified; the verifications of U and the units referred to by U do not interact. This independence of theM ___ verifications is preserved even in the presence of concurrency and permits verification of units to be done in any desired order. Thus, verification can be done step-by-step in parallel with any effective program development strategy, including a purely top-down strategy, if desired. This degree of independence also enhances independent compilation of routines. If a routine R is being compiled and refers to (calls) a routine S,then only the static external specifications (the header) of S are needed in compiling R. CHAPTER 4 ROUTINE DECLARATIONS Operations in Gypsy are performed by activations of routines. These activations are initiated by routine calls. A routine call supplies the operands, the actual parameters of the operation, and initiates an activation of a routine on those operands. The routine refers to the actual parameters through its corresponding formal parameters. These actual parameters are the only objects in the external environment of the routine to which it may refer except for globally defined units. The parameters of a routine completely define its data interface with its external environment (except possibly for global constants). The specifications and the implementation of the routine are distributed throughout the routine declaration. A routine may have both external and internal specifications of several different kinds. A routine declaration also may or may not contain an implementation for the routine. The implementation of a routine defines how it is decomposed into other operations; therefore, routines are a mechanism for operational abstraction. A routine declaration need not contain an implementation. These declarations may be used to describe operations used strictly in specifications. SyntaxM______ A consists of a and a . 1. ::= --- = --- --- | | ---- ----- 1.1 Define. The routine name of the isM ______ _______ ____ the in either the or the of the . 1.2 Define. The is the static externalM ______ ______ ________ specification of the routine named in the . 1.3 Define. The dynamic external specifications of theM ______ _______ ________ ______________ ROUTINE DECLARATIONS Page 4-2 routine named in the are the s of the . 1.4 Define. The internal specifications of the routine namedM ______ ________ ______________ in the are the internal specifications of the . 1.5 Define. The implementation of the routine named in theM ______ ______________ is the implementation defined in the , if any. If the defines an implementation, then the is also a part of the implementation of the routine as well as being its static external specification. 2. ::= | ExamplesM________ function Ordered(a: smallarray) : boolean = begin exit (assume all x, y:bounds, x < y -> a[x] < a[y]); end; function AMAX(a:smallarray; i,j:smallint): integer = begin entry i le j; exit all k:smallint, a[k] ge a[result]; var l:smallint := i + 1; result := a[i]; loop if l > j then leave elif a[l] > a[result] then result := l end; l := l+1; end; end; procedure Network(var Net_port:Internal_port_array) = begin block all u_id1,u_id2:User_id, proper_delivery(net_port, u_id1, u_id2, myid); exit false; end; SemanticsM_________ A defines the specifications and the implementation of the routine named in the declaration. The defines the static external specifications of the routine and is also considered as part of the implementation of the routine if the defines an implementation. The may also define additional specifications. ROUTINE DECLARATIONS Page 4-3 The static external specification of a routine defines the name of the routine and its formal parameters. When a routine is activated by a routine call, its formal parameters refer to parts of the external environment of the routine. These formal parameters specify the interface between the routine and its external environment. A routine may refer only to those parts of its external environment that are referred to by its formal parameters and to the globally defined units. (Nonlocal references to variables are not allowed.) The formal parameters may name either data objects or exception conditions. The ones that name data objects also specify a type [Section 7.0] for the object. The type defines a set of constraints on the object referred to by the formal parameter that must be satisfied throughout any activation of the routine. A routine call [Section 8.0] causes the activation of a routine on a sequence of actual parameters. Each actual parameter is the name of some data object or exception condition in the environment of the routine call. When a routine is activated, the actual parameters are passed by reference. The formal parameters are bound to the actual parameters so that the formals are interpreted as pseudonyms for the names of the corresponding actuals. The activation of the calling routine is then suspended, and the newly initiated routine is activated with respect to its formal parameters. Activation of the calling routine resumes when the activation of the newly initiated routine terminates, if it does. 3. Define. The activation of a routine terminates normally iffM ______ __________ ________ it terminates without signalling a condition. 4. Define. The activation of a routine terminates abnormallyM ______ __________ __________ iff it terminates signalling an exception condition. A routine that is activated by a routine call may or may not have an implementation. If it does have an implementation, the activation of the routine is the activation defined by its implementation with respect to its formal parameters. A routine without an implementation may be used only for expressing specifications; it may not actually be activated at run-time. These routines are used only to postulate the existence of certain routines with the prescribed set of properties expressed by their specifications. 4.1 PROCEDURE HEADER A procedure header gives a name to a procedure and defines its formal parameters. SyntaxM______ A consists of an that names the procedure, , and optional . ROUTINE DECLARATIONS Page 4-4 4.1 Procedure Header 1. ::= ----- procedure ---- | -- -- | | |-- -- | | |<----------------------------- | 1.1 Define. The formal parameter "const myid: activationid"M ______ is an implicit parameter to every .M ________ _________ "Myid" is the activation name of the procedure and is a localM __________ ____ name of the unit name scope. 2. ::= 2.1 Require. The must name a procedure.M _______ ExamplesM________ procedure Insert (id: key; var tbl: symtab) unless (cond tablefull, duplicate) procedure Delete(var r:register; i:int) procedure Tipcount(var num:int; b_tree:binarytree) unless (cond bigtree) SemanticsM_________ The defines the formal data parameters [Section 4.3] and condition parameters [Section 4.4] of the procedure. The formal data parameters are defined by and the condition parameters by . The effects of a procedure on the data objects of its external environment are strictly confined to the actual parameters that correspond to its formal var parameters. The activation name "myid" is a unique name that is assigned to each activation of the procedure. "Myid" is needed only to distinguish various activations of the procedure that may be executing concurrently. "Myid" is useful only in specifications and proof. ROUTINE DECLARATIONS Page 4-5 FUNCTION HEADER 4.2 FUNCTION HEADER A function header gives a name to the function, defines its formal parameters, and defines the type of result it will return. SyntaxM______ A consists of an that names the function, an optional that defines an equality extension, optional , a that defines the type of result returned by the function, and optional . 1. ::= ----- function ------ | ---------------------------------- | |---- extends ---------- | | |<------------------------------- | |-- -- | | |<------------------------------- | ----- : -------------- | --------------------------------- | |--- --- | | |<------------------------------- | 1.1 Require. If the is present, then the stringM _______ must be "=". 1.2 Define. The phrase "extends " is an equalityM ______ ________ extension.M _________ 1.3 Require. If the has an equalityM _______ extension, then the header must be equivalent to the form function extends "=" (, : A) : boolean where A is an abstract type [Section 7.4]. (The may not have .) 1.5 Require. There may be at most one equality extension forM _______ a given abstract type A. ROUTINE DECLARATIONS Page 4-6 4.2 Function Header 1.6 Define. The formal parameter "var result: "M ______ is an implicit parameter to every .M ________ _________ "Result" is a local name of the unit name scope. 1.7 Require. The must not define an activationidM _______ type at any level. 2. ::= 2.1 Require. The must name a function.M _______ ExamplesM________ function Message_Eq extends "=" (msg1,msg2:message):boolean function Count_Tips (t: binarytree): integer unless (cond overflow) SemanticsM_________ The defines the formal data parameters [Section 4.3] and condition parameters [Section 4.4] of the function. The formal data parameters are defined by the and the formal condition parameters by the . A function may not have var parameters (except for "result") and, therefore, cannot cause a side effect on any of its data parameters. The implicit var parameter "result" defines the result returned by the function. Within the it is treated in the same way as a normal var parameter, except that it is given the default initial value of the whenever the function is activated. Functions, therefore, always return a well-defined value. The are optional. If they are not present the function has no parameters and, in effect, defines a constant. Parameterless functions may be used to define constants of abstract types. The operator extension is used only in conjunction with abstract types [Section 7.4]. 4.3 FORMAL DATA PARAMETERS The formal data parameters of a routine name the data objects of the external environment that may be referred to by a routine. Constraints on the manipulations of these objects are defined by the types of the formal parameters. SyntaxM______ Formal data parameters may be either or . ROUTINE DECLARATIONS Page 4-7 4.3 Formal Data Parameters 1. ::= -- ; <------------------------------------------- | | | -- , <------------ | | | | | v v | | --- ( ---------------- --- : --- ) --- | ^ |- const ->| | | |- var --->| 1.1 Define. Every is a local name of the unitM ______ _____ ____ name scope. 1.2 Define. An that is not preceded by theM ______ keyword "var" is a formal const parameter and defines aM ______ _____ _________ constant name.M ________ ____ 1.3 Define. An that is preceded by "var" is aM ______ formal var parameter and defines a variable name.M ______ ___ _________ ________ ____ 1.4 Require. Any that appears in a M _______ must evaluate statically to a constant. 1.5 Define. The type of the constant or variable identifiedM ______ ____ by the is defined by the that follows it. 2. ::= -- ; <------------------------------------------- | | | -- , <------------ | | | | | v v | | --- ( ---------------- --- : ----- ) --- | ^ -- const --- 2.1 Define. Every is a local name of the unitM ______ _____ ____ name scope. 2.2 Define. Every is a formal const parameterM ______ ______ _____ _________ and defines a constant name.M ________ ____ 2.3 Require. Any that appears in the M _______ must evaluate statically to a constant. 2.4 Define. The type of the constant or variable identifiedM ______ ____ by the is defined by the that follows it. ROUTINE DECLARATIONS Page 4-8 4.3 Formal Data Parameters 3. ::= 3.1 Require. The must name a variable. (TheM _______ variable may be a formal var parameter or a local variable [Section 4.7-2].) 4. ::= 4.1 Require. The must name a constant. (TheM _______ constant may be a formal const parameter, a local constant, or a global constant [Section 5.0].) SemanticsM_________ Every formal parameter is a name that identifies a data object that is either a constant or a variable. The actual object that is referred to is the object referred to by the corresponding actual parameter. The that follows the formal parameter defines a type [Section 7.0]. All manipulations of the formal parameter by the routine must satisfy the constraints of the formal parameter type. Const parameters are not allowed to appear as actual var parameters in routine calls. Therefore, the value of a const parameter cannot be changed by a routine. The values of var parameters may be changed. Functions are not permitted to have var parameters (except for the implicit parameter "result") so that the values of the function data parameters cannot be changed as a consequence of activating the function. 4.4 FORMAL CONDITION PARAMETERS The formal condition parameters define the exception conditions that may be signalled from a routine to its calling environment. SyntaxM______ The s are a sequence of s. 1. ::= --- , <------------ | | v | ---- unless -- ( ---------------- ---- ) ----- | ^ | | --- cond --- 1.1 Define. Every is a local name of the unitM ______ _____ ____ name scope. ROUTINE DECLARATIONS Page 4-9 4.4 Formal Condition Parameters 1.2 Define. Each is a formal conditionM ______ ______ _________ parameter and defines a condition name.M _________ _________ ____ 2. ::= 2.1 Require. The must name a condition. (TheM _______ condition may be a formal condition parameter or a local condition [Section 4.7-3].) ExamplesM________ function Retrieve (s:symtab; id:identifier) : attributelist unless (cond Undefined_Id) = pending; procedure Get_Next(var q:priority_queue; var e:single_element) unless (cond empty_queue) = pending SemanticsM_________ Formal conditions are exception conditions which can be signalled to the external environment. The activation of a routine may terminate abnormally by signalling either a formal condition or a "routineerror". The calling environment can detect no conditions signalled within this routine other than "routineerror" or actual condition parameters that correspond to formal condition parameters. (See [Section 10.5]) 4.5 ROUTINE BODY The routine body defines the implementation of a routine, its dynamic external specifications, and its internal specifications. SyntaxM______ A consists of , s, a keep specification, a , and an . Each of these is optional except the . 1. ::= ROUTINE DECLARATIONS Page 4-10 4.5 Routine Body -- begin -- | |-- -- | | |<-------------------------------------- | |<------------------------------ | | |---- ; ---- | |-- keep ; -- | | |<--------------------------------------- | |--- --- | |<----------------------- | ---------- 1.1 Require. The may referM _______ only to formal parameters and globally defined units. 1.2 Define. The keep specification is the that follows "keep". 1.3 Require. All references to objects in the keepM _______ specification, statement list, and end clause must be to either objects declared in the formal parameters, local declarations or globally defined units. 1.4 Define. The internal specifications of the routineM ______ ________ ______________ consist of the keep specification and the internal specifications of the . 1.5 Define. The implementation of the routine is defined byM ______ ______________ the s and the . SemanticsM_________ The dynamic external specifications define the effects of the routine on its parameters. (This includes the "result" value of a function.) Local declarations create data objects only within the extent of a given activation of the routine. The declarations also may declare local conditions. When a routine is activated, the is executed with respect to the formal parameters. First, the data objects declared by the local declarations are instantiated (created and initialized), then the statement list is executed. If the execution of the terminates, the local data objects are destroyed and control returns to the calling environment. ROUTINE DECLARATIONS Page 4-11 DYNAMIC EXTERNAL SPECIFICATIONS 4.6 DYNAMIC EXTERNAL SPECIFICATIONS Dynamic external specifications define the effects of the routine on its parameters. This includes assigning values to var parameters and function results and signalling condition parameters. SyntaxM______ The are composed of and . 1. ::= | |--- ---- | |<------------------------------------------ | |--- ---- | |<------------------------------------------ | 1.1 Require. The may notM _______ refer to the concrete representation of any abstract type [Section 7.4]. 2. ::= | |-- entry -- -- ; -- | | |<--------------------------------------------- | |-- block -- -- ; --- | | |<--------------------------------------------- | |-- exit -- -- ; --- | | ^ | | -------- ---------- | | | |<--------------------------------------------- | 2.1 Define. The that followsM ______ "entry" is the abstract entry specification.M ________ _____ _____________ 2.2 Define. The that followsM ______ "block" is the abstract block specification.M ________ _____ _____________ 2.3 Define. The or M ______ that follows "exit" is the abstract exit specification.M ________ ____ _____________ ROUTINE DECLARATIONS Page 4-12 4.6 Dynamic External Specifications 3. ::= | |- centry -- -- ; -- | | |<--------------------------------------------- | |- cblock -- -- ; --- | | |<--------------------------------------------- | |- cexit -- -- ; --- | | ^ | | | | | | --------- ---------- | | | |<--------------------------------------------- | 3.1 Require. The that followsM _______ "centry" is the concrete entry specification.M ________ _____ _____________ 3.2 Require. The that followsM _______ "cblock" is the concrete block specification.M ________ _____ _____________ 3.3 Require. The or M _______ that follows "cexit" is the concrete exit specification.M ________ ____ _____________ 4. ::= ----- ; <--------------------------------------------------- | | | --- , <----------- | | | | | v v | | case ( -- is ---- ---- : -- --- ) | ^ | | ----- normal : ----- ----- 4.1 Require. Every must be unique.M _______ SemanticsM_________ The are external specifications of instantaneous extent. The of a routine R may not refer to the concrete representation of its parameters; therefore, they are accessible in proving any unit that may refer to routine R. The of R may refer to the concrete representation of the abstract types to which R has composition access [Section 7.3-2.2]. If R has composition access to abstract type T1,...Tn, the of R are accessible in proving only those units which ROUTINE DECLARATIONS Page 4-13 4.6 Dynamic External Specifications refer to R and which have composition access to at least T1,...Tn. This restriction prevents the proof of a unit from depending on the concrete specification of a type unless that unit has composition access to that type. This independence is just as necessary in proofs as it is in implementations. An entry specification is a relation that is assumed to be true whenever a routine is activated. The routine may be implemented and verified based on this assumption. If a routine has both an abstract and a concrete entry, the abstract entry must logically imply the concrete one. An entry specification may be either proved or validated at run time as directed in its [Section 9.1]. If it is to be proved, it must be proved at the call site of every call of its routine. If the calling routine has composition access to all abstract types that the called routine does, it is sufficient to prove the concrete entry of the called routine if it has one; otherwise, the abstract entry must be proved. If the entry is validated at run time [Section 9.1], first the abstract and then the concrete entry is validated upon activation. The failure of this validation may signal a formal condition parameter. This condition is signalled outside the scope of the of the and therefore can be handled only in the calling environment. A block specification must hold if the routine is blocked. AnM __ activation of a routine is blocked if its execution is completely suspended awaiting access to buffers shared with activations of other routines. 5. Define. An activation of a routine is blocked iff itsM ______ _______ is blocked. The blockage of a is defined in terms of the blockage of its individual s. In essence, a blockage point is a temporary termination point at which specifications can be stated for non-terminating processes. If a routine has both an abstract and a concrete block specification, the concrete block must imply the abstract one. An exit specification holds if the activation of the routineM __ terminates. An exit specification may follow either of two forms. It may be a or it may be an . The form describes a relation that must hold whenever the routine terminates normally. The describes relations that are to hold under either normal or abnormal terminations. The normal case is identified by the keyword "normal"; the relations that hold under abnormal termination are identified by the s that precede them. If a routine has both an abstract and a concrete exit for a particular case, the concrete exit must logically imply the corresponding abstract one. The normal concrete exit must imply the normal abstract exit and the concrete exit on condition c must imply the abstract exit on condition c. Only a normal exit specification can be validated at run time. If an entry specification is validated at run time, its logical negation is implicitly conjoined to the part of the exit case that ROUTINE DECLARATIONS Page 4-14 4.6 Dynamic External Specifications corresponds to the condition it signals. 4.7 LOCAL DECLARATIONS The local declarations define data objects that are strictly local to each activation of a routine. They also define local conditions. SyntaxM______ A may be a , a , or a . 1. ::= | | 2. ::= -- , <----------- | | v | var --- --- : ----------------------------- | | ^ | | | | -- := ----->| | | | | --- pending ---->| | | ------- := ---------------- 2.1 Define. Every is a local name of the unitM ______ _____ ____ name scope. 2.2 Define. Every is a local variable andM ______ _____ ________ defines a variable name.M ________ ____ 2.3 Define. The , if present, is the initialM ______ _______ value expression.M _____ __________ 2.4 Define. The type of the local variable identified by anM ______ ____ is the type defined by its succeeding , if there is one; otherwise, it is the type of the succeeding initial value expression. 2.5 Require. If the is followed by an initialM _______ value expression, the value of the must be potentially an element of the type defined by the [Section 7.1-1]. 2.6 Require. If the has an initial valueM _______ expression, there must be an assignment procedure defined on ROUTINE DECLARATIONS Page 4-15 4.7 Local Declarations the type of the . 2.7 Require. The must not define an activationidM _______ type at any level. 3. ::= --- , <---------------------- | | v | --- cond ------------ ------------------ 3.1 Require. Every is a local name of the unitM _______ _____ ____ name scope. SemanticsM_________ The execution of a or a causes the instantiation of a data object. A data object is instantiated by creating a new object and assigning an initial value to it. The instantiation of constants is described in Section 5.0. The variables named in a new are instantiated by creating new objects that are identified by the corresponding s and assigning to them the value of the initial value expression (if there is one). If the value of is not an element of the type defined by the a "valueerror" is signalled and control is immediately transferred to handle the error. If there is no initial value expression, the variables are initialized to the default initial value defined by the [Section 7.6]. A has no semantic effect. It simply defines s that can be used syntactically within the routine. 4.8 INTERNAL SPECIFICATIONS The internal specifications of a routine describe relations that must hold at various points in the execution of the routine statement list. Internal specifications are completely local to the routine declaration and cannot be used outside the routine. Keep specifications [Section 4.5-1.3] are internal specifications of closed extent. The keep assertion should remain true at all times during execution of a routine, except during execution of internally called routines. This form of internal assertion is an abbreviation indicating that the statement assert is implicitly present before the first statement of the routine's , and also after every in the . If the keep specification is to be run time validated, the ROUTINE DECLARATIONS Page 4-16 4.8 Internal Specifications normal rules for run time validating the (implicit) assert statements apply. Internal specifications arising from the are in the form of assertions which must be true at specific points. They are described in Section 10.0. CHAPTER 5 CONSTANT DECLARATIONS A constant declaration defines a constant. A constant is a data object whose value remains unchanged. Constant declarations may appear as unit declarations defining global constants, and they may appear within routine declarations. SyntaxM______ A consists of an that identifies the constant, and an that defines its value. The may be left "pending", in which case a is required to define the type of the constant. 1. ::= --- const -- --- : = --- --- | | ^ | | | | --- pending ---->| | | -------- = ------------- 1.1 Define. The constant name of a isM ______ ________ ____ the . 1.2 Define. If the appears as a , it defines a global constant.M ______ ________ 1.3 Define. If the appears within aM ______ , it defines a local constant.M _____ ________ 1.4 Require. If the defines a globalM _______ constant, the in the and any that appears in the must evaluate statically to a constant value. 1.5 Require. If the defines a globalM _______ constant and an follows the , then the value of the must be an element of the type defined by the [Section 7.1-1]. 1.6 Require. If the defines a localM _______ CONSTANT DECLARATIONS Page 5-2 constant and an follows the , the type of the must be compatible with the type T defined by the and the value of the expression must potentially be an element of type T. 1.7 Define. The type of the constant named isM ______ ____ the type of the if there is one; otherwise, it is the type of the . 1.8 Require. The must not define an abstractM _______ type. ExamplesM________ const m = 0 const n: integer = 4 const small: (1..n) = pending SemanticsM_________ A instantiates a data object. An object named is created and initialized to the value of the that appears in the . This value is fixed throughout the extent of the constant. 2. Define. The value of a constant is the value of theM ______ _____ in the . The declaration of a local constant creates a new data object. Both the type defined by the and the value of the in the may vary from one activation of a routine to the next. If the declaration has both a and an , the value of the must be an element of the type defined by the at the time the new constant object is created in the program state; otherwise, a "valueerror" is signalled. CHAPTER 6 LEMMA DECLARATIONS A lemma declaration defines a relation among a number of functions and globally defined constants. Lemmas are used only to express external specifications. Lemma units actually are used and referred to only in proofs; the only place a lemma name can appear in a program description, other than in its own definition, is in an access list. SyntaxM______ A consists of a and a . 1. ::= = 1.1 Define. The lemma name of a is theM ______ _____ ____ in the . 2. ::= lemma ----------------------------------------> | ^ | | --- --- 2.1 Define. The is a local name of the unitM ______ _____ ____ name scope. 2.2 Define. Each formal parameter of the is a local name of the unit name scope.M _____ ____ 3. ::= 3.1 Require. The [Section 9.1-2]M _______ may not refer to the concrete structure of any abstract type,M ___ even if the lemma name appears in the composition access list of the abstract type. LEMMA DECLARATIONS Page 6-2 ExamplesM________ lemma positiven = n > 0 {Note: n must be a global constant.} lemma popofpush(s:stack; x:integer) = pop(push(s,x)) = s SemanticsM_________ A defines a relation among a set of functions and global constants. The relation that is to hold is defined by the . The that is the is to hold for all values of the formal parameters such that (i) the entry specifications of all functions in the are satisfied, and (ii) all functions in the terminate normally. For example, if the entry specifications of push and pop in the preceding example are function push(s:stack, e:element):stack = begin entry not isfull(s); end; function pop(s:stack):stack = begin entry not isempty(s); end; then the relation defined by the "popofpush" example lemma is not isfull(s) and not isempty(push(s,x)) -> pop(push(s,x)) = s A lemma specification has an open extent. It holds everywhere except possibly during activations of functions in the . Lemmas may be used to express algebraic specifications of abstract types [Section 7.4] or relations among any other set of functions. If a lemma has a reference access list [Section 3.1-3.3], the lemma may be used only in proofs of units allowed by the access list. Lemmas also may be used quite effectively to decompose proofs into well-structured and manageable steps. Lemmas are proved from the external specifications of the functions in the . If a lemma name L appears in an access list <...,L,...>, then the proof of lemma L, rather than the lemma itself, may refer to theM_____ information that is protected by the access list. If the access list is a reference access list [Section 3.1-3.3], then the proof of L may use the program description unit that immediately follows the access LEMMA DECLARATIONS Page 6-3 list. If the access list is a composition access list [Section 7.3-2.1] of an abstract type A, then the proof of L potentially may use the concrete structure of type A. Suppose L has composition access [Section 7.3-2.3] to abstract types {A1,...,An}. The proof of L may use the concrete external specifications of a function F only if F has composition access to no abstract types other than those in {A1,...An}. The set {A1,...,An} defines the maximal set of concrete structures upon which the proof of L may depend. CHAPTER 7 TYPES Every data object in Gypsy has a type that describes a set of constraints on that object. The type of an object defines the set of values that may be referred to by an object, defines a default initial value for the object, and may also limit the set of operations that can be performed on the object. The value set of a type may be determined dynamically; all other aspects of a type are determined statically. The primary purpose of types is to provide a means of checking the consistency of actual and formal parameters of routine calls. Gypsy has three kinds of types: simple types, structured types, and special types which support concurrency. The simple types are the scalar types, the predefined types "integer" and "rational", and the subrange types. Types "character" and "boolean" are predefined scalar types. Each of these types has a value set. The subrange types are simple types whose value sets are subsets of other simple types. A structured type defines an object that has component objects. A structured type defines the type of each component and possibly additional constraints on the value set of the structured type. A structured type may be either static or dynamic. The number of components of an object of a dynamic type may vary at run time; the number of components of an object of a static type may not. The static types are "records" and "arrays". The dynamic types are "sets", "sequences", and "mappings". The types of the components of a record may be different; components of all other structured types must be the same. The special types to support concurrency are "buffers" and "activationids". A buffer is also a dynamic structured type. Buffers are unique in that they provide the sole mechanism for synchronizing systems of concurrent processes. Buffers also are the only types upon which operation restrictions can be defined. The activationid type is required in specification and verification to identify different concurrent activations of the same routine. Activationids are useful only in these contexts. Any of these types can be used to form the concrete representation of an abstract type. The concrete representation is encapsulated by using a composition access list. Only those units that are named by the access list are granted knowledge of the concrete representation. TYPES Page 7-2 THE CONCEPT OF TYPE 7.1 THE CONCEPT OF TYPE The data objects of Gypsy programs are referred to by constants and variables. Every data object has a name, a type, and refers to a value. The name of an object uniquely identifies the object and the type describes a set of constraints on the object. The type of an object consists of a value set and a default initial value. Buffer types also have an allowed operation set. We shall use the notation values#(T), initial#(T), and allowedops#(T), respectively, to denote the value set, the default initial value, and the allowed operation set of type T. (The "#" is used to signify and emphasize that these functions are not ones that can be written in a Gypsy program description; "#" is not allowed in s.) Values#(T) delimits the values that may be referred to by an object of type T. 1. Define. A value is an element of a type T iff the value isM ______ _______ an element of values#(T). Every value referred to by an object of type T must be an element of type T. Initial#(T) defines the default initial value of objects of type T. Objects are created (allocated) and destroyed (deallocated). Object are created and initialized to refer to some initial value by a process called instantiation. The default initial value of a type defines the value to which an object is initialized if no other initial value is given at the instantiation site. For a buffer type B, allowedops#(B) may limit the predefined buffer routines in which objects of type B may be used as an actual parameter. This allows the definition of buffer types which specify that the buffer be used strictly as an input or output buffer. These limitations on buffer operations can be used to simplify many aspects of the specification and verification of concurrent systems. 7.2 TYPE CONSISTENCY Types in Gypsy provide the means of checking the consistency of actual and formal parameters of routine calls. The type consistency rules are defined so that every routine can be analyzed completely with respect to the types of its formal parameters, and specifically without reference to any of its actual parameters. The typeM_______ consistency rules ensure that the actual parameters satisfy the constraints expressed by the corresponding formal parameters, and thus, they ensure that the actual parameters satisfy the assumptions of the analysis of the routine. The type consistency requirements for actual and formal parameters are very simple: 1. Require. The value of every actual parameter must be anM _______ element of the type of the corresponding formal parameter whenever the routine is called. TYPES Page 7-3 7.2 Type Consistency 2. Require. If the formal parameter is a var parameter, thenM _______ the type of the formal must be a subtype [3] of the actual. The subtype relation on types is defined as follows: 3. Define. If S is not a buffer type, then type S is a subtypeM ______ _______ of type T iff values#(S) is a subset of values#(T). If S is a buffer type, then S is a subtype of type T iff values#(S) =M _______ values#(T) and allowedops#(S) is a subset of allowedops#(T). Buffer parameters also must satisfy an additional requirement 4. Require. An actual parameter of a buffer type B may appearM _______ as an actual parameter to a predefined buffer routine only if the routine name is an element of allowedops#(B). The analysis of every routine is predicated upon the assumptions implied by the types of its formal parameters. (This "analysis" might range from compilation to formal verification.) The preceding requirements ensure that the actual parameters will conform to these assumptions. The first requirement ensures that the value referred to by the actual parameter will be in the value set of the corresponding formal. This is all that is required of a const parameter (which is not a buffer). The actual var parameter objects may have new values assigned to them by the routine. For the non-buffer types, the subtype relation ensures that these assignments always will be of a value that is in the value set of the actual parameter. Buffers are essentially different from the other types because they may be shared among routines that are executing concurrently. Therefore, the values that can be associated with a buffer during the execution of a routine cannot be determined even at the time of the routine call. Buffer parameters, therefore, must satisfy a more stringent set of requirements than non-buffer parameters. The types of actual and formal buffer parameters must be the same except for their allowed operation sets. (These operation sets are provided as a significant practical convenience for specification and verification; they are not a theoretical necessity.) The consistency requirements are enforced by a combination of syntax and semantics. In most cases, the consistency requirements can be enforced strictly statically through the concept of "base type". In other cases, some run time checks will be required. Every type has an associated base type which can be determined purely statically. Informally, every scalar type and the types "integer", "rational" and "activationid" are base types. Every other type is defined from these types by various restrictions (subranges, sizes, and buffer operation restrictions) and compositions (using the structured types). The base type of a given type is a type that is built in the same way from the same primitive base types, but without imposing any restrictions. (Exceptions are buffers and abstract types, and these require some special considerations.) The base types of the various types are defined in terms of the function basetype#(T) TYPES Page 7-4 7.2 Type Consistency in the following sections. The basic syntactic consistency requirement of the types of actual and formal parameters is type compatibility. 5. Define. Type S is compatible with type T iff basetype#(S) =M ______ __________ basetype#(T). Type compatibility is required of all actual and formal parameters. It also is required syntactically that the value and subtype requirements above [1,2] be potentially satisfiable. In most cases, it can be determined statically whether these requirements are satisfied. In other cases, it can be determined statically that they are not satisfied; these cases are not allowed. In some cases, it cannot be determined statically if the requirements are satisfied; these cases will require run time checks as described in [Section 8.1]. 7.3 TYPE DECLARATIONS A type declaration defines a type unit which in turn defines a new type from an existing type. The type declaration also may contain formal specifications. SyntaxM______ A has a and a . 1. ::= = 1.1 Define. The type name of a is theM ______ ____ ____ in the . 2. ::= type -- | | |---- ---- | | |<-------------------------------- | |------- ------ | | |<-------------------------------- | 2.1 Define. The is the composition accessM ______ ___________ ______ list of the type. The names that appear in the compositionM ____ access list are included automatically in the reference access list of the type unit if it has one. TYPES Page 7-5 7.3 Type Declarations 2.2 Define. A unit U has composition access to a type iff UM ______ ___________ ______ is named in the composition access list of the type. 2.3 Define. A type is an abstract type iff it has aM ______ ________ ____ composition access list. 2.4 Require. The of an abstract type must not beM _______ used in analyzing the syntax of any program description unit U unless U is named in the composition access list of the abstract type or U is a unit that appears in a scope named in the composition access list. (In effect, a scope name is an abbreviation for all units that are declared in that scope.) 3. ::= initially -- ( ----------------- --- ) ------ | ^ |- prove ---| | | -- assume --- 3.1 Require. The type of the must be of theM _______ same type as the (). 4. ::= pending | | 4.1 Require. An may only be used as theM _______ of an abstract type. 5. ::= 5.1 Require. The must be a type name.M _______ ExamplesM________ type Register = pending; type Charnum = int[0..255]; type Queue_Element = record (priority:int; item:item_type); type freqTable initially (NullTable) = Hashtable; SemanticsM_________ A that is not an abstract type defines a new type T from its as follows where T is the type name defined in the : TYPES Page 7-6 7.3 Type Declarations values#(T) = values#() initial#(T) = initial#(), and allowedops#(T) = allowedops#() if the defines a buffer type. Also, basetype#(T) = basetype#() The special considerations for abstract types are given in [Section 7.4]. The function initial#(T) is a predefined function for every type T that is defined by a , function initial (T:""):T "Initial" takes a as an actual parameter and returns the default initial value of the type named by the . The , if present, is a formal specification of initial#(T). If the is present, then the relation initial(T) = I must hold where I is the value of the in the . The is useful primarily with abstract types. The reserved words "prove" and "assume" are verification directives. "Prove" directs that the relation above be proved. "Assume" allows it to be assumed in the proof. The absence of an explicit directive is equivalent to the "prove" directive. 7.4 DATA ABSTRACTION An abstract type [Section 7.3-2.3] defines a data abstraction by using a composition access list to encapsulate a type definition of the concrete representation of the abstract type. The equivalence class of concrete objects representing an abstract object is defined by extending the "=" operator [Section 9.3.2] and [Section 4.2]. SyntaxM______ An abstract type is defined by a that has a composition access list [Section 7.3-2.1]. The composition access list prohibits general access to the of the abstract type. Only those units that appear in the composition access list may refer to the of an abstract type. The of an abstract type may be a , an , or pending. TYPES Page 7-7 7.4 Data Abstraction 1. ::= begin : ; end 1.1 Define. The is a local name of the unitM ______ _____ ____ name scope of the and names a constantM ________ with respect to the . 1.2 Define. The type of the is the type definedM ______ ____ by the . 2. ::= hold ---------------> | ^ | | ---- ; ---- ExamplesM________ type priority_queue = begin q: sequence [max_q_size] of queue_element; hold ordered_q(q); end; type hashtable = begin htab: array[bound] of Hentry; hold AllUnique(htab); end; SemanticsM_________ The abstract values of a data abstraction are defined by using an equality extension to partition the concrete representation into equivalence classes. Each member of a given class represents the same abstract value. The concrete representation is defined by the . 3. Define. The concrete representation of an abstract type isM ______ ________ ______________ the type defined by the in the . The may be the entire or it may appear in the . If the is an , the defines a constraint on the value set of the concrete representation. Only those values that satisfy the may represent an abstract object. TYPES Page 7-8 7.4 Data Abstraction 4. Define. A value z of the concrete representation satisfiesM ______ _________ the iff the is trueM ___ _____ ______________ when z replaces all occurences in the of the that precedes the . The is an external specification with very limited accessibility. It may be used in only those units that have composition access to the abstract type. The must be true for the default initial value of the abstract type. It then may be assumed upon entry to each routine with composition access to the type and must be proved upon either normal or abnormal exit. If a unit U refers to an object of an abstract type A, the type that is defined by the abstract type depends on whether unit U has composition access to type A. If U has composition access to A, (where A is the type name that is the in the of the abstract type), then the type and the base type of A are the same as the type and the base type of the that appears in the , values#(A) = values#(), initial#(A) = initial#(), allowedops#(A) = allowedops#() if defines a buffer type basetype#(A) = basetype#() In short, if U has composition access to A, then the is treated as a declaration of a non-abstract type. If unit U does not have composition access to A, however, then type A is treated differently. The abstract value set is defined by an extension of the equality operator [Section 4.2]. The axioms for equality partition the complete value set of the concrete representation into disjoint equivalence classes. (The may eliminate some concrete values as representatives of abstract values, but this does not effect the disjointness of the partitioning.) values#(A) = The set of equivalence classes defined by the equality extension on abstract type A. Each class defines a single abstract value that may be represented by any member of that class. initial#(A) = The abstract value represented by initial#() The is the one that appears in the of the abstract type. An abstract type is not a buffer type, and therefore, it does not have an allowed operation set. TYPES Page 7-9 7.4 Data Abstraction If U does not have composition access to A, the base type of A is the type name itself, A. basetype#(A) = A. This is the mechanism for encapsulating the concrete representation of an abstract type. The base type of an abstract type is the base type of its concrete representation only in units that have composition access to the abstract type. The axioms for equality [Section 9.3.2] partition the concrete representation into the equivalence classes that define the correspondence between abstract and concrete values. These are properties that must be proved for every extension of equality on an abstract type, so that the "=" operator can be used freely on abstract types in the same way it is used on other types. 7.5 TYPE DEFINITIONS A type definition defines a type. It may define any simple, structured, or special type. SyntaxM______ A may be a optionally followed by an , or it may be a , a , or a . 1. ::= ------ -------------------------------------------- | | ^ | --- := ------>| | | |-- ----------------------------------------| | | |-- -----------------------------------| | | --- ---------------------------------------- 1.1 Define. The , if present, is the initialM ______ _______ value expression.M _____ __________ 1.2 Require. If the is followed by an initialM _______ value expression, the type defined by the must have an assignment procedure. 1.3 Require. The type of the initial value expression mustM _______ be compatible with the type defined by the . 1.4 Require. The initial value expression must evaluateM _______ statically to a constant. TYPES Page 7-10 7.5 Type Definitions The simple types are defined by the s and the predefined s "character", "boolean", "integer", and "rational" that may appear in the . The structured types are defined by the s. The special types are defined by the predefined "activationid" and the s. 2. ::= SemanticsM_________ A defines a type. The type is the same as the type of the right hand side except that the initial value expression may define a different default initial value. If the right hand side RHS is a , , , or , then values#() = values#(RHS), initial#() = initial#(RHS), allowedops#() = allowedops#(RHS) if RHS defines a buffer type, and basetype#() = basetype#(RHS) If the is followed by an initial value expression, then values#() = values#(), initial#() = the value of , and basetype#() = basetype#() Buffer types do not have an assignment procedure so that the cannot be a buffer type and cannot have an allowed operation set. 7.6 TYPE REFERENCES A type reference defines a type from a type name and possibly a range restriction or an operation restriction. SyntaxM______ A may be composed of a , a , and a in various combinations. TYPES Page 7-11 7.6 Type References 1. ::= --- --------------------------------------- | | ^ | |------ ----| | | | ---------------|----------- ------------- 1.1 Require. If a follows a , the typeM _______ defined by the range must be compatible with the type defined by the . 1.2 Require. A may appear in the only if it begins with a that names a buffer type. 1.3 Define. The defines a subrange type iff itM ______ ________ has a . 2. ::= ( .. ) 2.1 Require. The types of the s must be simpleM _______ types that are compatible. 2.2 Require. If the appears as part of a M _______ in the context of , , a global , or a , then the s must statically evaluate to constants. 2.3 Require. If the expressions evaluate statically toM _______ constants, then the value of the first must be less than or equal to the value of the second . ExamplesM________ type int = integer(-2**35..2**35-1) type color = (red, white, blue) type line = buffer(100) of message; type internal_port = record(inline: line ; outline: line ); SemanticsM_________ A defines a type and a base type that depends on the form of the right hand side. Basetype#() = Basetype#() TYPES Page 7-12 7.6 Type References if the type has a ; otherwise, basetype#() = basetype#(a) where a is the type of either one of the s in the . These rules eliminate any range or operation restrictions from the base type. Form Type Defined by M ____ ____ _______ __ _____ ____ The type is the same as the type defined by , values#() = values#() initial#() = initial#() allowedops#() = allowedops#() This form defines a subrange type as follows values#() = the set of all values in the closed interval from a to b where a is the value of the first in the and b is the value of the second. initial#() = initial#(basetype#()) if that value is in values#(); otherwise "a" from the closed interval from a to b defined above. This form also defines a subrange type values#() = the intersection of values#() with values#(). (This set may be empty.) initial#() = initial#(basetype#()) if that value is in values#(); otherwise the smallest value in values#(). This form restricts the allowed operation set of a buffer type values#() = values#() initial#() = initial#() allowedops#() = the intersection of allowedops#() with allowedops#() The allowed operations of a are defined in [Section 7.11.2-4]. TYPES Page 7-13 SIMPLE TYPES 7.7 SIMPLE TYPES The simple types are the scalar types, the types "integer", and "rational" and the subrange types. Every simple type has an ordered value set, a way of expressing constants in that value set, a default initial value, and an operation set. Subrange types are simple types that are subtypes of the basic simple types. Each basic simple type, bs, has the following relational operations: Notation FunctionsM ________ _________ x = y function bs#eq(x,y:bs):boolean x eq y x ne y function bs#ne(x,y:bs):boolean x < y function bs#lt(x,y:bs):boolean x lt y x le y function bs#le(x,y:bs):boolean x > y function bs#gt(x,y:bs):boolean x gt y x ge y function bs#ge(x,y:bs):boolean The operations are written using strictly the notation of the left. Each notation denotes a call to the corresponding function on the right. (Overloading is dealt with in [Section 9.3.1].) The "lt" function defines a complete ordering of the value set and has the properties: lemma lt_transitive(x,y,z:bs) = (x lt y) and (y lt z) -> (x lt z) lemma trichotomy (x,y:bs) = [(x lt y) or (x = y) or (y lt x)] and [x lt y -> (x ne y) and not (y lt x)] and [x = y -> not (x lt y) and not (y lt x)] and [y lt x -> not (x lt y) and x ne y] {Exactly one of x lt y, x = y, and y lt x is true.} The remaining relational operations are defined as follows: lemma le_def(x,y:bs) = (x le y) iff (x y iff y < x; lemma ge_def(x,y:bs) = x ge y iff y le x The basic simple types also have the operations TYPES Page 7-14 7.7 Simple Types Notation DescriptionM ________ ___________ max(x,y) function max(x,y:bs):bs = begin exit result = if x>y then x else y fi; end; min(x,y) function min(x,y:bs):bs = begin exit result = if x ::= --------- , -------- | | v | -- ( ---- ----- ) -- 2. Require. A scalar type is regarded syntactically as definingM _______ a constant unit for every in the scalar type. The s are the names of the constant units and therefore must not conflict with any other local or unit names. These constant units are defined implicitly and may not appear in s or s. Let denote the first in the scalar type definition. Each subsequent in the type definition will be denoted by , where the preceding is . Value Set: {, ..., } for some constant n>0. Constants: The constants are the s. Order: lt iff i < j Default Initial Value: Operations: The function operations on a scalar type s are "eq", "ne", "lt", "le", "gt", "ge", "max", "min", "upper", and "lower" plus the following ("s" represents the name of a scalar type): Notation DescriptionM ________ ___________ pred(x) function s#pred(x:s):s unless (nopred)= begin exit case (is normal: some k:integer[1..n], x = and result = ; is nopred: x = ); end; succ(x) function s#succ(x:s):s unless (nosucc)= begin TYPES Page 7-16 7.7.1 Scalar Types exit case (is normal: some k:integer[0..n-1], x = and result = is nosucc: x = ); end; ord(x) function s#ord(x:s):integer= begin exit " = x"; end; scale(x,s) function s#scale(k:integer; s:"scalar type"): basetype#(s) unless (underscale, overscale) = begin exit case (is normal: k in <<0..n>> and result = ; is underscale: k<0; is overscale: n of a (e.g., 'a, 'b, ... , 'z). Default Initial Value: the ASCII character nul Operations: The operations are the same as for scalar types. 7.7.3 Boolean Type The boolean type is a special predefined scalar type "(false, true)". Value Set: {false, true} Order: false < true Constants: The constants are the reserved words "false" and "true". Default Initial Value: false Operations: The operations are the operations for scalar types and the following logical operations: Notation DescriptionM ________ ___________ not x function boolean#not(x:boolean):boolean = begin exit result=if x then false else true fi; end; x and y function boolean#and(x,y:boolean):boolean = x & y begin exit result=if x then y else false fi; end; x or y function boolean#or(x,y:boolean):boolean = begin exit result=if x then true else y fi; end; x -> y function boolean#imp(x,y:boolen);boolean = x imp y begin exit result= if x then y else true fi; end; x iff y function boolean#eq(x,y:boolean):boolean = x = y begin exit result = (x=y); end; TYPES Page 7-18 7.7.3 Boolean Type Type boolean also has the "all" and "some" operations for universal and existential quantification [Section 9.6]. 7.7.4 Integer Type Type integer is the unbounded set of integers. (The integers realizable on a given machine will be a subrange of type integer.) Value Set: {..., -1, 0, 1, ...} Order: ... < -1 < 0 < 1 < ... Constants: The non-negative constants are represented by s using conventional decimal digit notation. Negative constants are non-negative constants preceded by "-". Default Initial Value: 0 Operations: Type integer, as a simple type, has the function operations "eq", "ne", "lt", "le", "gt", "ge", "max", and "min". Integer division is handled by the "div" and "mod" operators. Types integer and rational also share the operators "+", "-", "*" and "**", which are described in [Section 7.7.6]. Notation DescriptionM ________ ___________ x div y function integer#divide(x,y:integer):integer unless (divideerror, zerodivide)= begin exit case (is divideerror: baddivide(x,y); is zerodivide: y=0); end; x mod y x - (x div y) * y pred(x) x - 1 succ(x) x + 1 These operations have the following conventional properties: lemma moddiv(x,y:integer) = [(x div y) * y + (x mod y) = x]; lemma integerorder(x,y:integer) = [x < y iff x+1 le y] Every integer function operation may signal an "error" condition - e.g., "divideerror". These are conditions that are signalled by an implementation of a function if the result of the operation will be an integer that is not available in the particular implementation. The meanings of these conditions, therefore, are implementation dependent and are defined by the functions "badadd", "badmultiply", .... The TYPES Page 7-19 7.7.4 Integer Type analysis and verification of integer operations is implementation independent, so long as the analysis refers only to "badadd", "badmultiply", ... and not to the actual definitions of these functions. Details of a particular implementation may be brought into the proof by expanding specific implementation definitions for these functions. 7.7.5 Rational Type Type rational is the unbounded set of rational numbers. The type rational is included in Gypsy mainly to support specification and formal verification. The analysis of expressions involving integers often requires solution of linear equations. Thus, our domain of discourse must include rational numbers. Particular implementations of Gypsy may choose not to support use of rationals at execution time. Value Set: {all rational numbers} Order: If x = p / q and y = r / s where q,s > 0, then x < y iff integer p * s < q * r. Constants: Non-negative constants are written in the form /; negative constants are written -/. Default Initial Value: 0 Operations: Type rational, as a simple type, has the function operations "eq", "ne", "lt", "le", "gt", "ge", "max", and "min". In addition, the "/" operator is overloaded to provide for both construction of rational numbers from integers and for rational division. Notation DescriptionM ________ ___________ i / j function rational#number(i,j:integer):rational unless (divideerror, zerodivide)= begin exit case (is normal: result = "the rational number whose numerator is x and denominator is y"; is divideerror: baddivide(x,y); is zerodivide: y=0); end; x / y function rational#divide(x,y:rational):rational unless (divideerror, zerodivide) = begin exit case (is zerodivide: y=0; is divideerror: baddivide(x,y)); end; TYPES Page 7-20 7.7.5 Rational Type 7.7.6 Properties Of Numeric Types The types integer and rational share many of the normal axioms from mathematics. Function descriptions for the arithmetic operators common to types integer and rational are provided here. Axiomatic properties of the arithmetic operators appear in [section 9.3.2]. In the following descriptions let T be either "integer" or "rational". Let zero and one be either "0" and "1" or "0/1" and "1/1" according to whether T is "integer" or "rational", respectively. Notation DescriptionM ________ ___________ x + y function T#add (x,y:T) : T unless (adderror) = begin exit case (is adderror: T#badadd(x,y)); end; x * y function T#multiply (x,y:T) : T unless (multiplyerror) = begin exit case (is multiplyerror: T#badmultiply(x,y)); end; -x function T#minus (x:T) : T unless (minuserror) = begin exit case (is minuserror: T#badminus(x)); end; x - y function T#subtract (x,y:T) : T unless (subtracterror) = begin exit case (is subtracterror: T#badsubtract(x,y)); end; x ** y function T#power (x,y:T) : T unless (powererror, negativeexponent, powerindeterminate) = begin exit case (is normal: y ge zero and (y = zero -> x ne zero) and (result = if y = zero then one else x * T#power(x,y-one) fi); is powererror: y > zero and T#badpower(x,y); is negativeexponent: y < zero; is powerindeterminate: x = zero and y = zero) end; TYPES Page 7-21 7.7.6 Properties of Numeric Types 7.7.7 Subrange Types A subrange type has the form T ( .. ) or ( .. ) where both s evaluate to elements in values#(T). The subrange is a subtype of simple type T. Value Set: {x | low le x & x le high} Order: The order is the same as for type T. Constants: The constants are the scalar constants of type T that are elements of the value set for the subrange. Default Initial Values: The default initial value is the default initial value d of type T if low le d & d le high; otherwise the default initial value is low. Operations: The operations are the same as for type T and produce the same results for the same arguments. The normal type consistency rules of parameter passage apply. Note that results are of type T, not the subrange type. Use of the results as objects of type T is handled by normal parameter transmission rules. Thus, pred(x) and succ(x) terminate abnormally if their result goes outside the scalar base type, not just outside the subrange. 7.8 STRUCTURED TYPES A value of a structured type may consist of a number of component values. These components can be referred to individually through special component selector operations. SyntaxM______ 1. ::= | | | | SemanticsM_________ Each value in the value set of a structured type may have several component values. 2. Define. A structured type is static if the number ofM ______ ______ components of its values is fixed. TYPES Page 7-22 7.8 Structured Types 3. Define. A structured type is dynamic if the number ofM ______ _______ components of its values may vary. The static structured types are arrays and records. The others are dynamic. A size restriction may be declared for each of the dynamic types. This restriction is an upper bound on the number of components of any structured value. If no size restriction is given, then the maximum number of components is unbounded. 7.9 STATIC STRUCTURED TYPES Elements may be selected from arrays, records, sequences, and mappings. A selector applied to a record object can be checked for validity statically. This is not so for arrays, sequences, and mappings. At run time, the validity of the selecting expression is checked. If the expression does not properly select an element of the structure, the condition "indexerror" is signalled. (Indexerror is a formal condition parameter to each of the structure selection functions and is signalled on abnormal termination, as described in [Section 8.2].) 7.9.1 Records SyntaxM______ 1. ::= ----------------------------------- ; ------- | | | -------- , ------- | | | | | v v | | -- record ( ------ ---- : --- ) -- 1.1 Require. Each be unique.M _______ The form ,..., : ; is equivalent to : ; ... : ; 2. Define. The basetype#() isM ______ _________ record(: basetype#(); TYPES Page 7-23 7.9.1 Records .. : basetype#(); SemanticsM_________ Value Set: The set of all record values of the . Record Value: A has the form record( : ; ... : ;) A record value is the ordered pair (record, {(identifier,i>, xi) | xi an element of the values of the corresponding to the field ; each must appear as the first element of an ordered pair exactly once.}). Constants: There are no primitive record structure constants. Statically evaluatable record structures may be composed using default initialization and alteration clauses (e.g., initial (R)). Default Initial Value: the record value (record, { (xi,yi) | xi is and yi is the default initial value for }). Operations: eq, ne, .fieldname, :=, with The specifications for record equality and record selection are given here. The general axioms for equality are given in Section [9.3.2], for component assignments in Section 9.4.2, and for assignment in general in Section 10.2.2. Notation DescriptionM ________ ___________ r eq s function record#eq(r:T1; s:T2): boolean = begin exit result iff all f: "field identifier of T", r.f = s.f; end; Where type T1 is a record type, and types T1 TYPES Page 7-24 7.9.1 Records and T2 are compatible. (Note: type compatibility requires both T1 and T2 to have the same field identifiers.) Record equality for is undefined if there is at least one for which equality is not defined. r.f function record#select(r:T; f:"field identifier"):Tf = begin exit Result = "The value x such that the ordered pair (f,x) is a com- ponent of r"; end; Where f is an in the T, and Tf is the associated with f. r with (.f := x) function record#componentassign (r:T; f:"field identifier"; x:"field type") : T = begin exit result = "the record value r with the value of the 'f' component equal to x"; end; ExamplesM________ record(day:(1..31); month:(1..12); year:integer) record(last_initial, first_initial: character; ssn: integer) 7.9.2 Arrays SyntaxM______ 1. ::= array ( ) of 1.1 Require. The must be a simple type.M _______ 1.2 Define. The value set of the is calledM ______ the index set of the .M _____ ___ TYPES Page 7-25 7.9.2 Arrays 1.3 Require. The must not be a subtype ofM _______ type rational. 1.4 Define. The is called the element typeM ______ _______ ____ of the . 2. ::= 2.1 Require. The must define a simple type.M _______ 3. Define. The (basetype#) is array () of basetype#(). SemanticsM_________ Value Set: The set of array values for . Array Value: (array, { (xi,yi) | xi is in the index set of and yi is in the value set of the element type; each element of the index set must appear as the first element of an ordered pair exactly once.}) Constants: There are no primitive array constants. Statically evaluatable array structures may be composed using default initializations and alteration clauses. Default Initial Values: the array value (array, {xi,d} | xi is an element of the index set, and d is the default initial value for the element type}). Operations: [i], eq, ne, :=, with The specifications for array equality and element selection are given here. The general axioms for equality are given in Section 9.3.2, for component assignment in Section 9.4.2, and for array assignment in Section 10.2.2. Notation DescriptionM ________ ___________ a eq b function array#eq(a:T1; b:T2): boolean begin exit result iff all i:"index set", a[i] = b[i]; end; where array types T1 and T2 are compatible. (Note: type compatibility requires that both T1 and T2 have the same index set.) Array TYPES Page 7-26 7.9.2 Arrays equality for is undefined if equality is not defined on the element type. a [i] function array#select(a:T; i:index):element = unless (indexerror) begin exit case (is normal: result = "the value z of the component (i,z) of a"; is indexerror: not i in "indexset"); end; where type T = array[index] of element a with ([i]:=x) function array#componentassign (a:T; i:index; x:element): T unless (indexerror) = begin entry i in values#(index) otherwise indexerror; exit result = "the value of array a the value of component i equal to x"; end; ExamplesM________ array[boolean] of color array([1..100]) of integer 7.10 DYNAMIC STRUCTURED TYPES The distinguishing property of dynamic types is that the number of components of a dynamic object may vary at run time. There are three dynamic types, "sets", "mappings", and "sequences". Since the size of dynamic objects may grow at run time, there is a possibility that an implementation will run out of available space trying to construct a new dynamic object. Space requirements for temporaries of static types may be computed statically, whereas they cannot be computed statically (in general) for dynamic structures. Each of the functions that construct objects of some dynamic structured type may terminate abnormally if sufficient space is not available. In this case, the function signals the condition "spaceerror". Dynamic structures of size zero (null sets, null mappings, and null sequences) are quite useful as constants. The standard function takes the type identifier of a dynamic structured type and returns a null object of that type. For example, if T is a dynamic type, TYPES Page 7-27 7.10 Dynamic Structured Types null(T) returns a null object of type T. 7.10.1 Sets Set types correspond directly to the equivalent mathematical concept. Each value of a set type is a set. SyntaxM______ 1. ::= set --------------------------- of | ^ | | -- ( ) -- 1.1 Define. The is a size restriction.M ______ ____ ___________ 1.2 Define. The is called the element typeM ______ _______ ____ of the set. 2. ::= 2.1 Require. The must evaluate to aM _______ non-negative integer. 3. Define. The basetype#() is set of basetype#(). SemanticsM_________ Let n be the value of size restriction if there is one, and let T be the type defined by . Value Set: the set of set values for . Constants: null(S), where S is the name of a set type. initial(S), where S is the name of a set type. (set:x1...xk), where each xi is a constant of the same basetype. This is a set constant of type "set of basetype(x1)". Default Initial Value: (set, {}), the set value representation of the empty set. Operations: eq, ne, union, intersect, difference, in, adjoin, omit, sub, with, :=, size TYPES Page 7-28 7.10.1 Sets Notation DescriptionM ________ ___________ x in s function set#member(x:element; s:settype): boolean = begin exit result iff "x is an element of the second component of the set value of s"; end; where settype = set ... of element. s adjoin x function set#adjoin (s:settype; e:element): "basetype#(settype)" unless (spaceerror) = begin exit x in result and all y:element, y ne x ->(y in s iff y in result); end; s omit x function set#delete(s:settype; x:element): basetype#(settype) unless (membererror, spaceerror) = begin entry x in s otherwise membererror; exit not x in result and all y:element, y ne x -> (y in result iff y in s); end; Let ST1 and ST2 be compatible set types whose elements are contained in values#(element), and ST be basetype#(ST1). s1 eq s2 function set#eq(s1:ST1; s2:ST2) : boolean begin exit set#eq(s1,s2) iff all y:element, y in s1 iff y in s2; end; Note that size restrictions need not match. Set equality is undefined if equality is not defined on the element type. size(s) function set#size (s:settype) : integer = begin exit result = "the number of elements in the set value of s"; end; s1 union s2 function set#union (s1:ST1; s2:ST2) : ST unless (spaceerror) = begin TYPES Page 7-29 7.10.1 Sets exit all x:element, x in Result iff x in s1 or x in s2; end; s1 intersect s2 function set#intersect(s1:ST1;s2:ST2):ST unless (spaceerror) = begin exit all x:element, x in Result iff x in s1 & x in s2; end; s1 difference s2 function set#difference(s1:ST1;s2:ST2):ST unless (spaceerror) = begin exit all x:element, x in Result iff x in s1 & not (x in s2); end; end lit.b .index Sub(operator) .lit s1 sub s2 function set#sub (s1:ST1; s2:ST2) : boolean = begin exit result iff all x:element, x in s1 -> x in s2; end; ExamplesM________ set of days_of_week set (11) of (1..35) 7.10.2 Mappings SyntaxM______ A is defined by a domain , a range , and an optional size restriction . 1. ::= TYPES Page 7-30 7.10.2 Mappings mapping -- | |-- ( ) -- | | |<------------------------ | -- from to 1.1 Define. The is a size restriction.M ______ ____ ___________ 1.2 Define. The following the keywordM ______ "from" is the domain type; the followingM ______ ____ the keyword "to" is the range type.M _____ ____ 1.3 Require. The domain type must not contain a buffer typeM _______ or an activationid type. 2. Define. The basetype() is mapping from to basetype#(). SemanticsM_________ Let n be the value of the size restriction, if there is one. Value Set: the set of mapping values for . Mapping Value: A mapping value is the ordered pair (mapping, { (x1,y1), ... ,(xk,yk) } ), where k is non-negative; each xi is a unique element inM ______ values#(domain type), and each yi is an element in values#(range type); k is less than or equal to n, if there is a size restriction. Constants: null (MT), where MT is a ; this denotes the empty mapping, (mapping,{}). initial(MT), where MT is a ; this denotes the default initial value for objects of type MT. Statically evaluatable mapping expressions may be constructed using default initialization and alteration clauses as described in Section 9.4.2. Default Initial Values: the value (mapping, {}), denoting the null mapping value for . Operations: [x], eq, ne, union, intersection, difference, sub, with, :=, domain, range, size TYPES Page 7-31 7.10.2 Mappings The general axioms for these operations are discussed in Section 9.3.2. Details specific to mapping types are described below. Let "mappingtype", "MT1", and "MT2" be compatible mapping types from domaintype to rangetype, and let "MTF" be basetype#(MT1). Notation DescriptionM ________ ___________ Domain(M) function domain(M:mappingtype): domaintype = begin exit result = "the set of all domain elements appearing as the first component of the ordered pairs in the set contained in the mapping value of M" ; end; Range(M) function range(M:mappingtype): rangetype = begin exit result = "the set of all range elements appearing as the second component of the ordered pairs in the set component of the mapping value of M" ; end; M[x] function mapping#select (M: mappingtype; x: domaintype): rangetype unless (indexerror) = begin entry x in domain(M) otherwise indexerror; exit result = "the value y such that the ordered pair (x,y) is an element of the set component of the mapping value of M" ; end; M1 eq M2 function mapping#eq (M1: MT1; M2: MT2): boolean begin exit mapping#eq(M1,M2) iff domain(M1) = domain(M2) and all x:domaintype, x in domain(M1) -> M1[x] = M2[x]; end; M1 union M2 function mapping#union (M1: MT1; M2: MT2): MTF unless (nonunique, spaceerror) begin entry all x: Domaintype, x in domain(M1) and x in domain(M2) -> M1[x] = M2[x] exit all s: basetype#(domaintype(MTF)) x in domain(M1) iff TYPES Page 7-32 7.10.2 Mappings x in domain(Result) & result[x] = M1(x) and x in domain(M2) iff x in domain(Result) & result[x] = M2(x) end; M1 intersect M2 function mapping#intersect (M1: MT1; M2: MT2): MTF unless (cond spaceerror, nonunique) = begin entry size(domain(M1) intersect domain(M2)) ne 0 and some x: D1, x in domain(M1) intersect domain(M2) -> M1[x] ne M2[x]; otherwise nonunique; exit domain (result) = domain(M1) intersect domain(M2) and x: D x in domain(M1) -> M1[x] = Result [x]; and x in domain(M2) -> M2[x] = Result [x]; end; M1 difference M2 function mapping#difference (M1: MT1; M2: MT2): MTF unless (cond suberror, spaceerror) = begin entry M2 sub M1 otherwise suberror; exit all x: D1, ( x in domain(Result) iff x in domain(M1) and not (x in domain(M2))) and ( x in domain(Result) -> (Result)[x] = M1[x]); end; M1 sub M2 function mapping#sub (M1: MT1; M2: MT2): boolean begin exit M1 sub M2 iff (domain(M1) sub domain(M2) and all x: D1, x in domain(M1) -> M1[x] = M2[x]); end; m with (mapomit[x]) function mapping#delete (M: MT; x:Domaintype): MTF unless (cond indexerror, spaceerror) = begin entry x in domain(M) otherwise TYPES Page 7-33 7.10.2 Mappings indexerror; exit domain(Result) = domain(M) omit x and all y: D, y in domain(Result) -> Result[y] = M[y]; end; size(m) function mapping#size (M:MT) : integer = begin exit Result = "the number of elements x of the domain for which M[x] is defined"; end; m with ([x]:=y) function mapping#componentassign (m:MT; x:Domaintype; y:Rangetype) unless (spaceerror) = begin exit result = "the mapping value of m with the value of the component x equal to y"; end; ExamplesM________ mapping from days_of_week to integer[1..7] mapping (3) from flag_colors to dye_num 7.10.3 Sequences SyntaxM______ 1. ::= sequence --------------------------- of ---> | ^ | | -- ( ) -- 1.1 Define. The is a size restriction.M ______ ____ ___________ 1.2 Define. The is called the elementM ______ _______ type.M ____ 2. Define. The basetype#() is sequence ofM ______ basetype#(). TYPES Page 7-34 7.10.3 Sequences SemanticsM_________ Let n be the value of the size restriction, if there is one. Value Set: the set of sequences for . Sequence Value: A sequence value is an ordered pair (sequence, { (1,y1), ... (k,yk) } ) where k le n, if there is a size restriction, and each yi is in the value set of the element type. Constants: null(T), where T is the name of a sequence type; this denotes the null sequence for type T. initial(T) (seq: e1, ... ek) (see Section 9.7) (e1, ..., ek) "abc..." denotes the sequence of characters ('a,'b,'c,...). Default Initial Values: the sequence value (sequence, {}), denoting the empty sequence for . Operations: [i], [i..j], @, <:, :>, first, last, nonfirst, nonlast, size, :=, with, null, initial, eq, ne, sub, in Let "seqtype", "seqtype1", and "seqtype2" be compatible sequence types whose elements are contained in values#(element). Notation DescriptionM ________ ___________ size(S) function sequence#size (S: seqtype): integer = begin exit Result = "the number of pairs in the set component of the sequence value of S" ; end; S[i] function sequence#select (S: seqtype; i: integer): element unless (indexerror) = begin entry 1 le i & i le size(S) otherwise indexerror; exit Result = "yi such that the ordered pair (i,yi) is an element of the set component of the sequence value of S"; end; TYPES Page 7-35 7.10.3 Sequences where seqtype = sequence ... of element. x in S function sequence#element (x: element; S: seqtype): boolean = begin exit result iff some i: integer[1..size(S)], S[i] = x; end; S[i..j] function sequence#subselect (S: seqtype; i,j: integer): seqtype unless (indexerror, spaceerror) = begin entry i le j+1 and i in (1..size(S) + 1) and j in (0..size(S)) otherwise indexerror; exit (all k: integer[1..j-i+1], Result[k] = S[i+k-1]) and size(Result) = j-i+1; end; (Note: Thus S[i..i-1] denotes the null sequence if i is in range 1 to size(S)+1.) S1 @ S2 function sequence#append (S1: seqtype1; S1 append S2 S1: seqtype2): "basetype#(seqtype1)" unless (spaceerror) = begin exit size(Result) = size(S1) + size(S2) and Result [1..size(S1)] = S1 and Result [size(S1)+1..size(Result)] = S2; end; s with([i]:=x function sequence#componentassign (s:seqtype; i:integer; x:element):S unless (indexerror, spaceerror) = begin entry i in (0..size(s)+1) otherwise indexerror; exit result = s[1..i-1] @ (seq: x) @ s[i+1..size(s)]; end; first(S) S[1] nonfirst(S) S[2..size(S)] last(S) S[size(S)] nonlast(S) S[1..size(S)] TYPES Page 7-36 7.10.3 Sequences ExamplesM________ sequence (365) of days_of_week sequence of coaches 7.11 OTHER TYPES 7.11.1 Activationid Types Activationid is a predefined type. There are no primitive constants of type activationid, and there are no primitive activationid valued functions. Activationids are used in the specifications of concurrent processes to distinguish between individual processes. Activationids may be passed as actual data parameters according to the normal rules for parameter passage. Objects of type activationid may only be declared explicitly as formal const parameters to routines or as bound identifiers in a . Variables and formal var parameters of type activationid may not be declared. As mentioned in Section 4.1 on procedure declarations, each Gypsy procedure has an implicit formal const parameter "myid" of type activationid. The value of this parameter is provided as part of the procedure call mechanism, allowing the specifications to distinguish each distinct activation of the procedure. Activationids are to support specification and proof of concurrent systems. The standard functions that extract histories of individual process actions on a buffer take an activationid parameter to identify the process. Constants: none may be specified in the program text; proof rules may introduce activationid constants into verification conditions and proofs. Default Initial Value: not applicable; activationids are always passed as parameters, and formal parameters need not be initialized to a default value. Operations: no operations yield results of type activationid. Assignment of activationids is not defined. Equality is defined. See Section 7.11.2 for examples of the use of activationids. TYPES Page 7-37 7.11.1 Activationid Types 7.11.2 Buffer Types Buffers are the mechanism used by Gypsy programs for concurrent process synchronization and data sharing. A general discussion of message buffers is found in [Brinch Hansen, 73]. In effect, a buffer consists of a sequence with access protected by mutual exclusion between concurrent processes. Execution time manipulation of the contents of the buffer is limited to a strict first in, first out discipline. SyntaxM______ 1. ::= buffer ------------------------------> of | | | | -- ( ) --- 1.1 Require. The is called a sizeM _______ ____ restriction.M ___________ 1.2 Require. If there is a size restriction, it mustM _______ evaluate statically to an integer constant greater than 0. 1.3 Require. The may not be a or a that has a as a component at any level. 2. ::= --- < --- input --- > --- | ^ | | - output -- 3. Define. The basetype#() is buffer ... ofM ______ basetype#(). (The base type includes the size restriction if there is one.) Mutual ExclusionM______ _________ Buffers are the only data objects which may potentially be manipulated by more than one process at any given time. To assure that the proper semantics of buffer manipulation operations are preserved, mutual exclusion is enforced within the primitive procedures for manipulating a particular buffer. These primitive procedures are described in more detail in Sections 10.2.5, 10.2.6, and 10.2.7. TYPES Page 7-38 7.11.2 Buffer Types Buffer Manipulation ProceduresM______ ____________ __________ The only means for manipulating buffer values are the send and receive statements. (The semantics of the give statement are based on the semantics of the send statement.) Send and receive correspond to the operations of enqueuing and dequeuing a message to or from a message buffer. These are the only operations that can alter the value of a buffer. Objects sent to a message buffer by one process may be received and then manipulated by another process. There are a number of standard functions that extract various information from a buffer. Since the value of a buffer may change from one reference to another as a result of buffer manipulations by other processes, the functions that depend on the current value of the buffer are of limited utility under most circumstances. There are several functions that extract history information concerning the buffer. Local histories do not depend on the current content of the buffer, and can only be changed by the process itself. Although the global history is affected by the actions of all processes manipulating a buffer, certain relations are maintained (e.g., the local history is a subsequence of the global history) that may permit meaningful statements to be made concerning the global histories. Operation RestrictionsM_________ ____________ Buffer types are the only types for which operation restrictions are defined. The operation restrictions permit a buffer to be declared an input-only or output-only buffer. The proof methods for concurrency rely on specification of buffer histories. Those operation restrictions allow easy specification that the corresponding restricted output or input history is null. For example: type msgbuf = buffer(n) of msg defines a buffer with no operation restrictions. An input-only buffer of this type might be declared as type in_msgbuf = msgbuf and an output-only buffer as type out_msgbuf = msgbuf The buffer restrictions are interpreted as follows: Unrestricted: Any buffer operation may be performed on the buffer. Input: Any operation may be performed on the buffer except a send orM ______ a give. Output: Any operation may be performed on the buffer except aM ______ receive. TYPES Page 7-39 7.11.2 Buffer Types Type Consistency and Parameter PassageM____ ___________ ___ _________ _______ Type consistency rules for buffer parameter passage are slightly different than for other data types. One reason for this is that passing a buffer value as an actual parameter does not permit the sort of value checking that is possible when passing a non-shared object. An actual buffer parameter is type consistent with a formal buffer parameter only if values#(TypeOfFormal) = values#(TypeOfActual) and allowedops#(TypeOfFormal) sub allowedops#(TypeOfActual) Thus an unrestricted buffer may be passed as an actual parameter that corresponds to a restricted formal buffer parameter. SemanticsM_________ For the purpose of exposition, let us assume the following type definitions based on the occurrence of the . Buffer types are not implemented in terms of these type names and type definitions that follow. Their use here is simply to provide type names for types that might otherwise be anonymous.M _____ const n= ; {if there was one.} type message = ; {from the } type stampedmsg# = record (timestamp#: integer; message# : message); type identifiedstampedmsg# = record (idset#: set of activationid; stampedmsg#: stampedmsg#); type history# = sequence of message; type extendedhistory# = sequence of stampedmsg#; type bufferhistory# = sequence of identifiedstampedmsg#; type buffercontent = sequence(n) of message; Value Set: the set of buffer values defined for the Buffer Value: A buffer value is a 4-tuple, (buffer, inputhistory, outputhistory, msgqueue) where Inputhistory and OutputHistory are of type bufferhistory, and msgqueue is of type buffercontent. The histories must satisfy the relation msgs(inputhistory) = msgs(outputhistory) @ msgqueue, TYPES Page 7-40 7.11.2 Buffer Types where function msgs extracts the msg field of the history sequence without timestamp or activationids. The input history records each message sent to the buffer, along with the activationid of the process sending the message, and a "timestamp" indicating when the message was sent. The output history records each message received from the buffer, along with the activationid of the process sending the message, and a "timestamp" indicating when the message was received. (The history must actually record the set of activationids of the procedure doing the actual send operation plus its parent procedure, and the parent's parent, and so on. Thus, if routine A calls routine B calls routine C, which finally sends a message, the set {A,B,C} will be recorded, because procedures A and B are indirectly responsible for initiating the send action.) The msgqueue component represents those messages that have been sent to the buffer, but not yet received by any process. The definition of a buffer value includes a complete history of all input and output activity on the buffer. These complete histories are needed to support the specification and proof methods. An implementation of Gypsy may choose not to support the use of the history extraction functions at runtime, and hence, choose not to maintain runtime representations for the histories. Constants: None Default Initialization: All buffer variables are initialized to the "default" value. No other value may be specified. The initial value is the buffer value (buffer, null(bufferhistory), null(bufferhistory), null(buffercontent)) Operations: send, give, receive (see Sections 10.2.5, 10.2.6, 10.2.7) full, empty, context allto, allfrom, outto, infrom xallto, xallfrom, xoutto, xinfrom msg, msgs, timestamp, timestamps Except for the send, give, and receive statements, all the other operations are standard functions that extract information from a buffer value but do not alter the value. Specifications for the standard functions follow. Notation DescriptionM ________ ___________ content(B) function content (B:buffertype): buffercontent = begin exit result = "the msgqueue component of the buffer value" ; end; TYPES Page 7-41 7.11.2 Buffer Types empty(B) function empty(B:buffertype): boolean = begin exit result iff size(content(B)) = 0; end; full(B) function full(B: buffertype): boolean = begin exit result iff size(content(B)) = n; {the size restriction} end; xallto(B) function xallto(B:buffertype): extendhistory# = begin exit result = xall# ("input history component of B"); end; function xall# (BH: bufferhistory#): extendedhistory# = begin exit result = if size (BH) = 0 then null (extendedhistory#) else BH[1].stampedmsg# :> xall#(nonfirst(BH)) fi; and xallfrom(B) function xallfrom(B: buffertype): extendedhistory# = begin exit result = xall#("output history component of B"); end; xoutto(B,id) function xoutto(B: buffertype; id: activationid): extendedhistory# = begin exit result = xsome#("outputhistory component of B",id); end; function xsome#(BH: bufferhistory#; id: activationid): extendedhistory# = begin exit result = if size (BH) = 0 then null(extendedhistory#) else if id in BH[1].idset# then BH[1].stampedmsg# :> xsome#(nonfirst(BH),id) else xsome#(nonfirst(BH),id) fi fi; end; xinfrom(B,id) function xinfrom(B: buffertype; id: activationid): TYPES Page 7-42 7.11.2 Buffer Types extendedhistory# = begin exit result = xsome#("input history component of B",id); end; allto(B) msgs(xallto(B)) allfrom(B) msgs(xallfrom(B)) outto(B,id) msgs(xoutto(B,id)) infrom(B,id) msgs(xinfrom(B,id)) The standard functions msg, msgs, timestamp, and timestamps are defined to extract the parts of the extended history. msg(tsm) function msg(tsm:stampedmsg#):message= begin exit result = tsm.message#; end; msgs(xh) function msgs(xh:extendedhistory#):history#= begin exit result = if size(xh) = 0 then null(history#) else msg(xh[1]) :> msgs(nonfirst(xh)) fi; end; timestamp(tsm) function timestamp(tsm:stampedmsg#) :integer = begin exit result = tsm.timestamp#; end; timestamps(xh) function timestamps(xh:extendedhistory#) :sequence_of_integer = begin exit result = if size(xh) = 0 then null(sequence_of_integer) else timestamp(xh[1]) :> timestamps(nonfirst(xh)) fi; end; The basis of the proof rules for concurrency involves merging local buffer histories. Since the local history for a procedure includes the individual local histories of each of its called procedures as subsequences, we can make statements relating the parent procedure's local history and a merge of the subprocedures' local histories. This merge can be performed deterministically using the time stamps of the extended history. The following standard functions TYPES Page 7-43 7.11.2 Buffer Types provide for merging of histories. HOrdered(xh) function HOrdered(xh:extendedhistory#):boolean= begin exit result iff all i:integer, i in (1..size(xh)-1) -> timestamp(xh[i]) < timestamp(xh[i+1]); end; HMerge(H1,H2) function HMerge(H1,H2:extendedhistory#) :ExtendedHistory# = begin entry HOrdered(H1) & HOrdered(H2) & all i,j:integer, i in (1..size(H1)) & j in (1..size(H2)) -> timestamp(H1[i]) ne timestamp(H2[j]); exit H1 sub Result & H2 sub Result & size(Result) = size(H1) + size(H2) & HOrdered(Result) & all x:stampedmsg#, x in Result iff x in H1 or x in H2; end; InfromMerge(B,Ids,i,j) function InfromMerge(B:buffertype; Ids:activationidarray; i,j:integer ):extendedhistory# = begin exit result = if i > j then null(extendedhistory#) else HMerge(infrom(B,Ids[i], InfromMerge(B,Ids,i+1,j)) fi; end; OuttoMerge(B,Ids,i,j) function OuttoMerge(B:buffertype; Ids:activationidarray; i,j:integer ):extendedhistory# = begin exit result = if i > j then null(extendedhistory#) else HMerge(Outto(B,Ids[i]), OuttoMerge(B,Ids,i+1,j)) fi; end; Since the user may not declare variables of type activationid, the only way to obtain a structure of activationids is through the process of generating verification conditions for a cobegin statement. TYPES Page 7-44 7.11.2 Buffer Types Lemmas for History FunctionsM______ ___ _______ _________ Several lemmas provide the basis for use of buffer histories in program proofs. The specifications for send and receive provide definitions of buffer manipulation. (See Sections 10.2.5 and 10.2.7.) lemma BasicHistoryAxiom (B:buffertype) = allto(B) = allfrom(B) @ content(B); lemma LocalHistoryAxiom (B: buffertype; id: activationid) = infrom (B,id) sub allfrom(B) & outto (B,id) sub allto(B); Timestamps in Extended HistoriesM__________ __ ________ _________ Each message in a buffer history is tagged with a "timestamp". The purpose of the timestamp is to uniquely identify the order of actions in histories. While there is no need for this redundancy when viewing the complete allto or allfrom histories (the ordering is defined by the order in the sequence), this source of ordering information is lost when outto and infrom histories local to a particular procedure are extracted and compared. To accomplish this purpose, we posit the existence of a "clock" of sufficiently high resolution that no two distinct buffer actions would receive the same time stamp. Since mutual exclusion is enforced between between processes accessing a given buffer, there is no possibility of true simultaneity, and the order of buffer actions can always be resolved. The timestamps are integers. The following lemmas summarize our assumptions concerning the hypothetical "clock" and the concept of "time". The meaning of the numerical difference between two stamps is not defined. lemma TimeIsMonotonic1 (B:buffertype; i,j: integer) = timestamp (xallto (B) [i]) < timestamp (xallto (B) [j]) iff i < j; lemma TimeIsMonotonic2 (B:buffertype; i,j: integer) = timestamp (xallfrom (B) [i]) < timestamp (xallfrom (B) [j]) iff i < j; lemma StampsAreUnique1 (B: buffertype; i,j: integer) = timestamp (xallto (B) [i]) = timestamp (xallto (B) [j]) iff i = j; lemma StampsAreUnique2 (B: buffertype; i,j: integer) = timestamp (xallfrom(B) [i]) = timestamp (xallfrom(B) [i]) iff i = j; CHAPTER 8 ROUTINE CALLS Operations in Gypsy are performed by activations of routines. These activations are initiated by routine calls. A routine call names a routine and defines the actual parameters of the call. Each implementation of Gypsy starts the execution of a complete program (a complete set of units) by calling a special procedure named "main" whose number and type of parameters are predefined by the implementation. SyntaxM______ A consists of a routine name and actual parameters. 1. ::= --- -----------------------------------------> | | ^ | ^ | v | | | -- -- -- | | | | ----------------------------- | | | ---- ---- 1.1 Require. The must not be "main".M _______ 1.2 Define. The called routine is the routine named byM ______ ______ _______ either the or the . 1.3 Require. The number of of theM _______ must equal the number of of the called routine. 1.4 Require. If the has , then the number of of the called routine must equal the number of . The are optional even if the called routine has . 2. ::= ROUTINE CALLS Page 8-2 2.1 Require. The must begin with a . ExamplesM________ if isleaf(btree) then if tstk = emptystack then leave else num_tips := num_tips + 1; poptop(tstk,btree) unless (stack_is_empty); end; end; In the above examples, the called functions and procedures are as follows: function Emptystack : treestack = pending; function Isleaf(btree:binarytree):boolean = pending; procedure Poptop(var tstk:treestack; var btree:binarytree) unless ( cond underflow) = pending; SemanticsM_________ A initiates an activation of the routine named by either the or . The are evaluated and checked for type consistency with the corresponding formal parameters, if necessary. Also, a unique value is created for the "myid" parameter of procedures. The routine is then activated on those actual parameters. The activation of a routine may or may not terminate. The only conditions that can be signalled by an abnormal termination are condition parameters or the predefined condition "routineerror". 8.1 ACTUAL DATA PARAMETERS The actual data parameters define the actual data variables and constants that are referred to by a routine as it executes. The actual data parameters and global constants referenced by the routine form the complete data interface between a routine and its external environment. Manipulations of the data objects in the calling environment are strictly isolated to the actual data parameters that correspond to var formal parameters. Only procedures may have var parameters. ROUTINE CALLS Page 8-3 8.1 Actual data parameters SyntaxM______ The are a list of s. 1. ::= -------- , --------- | | v | ( ---- ---- ) 1.1 Define. Each is an actual data parameter.M ______ ______ ____ _________ 1.2 Define. An actual data parameter that corresponds to aM ______ formal const parameter is an actual const parameter.M ______ _____ _________ 1.3 Define. An actual data parameter that corresponds to aM ______ formal var parameter is an actual var parameter.M ______ ___ _________ 1.4 Require. The type of each actual parameter must beM _______ compatible with the type of its corresponding formal parameter. 1.5 Require. The value of each actual parameter must beM _______ potentially an element of the type of its corresponding formal parameter. 1.6 Require. Every actual var parameter must be a . 1.7 Require. An actual var parameter must not name aM _______ constant or any component of a constant. 1.8 Require. The type of a formal var parameter must beM _______ potentially a subtype of the type of its corresponding actual parameter. 1.9 Require. All actual data parameters of non-predefinedM _______ routines that are s must potentially satisfy the non-aliasing requirement. (See "Semantics", below.) SemanticsM_________ Type consistency checking of the actual and formal parameter is completed if necessary. If the value of an actual parameter is not an element of the type of its formal parameter, then a "valueerror" is signalled. This is a check on the values referred to by the actual parameters. This condition may be signalled for either a const or a var parameter. Also a "varerror" is signalled for var parameters unless the type of the formal parameter is a subtype of the actual parameter. This check involves only the types of the actual and formal parameters. It does not involve the value of the actual parameter. If either "valueerror" or "varerror" is signalled, control is transferred immediately to handle these errors; the routine is not ROUTINE CALLS Page 8-4 8.1 Actual data parameters activated. The checks for "valueerror" and "varerror" may be performed in any order. If the types of corresponding actual and formal parameters are equal, then no run-time checks are required.M _____ All actual data parameters are passed by reference. If the actual parameter is an that is also a , the name of the object named by is passed to the routine. The names either a variable or a component of a variable of a structured type. If the actual parameter is an (that is not a ), then the expression is evaluated, a new data object is created that refers to that value and the name of the new object is passed to the routine. (Note that 1.6 above requires all actual var parameters to be strictly s.) All actual data parameters that are s refer to data objects in the calling environment. All of these parameters must satisfy the following non-aliasing requirement. 2. Require. Whenever a routine is called, no change in theM _______ value of any actual var parameter may affect the value of the object referred to by any other actual data parameter. The potential satisfaction of this requirement is enforced syntactically [Section 8.1-1.9]. The parts of the requirement that cannot be shown to be satisfied syntactically are checked at run time. If the requirement is not satisfied, an "aliaserror" is signalled. The non-aliasing requirement is satisfied automatically for the actual parameters that are not s because a uniquely named object is created for each of these. This requirement is necessary because it is implicitly assumed in verifying the called routine. Note that special care must be taken to detect aliasing in parameters that are sequences. The notation s[i..j] denotes the subsequence of s from element i to element j. Suppose s[1..2] is passed as an actual var parameter and s[3] is also an actual parameter. S[1..2] can be manipulated as a sequence by the routine and therefore change in size. Any change in size may cause a redefinition of the value s[3] through the renumbering of the sequence. 8.2 ACTUAL CONDITION PARAMETERS The actual condition parameters define the conditions that are signalled if the execution caused by an activation of a routine terminates abnormally. SyntaxM______ The actual condition parameters are a list of s. The actual condition parameters are optional even if the routine declaration has formal condition parameters. ROUTINE CALLS Page 8-5 8.2 Actual Condition Parameters 1. ::= -------- , -------- | | v | unless ( ----- ----- ) 1.1 Define. Each is an actual condition parameter.M ______ ______ _________ _________ The s are optional, but if present, the number actual parameters must agree exactly with the number of formal parameters. SemanticsM_________ The execution caused by an activation of a routine may terminate by signalling a condition. The only conditions that may be signalled by an abnormal termination are condition parameters or "routineerror". (Note: "valueerror" and "varerror" are signalled before the routineM ______ is activated.) The actual condition parameters permit a condition to be renamed as it is signalled from the called routine to the calling routine. If the routine call has actual condition parameters, the actual and formal parameters are paired in the same way as the data parameters. When the called routine signals a formal condition parameter "F", the corresponding actual parameter "A" is signalled in the calling environment. If the called routine signals the formal condition "F" and the does not have actual condition parameters, then "F" itself is signalled in the calling environment. Thus, the absence of actual condition parameters is semantically equivalent to the actual condition parameters unless(F1,...,Fn) where F1,...,Fn are the names of the corresponding formal parameters. Whenever a routine terminates abnormally by signalling a condition, control is transferred immediately to a condition handler [Section 10.5]. Function calls may only appear in expressions, and the abnormal termination of a function immediately terminates evaluation of the expression. Functions do not cause side effects and therefore, the partial evaluation of an expression has no effect on any variable in the calling environment. 8.3 MAIN PROGRAM, INPUT AND OUTPUT The actual execution of a program on a particular implementation environment machine is initiated by a procedure call of the form main(a1,...,an) The actual parameters of this call are the objects that are supported by the particular implementation. The implementation defines the ROUTINE CALLS Page 8-6 8.3 Main Program, Input and Output number of formal parameters to procedure "main" and their types. The implementation binds the actual parameters to the formal parameters of "main" and initiates execution of "main(a1,...,an)". The parameters of "main" are the mechanisms by which it communicates with its external environment and is the way that a particular implementation of Gypsy provides input and output facilities. Each implementation may define its own unique set of parameters for "main". The only constraints are that the types of the parameters be expressed in Gypsy and that the actual and formal parameters of "main" satisfy the normal rules of parameter passage. An implementation may predefine certain program description units that are unique to that implementation [Section 3.6], and the types of the parameters of "main" may be expressed in terms of these predefined units. For example, an implementation may define type bytebuffer = buffer(1) of byte; where "byte" is an abstract type whose operations are routines that also are defined by the implementation. If the parameters of "main" are of type "bytebuffer", input and output of "byte" may be done through the normal Gypsy statements for manipulating buffers. CHAPTER 9 EXPRESSIONS An expression is a rule for computing a value with respect to one or more program states. The value of an expression may be computed from a value reference, a logically quantified expression, or a composition of functions. Functions do not cause side effects in the program state, and therefore, computing the value of an expression cannot cause a side effect. Expressions are designed so that they can be manipulated algebraically according to the conventional rules of mathematics (unless the expression refers to objects of shared types). 9.1 SPECIFICATION EXPRESSIONS The specification expressions are used strictly for specifications. They define boolean relations that must be satisfied on certain states in the program execution. A specification expression also expresses how the consistency of the program and boolean relation is to be verified. The consistency may be proved, validated at run-time, or simply assumed. SyntaxM______ A consists of a number of s and verification directives. 1. ::= --- --------------------------------------------> | | ^ ^ | | | | | -- otherwise -- | | | | ---- ; ------------------------------------ | | | | | | v | | -- ( ------ prove ---- -------------- ) -- | ^ | ^ | | | |_______________ | | | | -- assume -- -- otherwise -- EXPRESSIONS Page 9-2 9.1 Specification Expressions 1.1 Define. The words "prove" and "assume" are proofM ______ _____ directives.M __________ 1.2 Define. The phrase "otherwise " is a validationM ______ __________ directive.M _________ A has the same form as a except that validation directives are not allowed. 2. ::= ---- ------------------------------ | ^ | ---- ; ------------------------- | | | | | | v | | -- ( ------ prove ---- --- ) -- | ^ | | -- assume -- 3. ::= 3.1 Require. The must evaluate to a value ofM _______ type boolean. ExamplesM________ x < y ordered(A) (prove p = q; prove x < y otherwise errx; assume ordered(A)) SemanticsM_________ A defines a relation that is to be true on various states in the program execution. The relation is the conjunction of all s in the . Any one of these s may be preceded by a proof directive or followed by a validation directive. If a proof directive is not stated explicitly, the default is "prove". "Prove" directs that the consistency of the following and the program be proved. "Assume" allows the consistency to be assumed without proof. The also will be evaluated at run-time iff it is followed by a validation directive. If the evaluates to "false", the condition named is signalled and control is transferred immediately to handle the condition. If the expression evaluates to true, control proceeds normally. The groupings of s within parentheses in the allow different s to be verified in different ways. There may be more than one with a validation directive. The order in which they are evaluated are run time is not defined. EXPRESSIONS Page 9-3 9.1 Specification Expressions It is possible to direct that a be both proved and validated by using the form (prove otherwise ) If this evaluates "false" at run-time, signalling the condition , then either the proof is invalid or there is some fault in the supporting hardware or software system. Certain kinds of specifications cannot be validated at run-time. These specifications are expressed syntactically as s. Their semantics are the same as s except that run-time validation is prohibited. 9.2 SIMPLE EXPRESSIONS A simple expression is a rule for computing a value with respect to a program state. A simple expression may appear in either specifications or implementations of programs. The value of an expression is computed strictly from value references, quantified expressions, and compositions of functions. Functions may not refer to non-local variables; therefore, every variable that is used in computing the value of the expression appears in the expression explicitly. SyntaxM______ A simple is a sequence of s, s, s, and possibly a . Each operator denotes a function that is applied to actual parameters that are defined by the . An with a or a is a notation for expressing a composition of functions. The function composition and the actual parameters of the functions are defined by precedence rules. (Precedence is not associated with the rewrite rules because of the large number of precedence levels.) 1. ::= ------------------ ---------------------- | | v | -------------------------------------- ------------ | ^ | ^ | | | | ----- ----- --- --- 1.1 Define. If the contains any orM ______ , the defines a function compositionM ________ ___________ as described by the operator precedence rules. (A single function is regarded as a degenerate composition.) 1.2 Require. If the defines a functionM _______ composition, the actual parameters of the functions must EXPRESSIONS Page 9-4 9.2 Simple Expressions satisfy the normal type consistency rules of parameter passage [Section 8.1]. 1.3 Define. The type of an is the type of itsM ______ right hand side. If the defines a function composition of the form f(a1,...,an) and the type of the is the type of the result of f. ExamplesM________ num_tips-1 + tips(btree) + tipsinstack(tstk); (lobnd + hibnd) div 2 a < b i in [1..k] SemanticsM_________ An is a rule for computing a value. 2. Define The value of an is the value of its rightM ______ _____ hand side. If the defines a function composition, its value is the value of the function composition applied to its actual parameters. 3. Define. The is statically evaluatable if itM ______ __________ ___________ does not contain a , and each contained in the is statically evaluatable. Functions do not cause side effects and therefore, the values of the s that appear on the right hand side of a particular can be computed in any order. If a function in the function composition terminates abnormally by signalling a condition, the evaluation of the function composition is terminated and control is transferred immediately to the handler for the condition signalled. 9.3 OPERATORS The operators are prefix and infix notation for functions. The function composition defined by an expression is determined first by fully parenthesizing the expression according to predefined precedence rules. This defines the order of application of functions (denoted by operators) to actual parameters. Many of the operators are overloaded so the same operator may denote different functions. Which function is denoted by an operator is determined from the types of the actual parameters of the operator. The overloading is designed so that all possible functions denoted by an operator satisfy a uniform set of algebraic properties that are associated with the operator -- e.g., any function denoted by "+" is commutative and associative. EXPRESSIONS Page 9-5 9.3 Operators SyntaxM______ The operators are s and s. The s are prefix operators. The s are infix operators of two arguments. 1. ::= - | not 2. ::= ** | * | / | div | mod | + | - | @ | union | intersect | difference | and | or | -> | iff | <: | :> | omit | adjoin | ne | < | gt | lt | le | > | ge | in | sub | = | eq | append | imp | & SemanticsM_________ The semantics of an operator are the semantics of the function it denotes. 9.3.1 Function Composition The function composition defined by an expression is determined by the rules in the following table. The placement of parentheses is defined by the precedence levels. Level "1" parenthesizes most tightly. Level "1" parentheses are installed first, then level "2", and so on. All operators at the same precedence level are left associative except for ":>", which is right associative. The function call denoted by an operator is shown at the right. If an operator is overloaded (may denote several possible function calls), it denotes the one in which the actual parameters satisfy the syntactic type consistency rules of actual and formal parameters [Section 8.1]. The functions are predefined so that an operator always denotes at most one function call for any possible set of actual parameters. The predefined functions that are denoted by the operators each contain a "#" to emphasize the fact that they cannot be called directly; they may only be invoked by means of an operator. Some of the operators below are defined in terms of other operators. Operator Level DenotesM ________ _____ _______ x ** y 1 integer#power(x,y) rational#power(x,y) -x 2 integer#minus(x) rational#minus(x) x * y 3 integer#multiply(x,y) rational#multiply(x,y) EXPRESSIONS Page 9-6 9.3.1 Function Composition x / y 3 rational#number(x,y) rational#divide(x,y) x div y 3 integer#divide(x,y) x mod y 3 x - (x div y) * y x + y 4 integer#add(x,y) rational#add(x,y) x - y 4 x + (-y) x <: y 4 x @ (seq:y) x :> y 5 (seq:x) @ y (right associative) x adjoin y 5 set#adjoin(x,y) x omit y 5 set#omit(x,y) x @ y 6 sequence#append(x,y) x append y 6 x @ y x union y 6 set#union(x,y) mapping#union(x,y) x intersect y 6 set#intersect(x,y) mapping#intersect(x,y) x difference y 6 set#difference(x,y) mapping#difference(x,y) x eq y 7 S#eq(x,y) where S is a scalar type integer#eq(x,y) rational#eq(x,y) record#eq(x,y) array#eq(x,y) set#eq(x,y) sequence#eq(x,y) mapping#eq(x,y) f(x,y) where x and y are objects of a user defined abstract type, and f is the user defined equality extension for that abstract type. x = y 7 x eq y x ne y 7 not (x=y) x lt y 7 S#lt(x,y) where S is a scalar type EXPRESSIONS Page 9-7 9.3.1 Function Composition integer#lt(x,y) rational#lt(x,y) x < y 7 x lt y x le y 7 (x < y) or (x = y) x gt y 7 y lt x x > y 7 x gt y x in y 7 set#element(x,y) sequence#element(x,y) x sub y 7 set#sub(x,y) mapping#sub(x,y) sequence#sub(x,y) not x 8 boolean#not(x) x and y 9 boolean#and(x,y) x & y x or y 10 boolean#or(x,y) x -> y 11 boolean#implies(x,y) x imp y x iff y 11 boolean#eq(x,y) 9.3.2 Operator Axioms The functions denoted by an overloaded operator satisfy a uniform set of algebraic properties. An operator may exhibit additional properties that are specifically associated with a particular function that the operator denotes. These additional properties are type specific (see [Chapter 7]). Equality OperatorsM________ _________ The "eq", "=", and "ne" operators are defined on all types except shared types and on abstract types that do not have an equality extension. These operators also are not defined on any structured type that contains a shared type or an abstract type without an equality extension. The basic operator is "eq"; "=" and "ne" are defined in terms of "eq". The "eq" operator satisfies the following properties for all types T on which it is defined: lemma Reflexive(x:T) = [x eq x]; EXPRESSIONS Page 9-8 9.3.2 Operator Axioms lemma Symmetric(x,y:T) = [x eq y -> y eq x]; lemma Transitive(x,y,z:T) = [x eq y and y eq z -> x eq z]; lemma Substitution(x,y:T) = [x eq y -> f(...,x,...) eq f(...,y,...)]; for every function f that can be applied to an actual parameter of type T. Simple Relational OperatorsM______ __________ _________ The relation operators on simple types are "eq", "=", "ne", "lt", "<", "le", "gt", ">", and "ge". These operators operate on operands of scalar types and types "integer" and "rational". The fundamental operators are "=" and "lt"; the others are defined in terms of these two. Let T be any type on which "lt" is defined. lemma lt_transitive(x,y,z:bs) = (x < y) and (y < z) -> (x < z) lemma trichotomy(x,y:bs) = [(x < y) or (x = y) or (y < x)] and [x < y -> (x ne y) and not (y < x)] and [x = y -> not (x < y) and not (y < x)] and [y < x -> not (x < y) and x ne y] This second lemma states that exactly one of the relations "x lt y", "x = y", or "y lt x" is true. The remaining operators are defined by the following lemmas: lemma LeDef(x,y:T) = [x le y iff x < y or x = y]; lemma GtDef(x,y:T) = [x gt y iff y lt x]; lemma GeDef(x,y:T) = [x ge y iff x > y or x = y]; Structure Relational OperatorsM_________ __________ _________ The relational operators on structured types [structure types] are "eq", "=", "ne", "in", and "sub". The "in" and "sub" operators are used strictly with the dynamic types, (sets, sequences, and mapping). "In" is not used with mappings. Let T be a dynamic structured type with elements of type E: lemma NotInNull(x:E; T:"typename") = [not(x in null(T))]; lemma SubDef(x,y:T) = x sub y -> all u:T, u in x -> u in y lemma EqSub(x,y:T) = x sub y and y sub x iff x = y EXPRESSIONS Page 9-9 9.3.2 Operator Axioms Arithmetic OperationsM__________ __________ The arithmetic operations are "+", "-" (both unary and binary), "*", "/", and "**". These operations apply to both types "integer" and "rational". The operators "mod" and "div" apply only to type "integer". Let T be either type "integer" or "rational" and let "zero" be either "0" or "0/1" and "one" be either "1" or "1/1", depending on whether T is type "integer" or "rational", respectively. lemma AddCommutes(x,y:integer) = [(x+y) = (y+x)]; lemma AddAssociates(x,y,z:integer) = [(x+y) + z = x + (y+z)]; lemma ZeroElement(x:integer) = [x+Zero = x]; lemma AdditiveInverse(x:integer) = [x + (-x) = Zero]; lemma MultiplyCommutes(x,y:integer) = [x * y = y * x]; lemma MultipleAssociates(x,y,z:integer) = [(x*y)* z = x *(y*z)]; lemma UnityElement(x:integer) = [1 * x = x]; lemma Distribution(x,y,z:integer) = [x *(y + z) = x*y + x*z]; lemma ZeroProduct(x,y:integer) = [x*y = Zero -> (x=Zero or y=Zero)]; lemma MultiplicativeInverse (x:T) = [x*(one/x) = x]; lemma ExponentsAdd (x,a,b:T) = [x**(a+b) = (x**a)*(x**b)]; lemma ExponentOne (x:T) = [(x**one) = x]; lemma ExponentZero (x:T) = [(x**zero) = one]; Structure OperatorsM_________ _________ The structural operators that are common to several structural types are "adjoin", "omit", "union", "intersect", and "difference". These operators are used with "sets", "union", "intersect", and "difference" are also used with "mappings". Let type settype be a set with elements of type E. lemma InAdjoin (x:settype; to y,z:E) = z in x adjoin y iff z in x or z = y lemma AdjoinOmit (x:settype; y:E) = (x omit y adjoin y) = x The following relations hold for T being any "set" or "mapping" type: lemma UnionCommutes (x,y:T) = [x union y = y union x]; EXPRESSIONS Page 9-10 9.3.2 Operator Axioms lemma UnionAssociates (x,y,z:T) = [(x union y) union z = x union (y union z)]; lemma NullUnion (x:T; T:"type name") = [x union null(T) = x]; lemma DifferenceDef (x,y:T) = [(x difference y) union y = x]; lemma IntersectCommutes (x,y:T) = [x intersect y = y intersect x]; lemma IntersectAssociates (x, y, z:T) = [(x intersect y) intersect z = x intersect (y intersect z)]; lemma StructureDistribution (x,y,z:T) = [x intersect (y union z) = (x intersect y) union (x intersect z)]; lemma NullIntersection (x,y:T; T:"type name") = x = null(T) or y = null(T) -> x intersect y = null(T) The following relations hold for T being sequence of element: lemma SizeofSubseq (S:T; i,j,: integer) = size (S[i..j]) = j - i; lemma InAppend (S1,S2: T; x: element) = x in S1@S2 iff x in S1 or x in S2; lemma InSingletonSeq (x,y: element) = x in (seq:y) iff (x = y); 9.4 VALUE REFERENCES A value reference defines a value which may be the value of a constant, a variable, a function or an expression. A value reference also may be a component of a value of a structured type, or it may be the value of a structured type with certain components assigned new values or removed. SyntaxM______ A may be a , a , a , a , a , an in parentheses, an , or a . Each of these may optionally be followed by a compatible sequence of intermixed s and s. EXPRESSIONS Page 9-11 9.4 Value References 1. ::= --- ---------------------------------------------- | | |-- ----------------------------------------------------- | ^ | ^ | | | | |-- -----------------------------| |<--------------------| | | ^ | | | | -- -- | |- -| | | | | |----- -------------------| - - | | |------ ( ) -----------------| | | | | ------ -------------------- | | -------- ----------- 1.1 Define. A that contains either a or an defines a structuralM __________ function composition as described below.M ________ ___________ 1.2 Define. The type of a depends on the form ofM ______ ____ its right hand side. If the form is then the type of the is the type of the . In all other cases, the type of is the type of its right hand side. 1.3 Define. A can be evaluated statically if itM ______ _________ __________ is a , a whose value can be determined statically, a statically evaluatable , a staticaly evaluatable , or a statically evaluatable . A that defines a structural function composition has the form VREF CLAUSE1 ... CLAUSEn for some n>0 where each CLAUSEi is either a or an . CLAUSE1 and each CLAUSEi define either a selection function composition or an alteration function composition with respect to a given subject [Sections 9.4.1 and 9.4.2]. The structural composition defined by these clauses is defined recursively according to the following table: Form CompositionM ____ ___________ VREF CLAUSE1 The composition defined by CLAUSE1 on the subject VREF VREF CLAUSE1...CLAUSEn SC CLAUSE2...CLAUSEn where SC is EXPRESSIONS Page 9-12 9.4 Value References the structural composition defined by VREF CLAUSE1. SemanticsM_________ A defines a value that depends on the form of its right hand side. Form ValueM ____ _____ The value of . The value of constant named . The value of the variable named in the current program state. The value of the variable in the program state that existed when execution of the routine in which the appears was initiated. The value of the result returned by the function call. () The value of . The value of . The value of the structural function The value of the structural function composition composition (either alteration clause or selector clause). 9.4.1 Selector Clauses And Lists A particular component of a value of a structured type may be selected by the use of a selector clause or a selector list which is a list of selector clauses. SyntaxM______ A is a sequence of s. A is composed of a of a record or a number of s 1. ::= EXPRESSIONS Page 9-13 9.4.1 Selector Clauses and Lists --------------------------- | | v | --------- --------- 1.1 Define. The selector sequence of a isM ______ ________ ________ the concatenation of the selector sequence of each individual . 1.2 Define. The selection function composition of aM ______ _________ ________ ___________ is defined by its subject and its selector sequence, as described below. 1.3 Require. The selector sequence of a mustM _______ be structurally compatible [Section 9.4.1-4] with its subject. 2. ::= --- . -------------------------------------------- | ^ | --------------------- , --------------------- | | | | | | v | | -- ( ---- ------------------------------ ) -- | ^ | | --- .. --- 2.1 Define. The selector sequence of a isM ______ ________ ________ defined as follows depending on the form of the right hand side. Form Selector SequenceM ____ ________ ________ . . () () () (..) (S1,...,Sn) PQ where P is the selector sequence of S1 and Q is the selector sequence of (S2,...,Sn). 2.2 Define. The selection function composition of aM ______ is defined from its selector sequence as described below. 2.3 Require. The selector sequence of a M _______ must be structurally compatible [Section 9.4.1-4] with its subject. EXPRESSIONS Page 9-14 9.4.1 Selector Clauses and Lists 3. ::= 3.1 Require. The must have a record field.M _______ A selector sequence always appears in conjunction with a subject x x S1 ... Sn for some n>0 and where each Si is selector of the one of the forms ".", "(expression)", or "(..)". A selector sequence defines a composition of selector functions on its subject. The selector function denoted by a particular selector is determined by the type of the subject and the form of the selector, as shown in the following table. Form DenotesM ____ _______ x.y record#select (x,y) x(y) array#select (x,y) sequence#select (x,y) mapping#select (x,y) x(y..z) sequence#subselect (x,y.z) x S1 ... Sn (P) X2 ... Sn where P is the function call denoted by "x S1". (The selector functions given in the table are defined in [7.0].) The selector form "(y)" is overloaded and the function call it denotes is determined from the type of its subject x. 4. Define. A selector Si is structurally compatible with itsM ______ ____________ __________ subject x iff it and its subject conform to one of the rules in the preceding table and if the actual parameters of the function call determined from the table satisfy the normal rules of parameter passage [Section 8.1]. 5. Define. A selector sequence is structurally compatible withM ______ ____________ __________ its subject iff every individual selector in the sequence is structurally compatible with its individual subject. Under these rules, ".y" can be applied only to records, "(y)" to arrays, sequences, and mappings, and "(y..z)" only to sequences. Also the forms "(S1, ..., Sn)" and "(S1)...(Sn)" define the same selector function composition, therefore, the forms are equivalent. ExamplesM________ [i][j].k[l] EXPRESSIONS Page 9-15 9.4.1 Selector Clauses and Lists [i,j] .k[i,j] SemanticsM_________ The semantics of a and a are strictly the semantics of the structural function composition that they define. 9.4.2 Alteration Clauses A value of a structured type often is described most conveniently as an existing value with certain components changed or deleted. These kinds of values can be described by an alteration clause that follows a value of a structured type. SyntaxM______ An consists of a sequence of s and s. This sequence defines an alteration function composition. 1. ::= --- ; <------------------------------------------- | | v | with ( ------------------------ --- ) --- | ^ | ^ | | | | -- -- -- --- 1.1 Define The alteration function composition is defined byM ______ __________ ________ ___________ the subject of an and its alteration sequence as described below. 1.2 Define. Each or is called an alteration descriptor.M __________ __________ 1.3 Require The alteration sequence must be structurallyM _______ compatible [Section 9.4.2-5] with the subject of the . 2. ::= EXPRESSIONS Page 9-16 9.4.2 Alteration Clauses ----------------------- ----- := | ^ | | |--- before ---| | | ---- behind ---- 3. ::= ------- seqomit ------- ------------ | ^ | | ---- mapomit ---- 4. ::= each : , 4.1 Define. The is the bound identifier of theM ______ . It is a local name of the unit name scope andM _____ ____ defines a constant name. The type of the bound identifier isM ________ ____ ____ the type defined by . 4.2 Require. The type defined by must not beM _______ rational. The alteration function composition defined by an with subject x is defined recursively according to the following table. Form CompositionM ____ ___________ x with (.f:=y) Record#ComponentAssign(x,f,y) x with ((i):=y) Array#ComponentAssign(x,i,y) Sequence#ComponentAssign(x,i,y) Mapping#ComponentAssign(x,i,y) x with ((i..j):=y) Sequence#SubAssign(x,i,j,y) x with (before (i):=y) Sequence#Put#Before(x,i,y) x with (behind(i):=y) Sequence#Put#Before(x,i+1,y) x with (seqomit (i)) Sequence#Delete(x,i) x with (mapomit (i)) Mapping#Delete(x,i) x with (s1...sn:=y) x with [s1:=(x s1)with(s2...sn:=y)] where s1...sn is the where (x s1) denotes the structural selector sequence function composition denoted by "x s1". defined by the x with (prefix s1...sn:=y) x with [s1:=(x s1) with (prefix s2...sn:=y)] where prefix is "before" where (x s1) denotes the structural or "behind" and s1...sn function composition denoted by "x s1". is the selector sequence EXPRESSIONS Page 9-17 9.4.2 Alteration Clauses defined by the x with (prefix s1...sn) x with [s1:=(x s1) with (prefix s2...sn)] where prefix is "seqomit" where (x s1) denotes the structural or "mapomit" and s1...sn is function composition denoted by "x s1". the selector sequence defined by the x with (each k:[a...b],D) if a>b then x; otherwise (x with (Da)) with (each k:[succ(a)..b],D), where Da is D with each occurrence of the bound identifier k replaced by a. D is either a or a . x with (D1;...;Dn) (x with D1) with (D2;...;Dn) (The functions given in the table are defined in [7.0].) The alteration form "with ((i):=y)" is overloaded and the function call it denotes is determined from the type of its subject x. 5. Define An is structurally compatible withM ______ ____________ __________ its subject iff every individual alteration descriptor is structurally compatible with its individual subject. ExamplesM________ with (.user1 := user1id; .user2 := user2id; .cstring := text) with (each i: [1..max], [i] := [i+1]) with (before [i] := x; behind [j] := y) SemanticsM_________ The semantics of an are strictly the semantics of its alteration function composition. The overloaded forms of the and are defined so that they satisfy the following lemmas: lemma Select with(x:Tx;i,j:TI;y:TE) = [x with [(i):=y](i)] = [if i=j then y else x(j) fi] where type TX = array (TI) of TE, or type TX = sequence ... of TE and TI is of type integer, or type TX = mapping ... from TI to TE. EXPRESSIONS Page 9-18 9.4.2 Alteration Clauses lemma Record with(R:record type; x:field type) = R with (.f1:=x) .f2 = R.f2 and R with (.f1:=x) .f1 = x; where field type is the corresponding to the field f1 in record type. lemma Mapping withOmit(M:maptype; x,y:domaintype) = x ne y -> M with (mapomit [x])(y) = M[y]; lemma Sequence withOmit(S:seqtype; i,j:integer) = S with (seqomit [i]) [j] = if j < i then s[j] else s[j+1] fi; lemma Sequence withomitsubseq(s:seqtype; i,j,k:integer) = S with (SeqOmit [i..j]) [k] = if k < i then s[k] else s [k + j - i + 1] fi; lemma Sequence withSubAssign(s1:seqtype1; s3:seqtype2; i,j,k:integer) = S1 with ([i..j] := s2) [k] = if k < i then s[k] else if k < i + size(s2) then s2[k-i+1] else s1[k - size(s2) + j - i + 1] fi fi; lemma Sequence makefirst(s:seqtype; x:element) = S with ([0] := x) = S with (before [1] := x); lemma Sequence makelast(s : seq type; x : element) = S with ([size (s) + 1] := x) = S with (behind [size(s)] := x); lemma Sequence insertedbefore(s:seq type; x:element; i,j:integer) = S with (before [i] := x) [j] = if j=i then x else if j < i then s[j] else s [j - 1] fi fi; lemma Sequence insertedbehind(s:seq type; x:element; i,j:integer) = S with (behind [i] := x) [j] = if j = i + 1 then x else if j < i + 1 then s[j] else s[j - 1] fi fi; These axioms specify how to select an element from an altered sequence value. Subsequence selection is defined in terms of element selection from the extracted subsequence; hence, subsequence selection from an altered sequence value is also defined. 9.5 IF EXPRESSIONS An computes a value from one of two values, depending on the value of a boolean expression. SyntaxM______ EXPRESSIONS Page 9-19 9.5 If Expressions An consists of a and two other type compatible s. 1. ::= if then else fi 1.1 Require. The two s must be type compatibleM _______ [Section 7.2-9]. 1.2 Define. The type of is the base type ofM ______ ____ the (which is the same as the base type of ). 1.3 Define. The can be statically evaluatedM ______ __________ _________ if the can be statically evaluated, and the or which must be evaluated (as defined by the semantics) is also statically evaluatable. ExamplesM________ if x < y then x + y else f(z) fi SemanticsM_________ The value of an depends on the value of its . 2. Define. The value of an is the value of theM ______ _____ if the evaluates "true"; if the evaluates to "false, then the value of the is the value of . The that is not needed to define the value of the is not evaluated.M ___ 9.6 QUANTIFIED EXPRESSIONS A quantified expression is either a universal or existential quantification and gives a value of type "boolean". SyntaxM______ A begins with "all" or "some" and has a bound , a , and a . 1. ::= EXPRESSIONS Page 9-20 9.6 Quantified Expressions -------- , ------- | | v | ---- all --- --- : , | ^ | | -- some -- 1.1 Define. The is the bound identifier of theM ______ _____ __________ . 1.2 Define. The bound identifier is a local name of the unitM ______ _____ ____ name scope. (Uniqueness among bound identifiers in a unit name scope is not required.) 1.3 Require. The may not contain anotherM _______ with the same bound identifier. 1.4 Define. The type of is boolean.M ______ ____ 1.5 Define. The initial keyword ("all" or "some") is calledM ______ the quantifier.M __________ 1.6 Require. If the is nested withinM _______ another , and the is a subrange, then the range restriction of the may not contain references to the bound identifiers of any enclosing . ExampleM_______ all x: integer[a..b], x > y some m:message, hello(m) SemanticsM_________ The is evaluated for each binding of the bound identifier to a value in the value set [Chapter 7] V of the type defined by the . 2. Define. If the quantifier is "all", the value of theM ______ _____ quantified expression> is "true" if V is empty or the evaluates "true" for all bindings of the bound identifier to elements of V; if the value of the is "false" for some binding of the bound identifier to an element of V, the evaluates to "false". 3. Define. If the quantifier is "some", the value of theM ______ _____ quantified expression> is "true" if there is at least one binding of the bound identifier to an element of V such that the evaluates "true"; the value of the is "false" if V is empty or the evaluates to "false" for all bindings of the EXPRESSIONS Page 9-21 9.6 Quantified Expressions bound variable to an element of V. The is always evaluated for every binding of the boundM ______ variable to an element in V. (There is not "short circuit" evaluation.) The order in which the bound identifier assumes values from V is undefined. 9.7 SET AND SEQUENCE CONSTRUCTORS It is often convenient in programs and specifications to use set or sequence constants. The provides a convenient means for constructing sets and sequences from constant expressions. SyntaxM______ 1. ::= --------- , ------------------------ | | v | -- ( ------ set: ----------- ---------------------- ) -- | ^ | ^ | | | | |----- seq: --------| |- .. -| | ^ | | | | | , | | | | | | --- --------------------- 1.1 Define. If the keyword "set" begins the , then the result is a set value; otherwise it is a sequence value. 1.2 Require. Neither in a phrase of the formM _______ .. may be of type rational. 1.3 Require. If a phrase ..M _______ appears in the , it is an abbreviation for: , [succ().. ], with such expansion continued until an empty interval is reached. 1.4 Define. The sequence of that appears inM ______ the expanded is called the constructorM ___________ list.M ____ EXPRESSIONS Page 9-22 9.7 Set and Sequence Constructors 1.5 Require. Each must be type compatibleM _______ with . 1.6 Define. The element type of the value of the is basetype#(). 1.7 Define. The is staticallyM ______ __________ evaluatable if each expression appearing in the sequence isM ___________ statically evaluatable. ExamplesM________ (set: red, blue, green) (seq: 2..10, 1..10) (1..10) (x+2, y div 3, z * 4) SemanticsM_________ The defines a value V such that in V for each appearing in the constructor list. If V is a sequence value, then V[i] = and size(V) = n, where n is the length of the constructor list. If V is a set value, then the set V consists of exactly those elements x of values#(element type) for which some evaluates to x in the current program state. CHAPTER 10 STATEMENT LISTS Statement lists are sequences of statements and internal assert specifications. Assert specifications are relations that are to hold whenever control reaches that point in the statement list. Each statement in a statement list defines an operation or defines the order in which operations are performed. The procedural statements define procedure calls, the sequential control statements define the order in which sequential operations are performed, and the concurrent control statements define operations that are performed concurrently. Exception handlers for specifically named conditions can be placed at the end of any statement that ends with the reserved word "end". SyntaxM______ A is a sequence of s and s. 1. ::= --------------------------------------------> | ^ | ^ | | | | |---------- pending ---------| -- ; -- | ^ v | |<------------ ; ------------- | ^ |------- --------| | | --- --- 1.1 Define. The internal specifications of a are s that are contained in the or within any that also may contain a . 2. ::= | | STATEMENT LISTS Page 10-2 SemanticsM_________ The s of a are executed in order unless specified otherwise by a or a . The semantics of the individual s are described in the following sections. The s each have a single entry, single exit control structure. Control enters only at the beginning of a statement and leaves only through the end. The blockage of a is defined in terms of its component s. 3. Define. A is blocked iff one of itsM ______ _______ s is blocked. The s that can be blocked are described in the following sections. 10.1 ASSERT SPECIFICATION An assert specification defines a relation that is to hold at that point in a statement list. It is an internal specification of instantaneous extent. SyntaxM______ An is a . 1. ::= assert ExamplesM________ assert m = amin(a,1,i) assert (prove m = amin(a,1,i); assume i < n otherwise indexfault) SemanticsM_________ The relation defined by the must be true whenever control reaches the . The s in a are used as the bases for implicit inductions in proofs by inductive assertions. A proof normally will require that every possible loop in a routine contain at least one . STATEMENT LISTS Page 10-3 PROCEDURAL STATEMENTS 10.2 PROCEDURAL STATEMENTS The procedural statements define procedure calls. The procedure called may be a predefined procedure or a procedure defined by a procedure declaration. The calls of predefined procedures are written in a syntactic notation that is different from a procedure call. This notation is an aid to readability; the effects of these statements are equivalent to procedure calls. SyntaxM______ The s are s, s, s, s,s, s, and s. 1. ::= | | | | | | SemanticsM_________ The semantics of a are the semantics of its right hand side. 10.2.1 Procedure Call Statement A procedure call statement activates an execution of a procedure. The execution may terminate normally or abnormally, or it may not terminate. SyntaxM______ 1. ::= 1.1 Require. The must be a procedure call.M _______ SemanticsM_________ The semantics of procedure calls are described in [Section 8.0]. STATEMENT LISTS Page 10-4 10.2.1 Procedure Call Statement 2. Define. A is blocked iff itsM ______ _______ called procedure is blocked. 10.2.2 Assignment Statement An assignment statement binds a value to a variable. SyntaxM______ An consists of a and an . 1. ::= := 1.1 Define. An defines an assignmentM ______ __________ procedure call as described below.M _________ ____ 1.2 Require. An assignment procedure must exist for theM _______ (see below). 1.3 Require. The assignment procedure call and its actualM _______ parameters must satisfy all of the normal syntax rules. 2. ::= --- ---------------------------------------> | ^ | | -- before ----- ------ | ^ | | -- behind -- 3. ::= --------------------------- | ^ | | --- --- 4. ::= ExamplesM________ x := y a[i,j] := if i = j then 1 else 0 fi before a.f[i] := g(x,y,z) STATEMENT LISTS Page 10-5 10.2.2 Assignment Statement SemanticsM_________ The ":=" is an overloaded operator that denotes a procedure call that depends on the form of the and on the types of the operands of the ":=" operator. First, the is converted, if necessary, into the form ":=" by converting the form PREFIX := where PREFIX is either empty, "before", or "behind" into the form := with (PREFIX := ) The assignment procedure is defined on this converted form. 5. Define. The assignment procedure call of an is: S#assign#T(x,y) where x:=y is the converted assignment statement, S is the base type, and T is the type of x. Assignment procedures exist for all base types except activationids and buffers. If S is an abstract type, the assignment procedure for its concrete representation is used. Each assignment procedure has the specification procedure S#assign#T(var v:T; e:T) = begin exit v = e; end so that a "valueerror" will be signalled if v is not in the value set of type T. This keeps the value of variable x in the value set of its type T. The only requirement of an implementation of ":=" is that these specifications of the assignment procedure call be met. These specifications allow assignments to components of variables of structured types -- e.g., a[i] := b+c -- to be made efficiently in the usual way; it is not necessary for the converted form of ":=" to make a copy of " with (PREFIX := )". Notice that the assignment statement may change the number of components in the value of a variable of a dynamic type, as in s := a @ b or s[i..j] := r[p..q] or s := null(seq) STATEMENT LISTS Page 10-6 10.2.2 Assignment Statement where s and r are variables of type sequence. 10.2.3 Remove Statements A remove statement deletes one or more components of a set, sequence, or mapping. SyntaxM______ A consists of a . 1. ::= remove 1.1 Require. The is functionallyM _______ equivalent to an assignment statement as described below. That assignment statement must satisfy all of the normal syntax rules. 2. ::= | from 3. ::= 4. ::= ExamplesM________ remove m[j][i+4] remove s[i..j] remove m.f[i,j,k] remove f(x) from setvar SemanticsM_________ A deletes one or more components of a dynamic structure and is functionally equivalent to an assignment statement that depends on the form of the . If the has the form then the equivalent assignment statement is either := with (seqomit ) or := with (mapomit ) depending upon the type of selector function composition defined by the of the . If the STATEMENT LISTS Page 10-7 10.2.3 Remove Statements has the form from then the equivalent assignment statement is := omit The need not be implemented as the assignment statement given above. The effect of this assignment can be obtained efficiently by an implementation using pointers. 10.2.4 Move Statements A move statement moves elements from one set, sequence, or mapping to another set, sequence, or mapping. SyntaxM______ A consists of a and either a or a . 1. ::= move --- to --- | ^ | | ---- into ---- 1.1 Require. The is functionally equivalentM _______ to a sequence of statements as described below, and must meet the normal syntax requirements of these statements. 2. ::= ExamplesM________ move s[i] to r[j] move a.m[j+1] to behind m[i] move e from s.f into setvar move s[i] into setvar move x from setvar to before s[k+j] SemanticsM_________ The moves components from one dynamic structure to another. It is functionally equivalent to an assignment and a remove statement, depending on its form. The form move to STATEMENT LISTS Page 10-8 10.2.4 Move Statements is equivalent to := ; remove The form move from to is equivalent to := ; remove from The form move into is equivalent to := adjoin ; remove The form move from into is equivalent to := adjoin ; remove from The need not be implemented as its two equivalent statements. The effect of the move can be implemented efficiently using pointers. 10.2.5 Send Statement A send statement enqueues a value to a buffer. SyntaxM______ A consists of an and a . 1. ::= send to 1.1 Require. The is equivalent to aM _______ procedure call as described below. Actual parameters of this call must satisfy all of the normal syntax rules. STATEMENT LISTS Page 10-9 10.2.5 Send Statement 2. ::= ExampleM_______ send m to b send f(x) to b[i] SemanticsM_________ The enqueues the value of to the buffer referred to by . The effects of the are equivalent to the procedure call buffer#send#A(, , myid) where A is the type of the and procedure buffer#send#T(x:E; var B:T; a:activationid) unless(senderror) = begin block full(B); exit case (is normal: outto(B,a) = outto(B',a) <: X and infrom(B,a) = infrom(B',a); is senderror: outto(B,a) = outto(B',a) and infrom(B,a) = infrom(B',a)); end; and where type T = buffer ... of E. If the buffer B is not full, the buffer#send procedure is executed at some time when no other buffer#send or buffer#receive is being executed on buffer B. Once execution of the buffer#send is initiated on B, no other buffer#send or buffer#receive call may be initiated on B until the buffer#send that is executing terminates. If buffer B is full, execution of the routine that called the buffer#send is blocked until the buffer becomes not full. 3. Define. A is blocked iffM ______ _______ full(). 10.2.6 Give Statement A give statement enqueues a component of a dynamic structure to a buffer and removes the component from the structure. STATEMENT LISTS Page 10-10 10.2.6 Give Statement SyntaxM______ A consists of and a . 1. ::= give to 1.1 Require. A is functionally equivalentM _______ to a sequence of statements described below, and must meet the normal syntax requirements of these statements. ExamplesM________ give m[i] to b give s[j..k] to port.away SemanticsM_________ The effects of a are functionally equivalent to a send and a remove statement, depending on the form of the . The form give to is equivalent to send to ; remove The form give from to is equivalent to send from to ; remove from The need not be implemented as its two equivalent statements. The semantics of the give permit efficient implementation using pointers. 2. Define. A is blocked iff its equivalentM ______ _______ send statement is blocked. STATEMENT LISTS Page 10-11 10.2.6 Give Statement 10.2.7 Receive Statement A receive statement dequeues a value from a buffer and assigns it to a variable. SyntaxM______ A consists of a and a . 1. ::= receive from 1.1 Require. A is functionallyM _______ equivalent to a procedure call as described below. The actual parameters of this call must satisfy all of the normal syntax rules. ExamplesM________ receive m from b receive a[i] from port[j] SemanticsM_________ The effects of a are equivalent to the procedure call buffer#receive#BT(, , myid); where #BT is the type of and procedure buffer#receive#T(var x:E; var B:T; a:activationid) unless(receiveerror) = begin block empty(B); exit case (is normal: infrom(B,a) = infrom(B',a) <: E and outto(B,a) = outto(B',a); is receiveerror: infrom(B,a) = infrom(B',a) and outto(B,a) = outto(B',a)); end; and where type T = buffer... of E. If the buffer B is not empty, the buffer#receive is performed at some time when no other buffer#send or buffer#receive is being executed on the buffer. Once execution of a buffer#receive call on buffer B begins, no other buffer#send or buffer#receive call may be initiated until the buffer#receive that is executing terminates. If buffer B is empty, execution of the routine that called the buffer#receive is STATEMENT LISTS Page 10-12 10.2.7 Receive Statement blocked until the buffer becomes not empty. 1. Define. A is blocked iff empty(). 10.3 SEQUENTIAL CONTROL STATEMENTS The sequential control statements define control flow that alters the normal sequential flow through a statement list. There are two branching statements, if and case, one loop statement that is terminated by a leave statement, and a signal statement that signals a condition. A sequential control statement may be blocked if it contains a statement list. 1. ::= | | | | | 2. Define. Any is blocked iff itM ______ contains a that is blocked. 10.3.1 If Statements An if statement defines one or more alternative statement lists that may be executed. SyntaxM______ An consists of s and s. 1. ::= if then ----- | v |<----------------------------------------------- | ^ | | |-- elif then -->| | |-------------------------------------- | ^ STATEMENT LISTS Page 10-13 10.3.1 If Statements | | ----- else ------ ExamplesM________ if a and b then x := y end if i = n then send m to b[0] else send m to c[i] end if opa(x) then doa(x,y) elif opb(x) then dob(x,y) elif opc(x) then doc(x,y) end SemanticsM_________ The most general form of an is if then elif then ... elif then else ; The control through an depends on the values of the s. The s are evaluated in order 1,2,..,n until the first one, say , evaluates "true". Control is then transferred to the corresponding . If control then reaches the end of , it continues at whatever follows the . If none of the s evaluates to "true", then control is transferred to the following the "else" if there is one; otherwise, control is transferred to whatever follows the . If control reaches the end of , it continues at whatever follows the . If a condition is signalled within any and not handled, control is transferred immediately to the . 10.3.2 Case Statements A case statement defines a multi-way branch based on the value of an expression. The outcome of the case statement is well defined for every possible value of the expression. SyntaxM______ A consists of a number of s that are labelled by case labels. STATEMENT LISTS Page 10-14 10.3.2 Case Statements 1. ::= case -- |<------------------------------------------------- | | | ---------- , ---------- | | | | | | v | | |- is -- -- : - | ^ | |------ -----| | | | | |---- - -----| | | | | |---- -----| | | | | ----- ----- | | |<------------------------------------------------| | |--- else : ---- | | |<------------------------------- | --- 1.1 Require. The type of the must be a simpleM _______ type S or a subrange of a simple type S. 1.2 Define. Each , , -,M ______ and is a case label.M ____ _____ 1.3 Require. Every case label must be an element of type S.M _______ 1.4 Require. Every case label must have a unique value.M _______ 1.5 Require. Any used as a label must evaluateM _______ statically to a constant value of some simple type. 2. ::= 2.1 Require. The must name a constant of aM _______ scalar type. ExamplesM________ case carcolor is red, blue: count := count+1; else: count := 0; end; STATEMENT LISTS Page 10-15 10.3.2 Case Statements SemanticsM_________ The control through a depends on the value of the . If the value of is one of the case labels, control flows to the immediately following that case label. If control reaches the end of the , it goes next to whatever follows the . If the value of is not one of the case labels, control flows to the following the "else" if there is one; otherwise a "caseerror" is signalled and control is transferred to the of the . If control reaches the end of , it goes next to whatever follows the . If a condition is signalled within any and not handled, control is transferred immediately to the . 10.3.3 Loop Statements A loop statement defines the repeated execution of a statement list. The repeated execution is terminated by executing a leave statement in the statement list. SyntaxM______ A consists of a single . 1. ::= loop ExamplesM________ loop if i > n then leave s := s+a[i]; i := i+1 end SemanticsM_________ A loop statement defines an indefinite and possibly infinite number of repeated executions of its . Control is first transferred to the . If control reaches the end of the , control is transferred back to the beginning of the . This repeated execution can be terminated only by executing a or signalling a condition from within the . If a is executed, control is transferred immediately to whatever follows the . If a condition is signalled and not handled within the , control is transferred immediately to the . (Once control is transferred to the , the repeated execution of the terminates.) STATEMENT LISTS Page 10-16 10.3.3 Loop Statements If an of the form if then leave end is the first statement in the , the behaves as a conventional "while" statement (as in Pascal). If the is the last statement in the list, the loop behaves as a "repeat" statement. If the is some statement other than the first or last, the loop behaves as a "loop and a half". Any number (including zero) of s may be placed in a loop for internal control. If there are no s, the loop does not terminate. 10.3.4 Begin Statements A begin statement is a statement list. Its only purpose is to associate condition handlers with a statement list. Syntax M______ A consists of a . 1. ::= begin ExampleM_______ begin x := a[i]; when is indexerror: x := 0; end SemanticsM_________ Control begins with the . If control reaches the end of the , it goes next to whatever follows the . If a condition is signalled and not handled within the , control is transferred immediately to the . 10.3.5 Leave Statement A leave statement terminates the repeated execution of the statement list of a loop statement. SyntaxM______ 1. ::= leave STATEMENT LISTS Page 10-17 10.3.5 Leave Statement 1.1 Require. A may appear only in theM _______ of a . SemanticsM_________ Executing a causes control to be transferred to whatever follows the most recently entered . 10.3.6 Signal Statement A signal statement signals a condition. SyntaxM______ 1. ::= signal ExamplesM________ signal badinput; SemanticsM_________ A signals the condition and causes control to be transferred immediately to the of the most recently entered that has an . The condition is handled as described in [Section 10.5]. 10.4 CONCURRENT CONTROL STATEMENTS The two concurrent control statements initiate concurrent execution of several processes. Both statements have a strictly single entry, single exit control structure. SyntaxM______ A is a or an . 1. ::= | SemanticsM_________ The semantics of a are the semantics of its right side. STATEMENT LISTS Page 10-18 10.4 Concurrent Control Statements 10.4.1 Cobegin Statement The cobegin statement initiates concurrent execution of several procedures. SyntaxM______ A consists of several s that are procedure calls. 1. ::= -> cobegin -- |<--------------- ; ------------------ | | |-- -- | | | | |<------------------ | | | ----- --------- | ^ | | -- ; -- 1.1 Define. If an precedes a ,M ______ one is defined for each possible value of the bound identifier of the . 1.2 Define. A completely buffered type is a buffer type or aM ______ __________ ________ structured type each of whose components is a completely buffered type. 1.3 Require. Only s of a completely bufferedM _______ type can appear as actual var parameters of more than one routine call. 1.4 Require. The non-aliasing requirement [Section 8.1-2]M _______ applies to all actual var parameters of all within the cobegin, except as allowed by [1.3]. ExamplesM________ cobegin transport(x,b); transport(b,y); end cobegin each i:[1..n], transport(x[i],b); each j:[1..m], transport(b,y[j]); end SemanticsM_________ STATEMENT LISTS Page 10-19 10.4.1 Cobegin Statement A transfers control to each of its procedure calls and these calls are executed concurrently. (The routine that executed the is not executed concurrently with the procedure calls of the .) If all procedure calls of the terminate normally, then control goes next to whatever follows the . If all procedure calls terminate and some terminate abnormally, then, when all have terminated, control is transferred to the of the . This may lead to a situation in which the of an may be entered with several conditions signalled simultaneously. Control flows from the only if all procedure calls terminate. If a is blocked, the block specification of the routine in which the appears must hold. 2. Define. A is blocked iff all of itsM ______ _______ procedure calls that have not terminated are blocked. 10.4.2 Await Statements An await statement is similar to a non-deterministic case statement in which the "case label"s are buffer statements. SyntaxM______ An consists of a number of " then " pairs. 1. ::= await - |<----------------------------------------------- | | |-- -- | | | | |<------------------ | | | -- on then --- 2. ::= | | ExamplesM________ await each i:[1..n], on receive x from b[i] then send x to queue; STATEMENT LISTS Page 10-20 10.4.2 Await Statements end SemanticsM_________ An defines a number of "on then " segments. If an appears before an "on", it defines one segment for each possible value of its bound identifier. Upon entering an , control pauses until at least one of the s is not blocked. At that point, one of the unblocked s is selected nondeterministically. The statement selected is performed and control is transferred to the that follows it. If control reaches the end of the , it goes next to whatever follows the . If a condition is signalled and not handled within either , control is transferred immediately to the . 3. Define. An is blocked iff all of itsM ______ _______ are blocked. 10.5 CONDITION HANDLING Condition handling may be performed at the end of any structured statement or at the end of a routine. The condition handlers are expressed in the general form of a case statement where the "case labels" are conditions. The condition handling is defined so that the conditions that can be signalled across routine boundaries are very limited and do not inadvertently reveal information about the implementation of a routine. Conditions and signal statements are a very restricted form of labels and gotos. Within a routine, the handler for any given condition signalled always can be determined statically. SyntaxM______ Condition handling is done in s. An may have a which has the form similar to a case statement. 1. ::= end | end 2. ::= STATEMENT LISTS Page 10-21 10.5 Condition Handling -- when -- | |<---------------------------------------------- | | | --- , <-------- | | v | | |--- is --- --- : --- | |--- else: --- | | |<----------------------------- | ExamplesM________ begin s.p := s.p + 1; s.a[s.p] := x; when is indexerror: signal stackoverflow; end loop s := s + a[i]; i := i + 1; when is indexerror: ; end SemanticsM_________ When a condition "c" is signalled, control is transferred immediately to the of the most tightly enclosing or that has an . Condition "c" is handled by that if it can be, and control continues normally from whatever follows the . If condition "c" cannot be handled by that , control is transferred to the of the next most tightly enclosing statement that has an . A condition "c" is handled by an iff "c" appears as an in a or if the appears at the end of a . If "c" appears as an in the , then the condition is handled by transferring control to the that immediately follows the . If control reaches the end of either or , it continues at whatever follows the . If "c" does not appear as an and the has an "else", the condition is handled by transferring control to the that follows the "else". If "c" does not appear as an in the and the does not have an "else" and the appears as the of a , then the condition is handled by signalling the predefined condition "routineerror". A cobegin may terminate signalling several conditions simultaneously. This is referred to as a multiple condition. AM ________ _________ multiple condition can only be handled by the "else" of a or by signalling a "routineerror" in the usual way. Under these rules, every condition that is signalled with a routine is handled within that routine. Conditions may cross routine boundaries only as condition parameters or as "routineerrors". Thus, an abnormal termination of a routine cannot inadvertently reveal information about the implementation of the routine. CHAPTER 11 REFERENCES REFERENCES Page 11-2 REFERENCES [Ambler, 76] A. Ambler, D.I. Good, W.F. Burger. "Report on the Language Gypsy", The University of Texas at Austin, ICSCA-CMP-1 (August, 1976). [Brinch Hansen, 73] Per Brinch Hansen. "Operating Systems Principles", Prentice-Hall, 1973. [Brinch Hansen, 75] Per Brinch Hansen. "The Purpose of Concurrent Pascal", Proceedings ICRS, 1975.M ___________ ____ [Dahl, 66] O.J. Dahl and K. Nygaard. "SIMULA - An ALGOL-Based Simulation Language", CACM 9-9, September, 1966.M ____ [Jensen, 74] K. Jensen and N. Wirth. Pascal User Manual and Report,M ______ ____ ______ ___ ______ Springer Verlag, 1974. [Good, 73] D.I. Good and L.C. Ragland. "Nucleus--A Language for Provable Programs", Program Test Methods, Hetzel, ed.,M _______ ____ _______ Prentice-Hall, 1973. [Good, 77-2a] D.I. Good. "Constructing Verified and Reliable Communications Processing Systems", ACM Software Engineering Notes, 2-5, October, 1977. [Hoare, 72-2] C.A.R. Hoare, O.J. Dahl, E. W. Dijkstra. "Notes on Data Structuring", Structured Programming, Academic Press, 1972.M __________ ___________ [Lampson, 76] B.W. Lampson, J.J. Horning, R.L. London, J.G. Mitchell, G.J. Popek. "Report on the Programming Language Euclid", Xerox Research Center, August, 1976. [Liskov, 76] B.H. Liskov. "An Introduction to CLU", CSG Memo 136, MIT Laboratory for Computer Science, February, 1976. [Naur, 63] "Report on the Algorithmic Language ALGOL 60", P. Naur, ed., CACM 6,1, 1963. [Roubine, 76] O. Roubine and L. Robinson. "SPECIAL Reference Manual", Stanford Research Institute, August, 1976. [van Wijngaarden, 68] A. van Wijngaarden. "Report on the Algorithmic Language ALGOL 68", Numerische Mathematik 14, 1969.M __________ __________ __ [Wulf, 77] W.A. Wulf, R.L. London, M. Shaw. "Abstraction and Verification in Alphard: Defining and Specifying Iteration and Generators", CACM 20,8 August, 1977. APPENDIX A GYPSY REWRITE RULES [4.6-2] ::= | |-- entry -- -- ; -- | | |<--------------------------------------------- | |-- block -- -- ; --- | | |<--------------------------------------------- | |-- exit -- -- ; --- | | ^ | | -------- ---------- | | | |<--------------------------------------------- | [7.4-1] ::= begin : ; end [8.2-1] ::= -------- , -------- | | v | unless ( ----- ----- ) GYPSY REWRITE RULES Page A-2 [8.1-1] ::= -------- , --------- | | v | ( ---- ---- ) [9.4.2-1] ::= --- ; <------------------------------------------- | | v | with ( ------------------------ --- ) --- | ^ | ^ | | | | -- -- -- --- [7.9.2-1] ::= array ( ) of [2.2.1-2] ::= # any ASCII character # [10.1-1] ::= assert [10.2.2.1] ::= := [10.4.2-1] ::= await - |<----------------------------------------------- | | |-- -- | | | | |<------------------ | | | -- on then --- [10.3.4-1] ::= begin [9.3-2] ::= ** | * | / | div | mod | + | - | @ | union | intersect | difference | and | or | -> | iff | <: | :> | omit | adjoin | ne | < | gt | lt | le | > | ge | in | sub | = | eq | append | imp | & [9.1-3] ::= GYPSY REWRITE RULES Page A-3 [7.11.2-2] ::= -- < ---- input ---- > --- | ^ | | -- output --- [10.4.2-2] ::= | | [7.11.2-1] ::= buffer ------------------------------> of | | | | -- ( ) --- [10.2.5-2] ::= [10.3.2-1] ::= case -- |<------------------------------------------------- | | | ---------- , ---------- | | | | | | v | | |- is -- -- : - | ^ | |------ -----| | | | | |---- - -----| | | | | |---- -----| | | | | ----- ----- | | |<------------------------------------------------| | |--- else : ---- | | |<------------------------------- | --- GYPSY REWRITE RULES Page A-4 [10.4.1-1] ::= -> cobegin -- |<--------------- ; ------------------ | | |-- -- | | | | |<------------------ | | | ----- --------- | ^ | | -- ; -- [2.3-1] ::= | [9.4.2-2] ::= ----------------------- ----- := | ^ | | |--- before ---| | | ---- behind ---- [9.4.2-3] ::= ------- seqomit ------- ------------ | ^ | | ---- mapomit ---- GYPSY REWRITE RULES Page A-5 [4.6-3] ::= | |- centry -- -- ; -- | | |<--------------------------------------------- | |- cblock -- -- ; --- | | |<--------------------------------------------- | |- cexit -- -- ; --- | | ^ | | | | | | --------- ---------- | | | |<--------------------------------------------- | [10.4-1] ::= | [4.7-3] ::= --- , <---------------------- | | v | --- cond ------------ ------------------ [4.4-2] ::= [5.0-1] ::= const -- --- : = --- --- | | ^ | | | | --- pending ---->| | | -------- = ------------- [4.3-4] ::= [2.3-2] ::= --- --- | | v | ----> { ---------------------------------> } ------> GYPSY REWRITE RULES Page A-6 [2.0-6] ::= 0|1|2|3|4|5|6|7|8|9 [2.2.2-3] ::= --- --- | | v | --- ($ ------------------------------- $) --- | ^ | | ------ $$ ----- [10.2.3-2] ::= | from [4.6-1] ::= | |--- ---- | |<------------------------------------------ | |--- ---- | |<------------------------------------------ | [9.4.2-4] ::= each : , [10.5-1] ::= end | end [4.6-4] ::= ----- ; <--------------------------------------------------- | | | --- , <----------- | | | | | v v | | case ( -- is --- ------- : -- --- ) | ^ | | ----- normal : ----- ----- GYPSY REWRITE RULES Page A-7 [9.2-1] ::= ------------------ ---------------------- | | v | -------------------------------------- ------------ | ^ | ^ | | | | ----- ----- --- --- [9.4.1-3] ::= [4.4-1] ::= --- , <------------ | | v | ---- unless -- ( ---------------- ---- ) ----- | ^ | | --- cond --- [8.0-2] ::= [4.3-2] ::= -- ; <------------------------------------------- | | | -- , <------------ | | | | | v v | | --- ( ---------------- --- : ----- ) --- | ^ -- const --- GYPSY REWRITE RULES Page A-8 [4.2-1] ::= ----- function ------ | ---------------------------------- | |---- extends ---------- | | |<------------------------------- | |-- -- | | |<------------------------------- | ----- : -------------- | --------------------------------- | |--- --- | | |<------------------------------- | [4.2-2] ::= [10.2.6-1] ::= give to [7.4-2] ::= hold ---------------> | ^ | | ---- ; ---- [2.1-1] ::= -------------------------------------- | | v | ---> --------------------------> ---------> | | ^ | ^ ^ | |<----------| | | | | | | | | | | -- -- --- ---- | | | -------------------------------------------- GYPSY REWRITE RULES Page A-9 [9.5-1] ::= if then else fi [10.3.1-1] ::= if then ------ | v |<----------------------------------------------- | ^ | | |-- elif then -->| | |-------------------------------------- | ^ | | ----- else ------ [7.3-3] ::= initially -- ( ----------------- --- ) ------ | ^ |- prove ---| | | -- assume --- [10.3.5-1] ::= leave [6.0-3] ::= [6.0-1] ::= = [6.0-2] ::= lemma ---------------------------------------- | ^ | | --- --- [2.0-3] ::= | [2.2-1] ::= | | GYPSY REWRITE RULES Page A-10 [4.7-1] ::= | | [10.3.3-1] ::= loop [2.0-4] ::= # any lower case ASCII letter a..z # [7.10.2-1] ::= mapping -- | |-- () -- | | |<---------------------- | -- from to [10.2.4-1] ::= move --- to --- | ^ | | -- into ------- [3.3-1] ::= ---------------- , ----------------- | | v | name ---------------------- --------> from | ^ | | -- = -- [7.10.1-2] ::= GYPSY REWRITE RULES Page A-11 [9.1-2] ::= ---- ------------------------------ | ^ | ---- ; ------------------------- | | | | | | v | | -- ( ------ prove ---- --- ) -- | ^ | | -- assume -- [2.2.3-1] ::= ------------------- | | v | ---------> ------------> [10.2.2-2] ::= --- ---------------------------------------> | ^ | | -- before ----- ------ | ^ | | -- behind -- [2.2.1-4] ::= '|$ [2.2.1-1] ::= [10.2-1] ::= | | | | | | [10.2.1-1] ::= GYPSY REWRITE RULES Page A-12 [4.3-1] ::= -- ; <------------------------------------------- | | | -- , <------------ | | | | | v v | | --- ( ---------------- --- : --- ) --- | ^ |- const ->| | | |- var --->| [4.1-1] ::= ----- procedure ----- | |-- -- | |---- --- | | |<-------------------------------- | [4.1-2] ::= [3.0-1] ::= ---- ; <------------------------------------------ | | v | --------------------------> ----------> | ^ | ^ | | | | - -- -- ; -- [9.6.1] ::= --- , ------------ | | v | ---- all ---- --- : , | ^ | | -- some -- [2.2.2-2] ::= --- --- | | v | GYPSY REWRITE RULES Page A-13 ---- " ------------------------------- " ---- | ^ | | ------ "" ----- [7.6-2] ::= ( .. ) [10.2.7-1] ::= receive from [7.9.1-1] ::= ----------------------------------- ; --------------- | | | -------- , ------- | | | | | v v | | -- record ( ------ ---- : ----------- ) [10.2.3-1] ::= remove [4.5-1] ::= -- begin -- | |-- -- | |<-------------------------------------- | |<------------------------------ | | |---- ; ---- | |-- keep ; -- | | |<--------------------------------------- | |--- --- | |<----------------------- | ---------- GYPSY REWRITE RULES Page A-14 [8.0-1] ::= --- -----------------------------------------> | | ^ | ^ | v | | | -- -- -- | | | | ----------------------------- | | | ---- ---- [4.0-1] ::= --- = --- --- | | ---- ----- [4.0-2] ::= | [10.3.2-2] ::= [7.7.1-1] ::= --------- , -------- | | v | -- ( ---- ----- ) -- [3.4-1] ::= ------- , ------- | | v | --- < ---- ---- > --- [3.1-3] ::= ----- ; <----------------------------------------- | | v | begin -------------------------> ------------ end -> | ^ ^ | ^ | | | | | |- - | -- ; -- | | --------------- ------------ [3.1-4] ::= GYPSY REWRITE RULES Page A-15 [3.1-1] ::= = [3.1-2] ::= scope [2.1-2] ::= _ [9.4.1-2] ::= --- . -------------------------------------------- | ^ | --------------------- , --------------------- | | | | | | v | | -- ( ---- ------------------------------ ) -- | ^ | | --- .. --- [9.4.1-1] ::= --------------------------- | | v | --------- ------- [10.2.5-1] ::= send to [10.2.4-2] ::= [10.2.3-3] ::= [10.2.2-4] ::= [7.10.3-1] ::= sequence -------------------------- of ---> | ^ | | -- ( ) -- GYPSY REWRITE RULES Page A-16 [10.3-1] ::= | | | | | [7.10.1-1] ::= set --------------------------- of | ^ | | -- ( ) -- [10.2.3-4] ::= [9.7-1] ::= --------- , ------------------------ | | v | -- ( ------ set: ----------- ---------------------- ) -- | ^ | ^ | | | | |----- seq: --------| |- .. -| | ^ | | | | | , | | | | | | --- --------------------- [7.5-2] ::= [10.3.6-1] ::= signal [7.9.2-2] ::= GYPSY REWRITE RULES Page A-17 [9.1-1] ::= --- --------------------------------------------> | | ^ ^ | | | | | -- otherwise -- | | | | ---- ; ------------------------------------ | | | | | | v | | -- ( ------ prove ---- -------------- ) -- | ^ | ^ | | | |_______________ | | | | -- assume -- -- otherwise -- [2.3-3] ::= --- --- | | v | ---- (* ------------------------------ *) ---- [10.0-2] ::= | | [10.0-1] ::= --------------------------------------------> | ^ | ^ | | | | |---------- pending ---------| -- ; -- | ^ v | |<------------ ; ------------- | ^ |------- --------| | | --- --- [2.2.2-1] ::= | [7.8-1] ::= | | | | GYPSY REWRITE RULES Page A-18 [7.3-4] ::= pending | | [7.3-1] ::= = [7.5-1] ::= ------ -------------------------------------------- | | ^ | --- := ------>| | | |-- ----------------------------------------| | | |-- -----------------------------------| | | --- ---------------------------------------- [7.3-2] ::= type -- | | |-- -- | | |<---------------------------- | |--- ------ | | |<---------------------------- | [7.3-5] ::= [7.6-1] ::= --- --------------------------------------- | | ^ | |------ ----| | | | ---------------|----------- ------------- [9.3-1] ::= - | not GYPSY REWRITE RULES Page A-19 [3.4-2] ::= ----------- , ---------- | | v | < --------- --------- > | ^ | | ----- ----- [3.2-1] ::= | | | [3.2-2] ::= [2.0-] ::= # any upper case ASCII letter A..Z # [9.4-1] ::= --- ---------------------------------------------- | | |-- ----------------------------------------------------- | ^ | ^ | | | | |-- -----------------------------| |<--------------------| | | ^ | | | | -- -- | |- -| | | | | |----- -------------------| - - | | |------ ( ) -----------------| | | | | ------ -------------------- | | -------- ----------- GYPSY REWRITE RULES Page A-20 [4.7-2] ::= -- , <----------- | | v | var --- --- : --------------------------- | | ^ | | | | -- := ----->| | | | | --- pending ---->| | | ------- := ---------------- [4.3-3] ::= [10.2.2-3] ::= --------------------------- | ^ | | --- --- [10.5-2] ::= -- when -- | |<---------------------------------------------- | | | --- , <-------- | | v | | |--- is --- --- : --- | |--- else: --- | | |<----------------------------- | APPENDIX B CROSS REFERENCE OF NONTERMINAL SYMBOLS Nonterminal Symbols Referenced byM ___________ _______ __________ __ , , , , , , , , CROSS REFERENCE OF NONTERMINAL SYMBOLS Page B-2 , , , , , , , , , , , , , , , , , , , , , , , , CROSS REFERENCE OF NONTERMINAL SYMBOLS Page B-3 , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , CROSS REFERENCE OF NONTERMINAL SYMBOLS Page B-4 , , , , , , , , , , , , , , CROSS REFERENCE OF NONTERMINAL SYMBOLS Page B-5 , , , , , , , , , CROSS REFERENCE OF NONTERMINAL SYMBOLS Page B-6 , , , , , , , , , , , , , , , , , , , , , , , , , , , CROSS REFERENCE OF NONTERMINAL SYMBOLS Page B-7 , , , , , , , APPENDIX C CROSS REFERENCE OF RESERVED WORDS Reserved Word Referenced byM________ ____ __________ __ adjoin all and array append assert assume , , await before , begin , , , behind , block buffer case , cblock centry cexit CROSS REFERENCE OF RESERVED WORDS Page C-2 cobegin cond , const , , difference div each elif else , , , end , , entry eq exit extends fi from , , , function ge give gt hold if , iff imp in initially input intersect CROSS REFERENCE OF RESERVED WORDS Page C-3 into is , , keep le leave lemma loop lt mapomit mapping mod move name ne normal not of , , , omit on or otherwise output pending , , , , procedure prove , , receive CROSS REFERENCE OF RESERVED WORDS Page C-4 record remove scope send seq seqomit sequence set , signal some sub then , , to , , , type union unless , var , when with APPENDIX D PREDEFINED IDENTIFIERS AND STANDARD FUNCTIONS Every Gypsy program is contained within a predefined scope. This scope defines certain identifiers that may be used in the Gypsy program. Predefined types: activationid, boolean character, integer, rational Predefined scalar constants: true, false Standard functions: allfrom [section 7.11.2] allto [section 7.11.2] content [section 7.11.2] domain [section 7.10.2] empty [section 7.11.2] first [section 7.10.3] full [section 7.11.2] Hordered [section 7.11.2] HMerge [section 7.11.2] infrom [section 7.11.2] InfromMerge [section 7.11.2] initial [section 7.3] last [section 7.10.3] lower [section 7.7.1] max [section 7.7] min [section 7.7] msg [section 7.11.2] msgs [section 7.11.2] nonfirst [section 7.10.3] nonlast [section 7.10.3] null [section 7.10] ord [section 7.7.1] outto [section 7.11.2] OuttoMerge [section 7.11.2] pred [section 7.7.1 and 7.7.4] range [section 7.10.2] scale [section 7.7.1] size [section 7.10] PREDEFINED IDENTIFIERS AND STANDARD FUNCTIONS Page D-2 succ [section 7.7.1 and 7.7.4] timestamp [section 7.11.2] timestamps [section 7.11.2] upper [section 7.7.1] xallfrom [section 7.11.2] xallto [section 7.11.2] xinfrom [section 7.11.2] xoutto [section 7.11.2] Standard conditions: Standard condition names are defined as formal cond parameters. These condition names are not reserved, but, if defined in a user routine, may be used as implicit actual cond parameters in place of an omitted actual cond parameter. (See [section 8.2].) adderror [section 7.7.4 and 7.7.5] aliaserror [section 8.1] caseerror [section 10.3.2] divideerror [section 7.7.4 and 7.7.5] indexerror [section 7.8] membererror [section 7.10] minuserror [section 7.7.6] multiplyerror [section 7.7.4 and 7.7.5] negativeexponent [section 7.7.4 and 7.7.5] nonunique [section 7.10.2] nopred [section 7.7.1 and 7.7.4] nosucc [section 7.7.1 and 7.7.4] overscale [section 7.7.1] powererror [section 7.7.4 and 7.7.5] powerindeterminant [section 7.7.4 and 7.7.5] receiveerror [section 10.2.7] routineerror [section 10.5] senderror [section 10.2.5] spaceerror [section 7.10] suberror [section 7.10] subtracterror [section 7.7.6] underscale [section 7.7.1] valueerror [section 8.1] varerror [section 8.1] APPENDIX E PROGRAM EXAMPLES As a Specification Language I. Binary Search (Specification only) SCOPE B_SEARCH = begin {C o n s t a n t s} const K: integer = pending; {F u n c t i o n s} function Bsearch(a: smallarray; lobnd: bounds; hibnd: bounds; item: integer) : bounds unless (cond notfound) = begin entry ordered(a); exit case (is normal: a[bsearch(a, lobnd, hibnd, item)] = item; is notfound: notthere(a, lobnd, hibnd, item)); end; function Ordered(a: smallarray) : boolean = begin exit (assume all x, y:bounds, x < y -> a[x] < a[y]); end; PROGRAM EXAMPLES Page E-2 Specification Examples function Notthere(a: smallarray; x, y: bounds; n: integer) : boolean = begin exit (assume notthere(a, x, y, n) iff (all i: bounds, i in [x..y] -> a[i] ne n)); end; {T y p e s} type Bounds = integer[1..k]; type Smallarray = array[bounds] of integer; end; {scope bsearch} PROGRAM EXAMPLES Page E-3 Specification Examples II. Register Module (Specifications only) { Register module adapted from Neumann [1975] as an example of Parnas' style module specification in Gypsy. } SCOPE REGISTER_MODULE = begin {T y p e s} type Register = pending; type Charnum = integer[0..255]; {V - F u n c t i o n s} function RLength (r:register) : integer = pending; { Purpose: returns RLength of register r } function Char (r:register; i:integer) : charnum = begin { Purpose: returns the character in place i of register r } entry i in [1..RLength(r)]; pending; end; {O - F u n c t i o n s} procedure Insert (var r:register; i:integer; c:charnum) = begin entry i in [0..RLength(r)] and RLength(r) < 1000; exit (all j:integer, char(r,j) = if j le i then char(r',j) else if j = i then c else char(r',j-1) fi fi) and RLength(r) = RLength(r') + 1; pending; end; procedure Delete (var r:register; i:integer) = begin { Purpose: deletes the ith character of register r } entry i in [1..RLength(r)]; exit (all j:integer, char(r,j) = if j < i then char(r',j) else char(r',j-1) fi) and RLength(r) = RLength(r') - 1; pending; end; end { scope Register_Module } ; PROGRAM EXAMPLES Page E-4 Specification Examples III. Block Structured Symbol Table (Specifications only) { Example of axiomatic definition of a block structured symbol table, adapted from Guttag, Horowitz and Musser (1976) } SCOPE SYMBOL_TABLE_SPECS = begin {T y p e s} type Symtab = pending; type Identifier = pending; type Attributelist = pending; {S y n t a x o f F u n c t i o n s} function Init : symtab = pending; {Note: this function has no parameters. } function Enter_Block (s:symtab) : symtab = pending; function Add_Id (s:symtab; id:identifier; attrlist:attributelist) : symtab = pending; function Leave_Block (s:symtab) : symtab = pending; function Is_In_Block (s:symtab; id:identifier) : boolean = pending; function Retreive (s:symtab; id:identifier) : attributelist unless (cond Undefined_Id) = pending; function Eq_Symtab extends "=" (s1,s2:symtab): boolean = pending; {F u n c t i o n S e m a n t i c s} lemma S1 = Leave_Block(Init) = Init; lemma S2 (s:symtab) = Leave_Block(Enter_Block(s)) = s; lemma S3 (s:symtab;id:identifier; attrlist:attributelist) = Leave_Block(Add_Id(s,id,attrlist)) = Leave_Block(s); lemma S4 (id:identifier) = Is_In_Block(Init,id) = false; lemma S5 (s:symtab; id:identifier) = Is_In_Block(Enter_Block(s),id) = false; PROGRAM EXAMPLES Page E-5 Specification Examples lemma S6 (s:symtab; id,id1:identifier; attrlist:attributelist) = Is_In_Block(Add_Id(s,id,attrlist),id1) = if id = id1 then true else Is_In_Block(s,id1) fi; { We now add an entry condition to the function Retrieve which corresponds to their axiom 7. The entry condition will be run-time validated, and act as a guard for the partial function.} function Retrieve (s:symtab; id:identifier) : attributelist unless (cond Undefined_Id) = begin entry (assume s ne Init otherwise Undefined_Id); pending; end; Lemma S8 (s:symtab; id:identifier) = Retrieve(Enter_Block(s),id) = Retrieve(s,id); lemma S9 (s:symtab; id,id1:identifier; attrlist:attributelist) = Retrieve(Add_Id(s,id,attrlist),id1) = if id = id1 then attrlist else Retrieve(s,id1) fi; end { scope Symbol_Table_Specs } ; PROGRAM EXAMPLES Page E-6 Use as Programming Language Use as Programming Language I. Priority Queue (Program code only) { A Prioroity Queue. } SCOPE PRIORITY_QUEUE = begin { C o n s t a n t s } const Max_Q_Size : integer = pending; const Null_Item : item_type = pending; { T y p e s } type Queue = begin q: cqueue; { default initialization for sequence types is the empty sequence. } hold ordered_q(q); end; type cqueue = sequence(max_q_size) of queue_element; type Queue_Element = record (priority:integer; item:item_type); { Type single_element is used as a temporary for the use in the MOVE statement. Elements may be MOVEd between these one element sequences and the priority queue without copying.} type Single_Element = sequence [1] of queue_element; type Item_Type = pending; { F u n c t i o n s } function Ordered_Q (q: CQueue) : boolean = begin cexit (assume ordered_q(q) iff all i:integer[1..max_q_size], i < size(q) -> q[i].priority ge q[i+1].priority); end; PROGRAM EXAMPLES Page E-7 Use as Programming Language { P r o c e d u r e s } procedure Insert (var q: Queue; var e:single_element) unless (cond q_overflow) = begin centry size(q) < max_q_size otherwise q_overflow; var i:integer[1..max_q_size] := 1; cond insert_before, indexerror; loop if q[i].priority < e[1].priority then signal insert_before; end; i := i + 1; when is indexerror, insert_before: { insert before queue element i } move e[1] to before q[i]; end; end; procedure Get_Next(var q:Queue; var e:single_element) unless (cond empty_queue) = begin centry size(q) > 0 otherwise empty_queue; move q[1] to e[1]; end; procedure Delete (var q:Queue; e:single_element) unless (cond not_found) = begin var i:integer[1..max_q_size] := 1; cond indexerror; loop if q[i] = e[1] then remove q[i]; leave; end; when is indexerror: signal not_found; end; end; end; { scope Priority_Queue } PROGRAM EXAMPLES Page E-8 Use as Programming Language III. Shared Table (Program code only) SCOPE TABLE_SHARING = begin { This is an example of the memory management features of Gypsy. There are two concurrent processes sharing a single copy of a table. The GIVE statement is used to assure mutual exclusion, and avoid the overhead of copying the shared table. Access lists are used to control actual manipulation of the abstract table structure. {T y p e s} type Table = pending; type message = pending; type message_Buf = buffer of message; type Table_Buf = buffer (1) of table; type Box = sequence (1) of table; {F u n c t i o n s} function Init_Table : box = pending; { a parameterless function } function Requires_Mod (m:message) : boolean = pending; function Form_Answer (m:message; t:table) : message = pending; {P r o c e d u r e s} procedure Main (var messagesin, messagesout:message_buf) = begin var t:box := Init_table; var shared_table:table_buf; give t[1] to shared_table; cobegin Table_User(messagesin, messagesout, shared_table); Table_User(messagesin, messagesout, shared_table); end; end; PROGRAM EXAMPLES Page E-9 Use as Programming Language procedure Table_User (var messagesin, messagesout:message_buf; var shared_table:table_buf) = begin var request, reply:message; var t:box; loop receive request from messagesin; receive t[1] from shared_table; reply := Form_Answer(request,t[1]); if Requires_Mod(reply) then Modify(t,request,reply) end; give t[1] to shared_table; send reply to messagesout; end; end; procedure Modify (var t:box; request,reply:message) = pending; end {scope Table_Sharing } ; PROGRAM EXAMPLES Page E-10 Use as Program Description Language Use as Program Description Language I. Count Tips (Full Program Description) SCOPE STACK_PROCEDURES = begin {C o n s t a n t s} const Stack_Limit = 100; {F u n c t i o n s} function Emptystack : treestack = pending; function Isfull(tstk:treestack):boolean = pending; function Pop(tstk:treestack):treestack = begin entry tstk ne emptystack; end; function Push(tstk:treestack; btree:binarytree):treestack = begin entry not isfull(tstk); end; function Top(tstk:treestack):binarytree = begin entry tstk ne emptystack; end; function tstack_eq extends "="(x,y: treestack): boolean = begin cexit result iff x.p = y.p and (all j: integer, j in [1..x.p] -> x.a(j) = y.a(j) ); end; {L e m m a s} lemma Treestack_Req(tstk: treestack; btree: binarytree) = top(push(tstk,btree)) = btree and pop(push(tstk,btree)) = tstk and push(tstk,btree) ne emptystack; {P r o c e d u r e s} procedure Poptop(var tstk:treestack; var btree:binarytree) PROGRAM EXAMPLES Page E-11 Use as Program Description Language unless (cond underflow) = begin exit case (is normal: tstk = pop(tstk') and btree = top(tstk'); is underflow: tstk' = emptystack); cexit case (is normal: tstk = tstk' with(.p := tstk'.p - 1) and btree = tstk'.a[tstk'.p]; is underflow: tstk'.p = 0); end; procedure Pushon(var tstk:treestack; btree:binarytree) unless (cond overflow) = begin exit case (is normal: tstk = push(tstk',btree); is overflow: isfull(tstk')); cexit case (is normal: tstk.a = tstk'.a with ([tstk'.p + 1] := btree) and tstk.p = tstk'.p + 1; is overflow: tstk'.p = stack_limit); pending; end; {T y p e s} name Binarytree from tree_abstraction; name bitree_eq from tree_abstraction; type Treestack = record (a: array ([1..stack_limit]) of binarytree; p: integer[0..stack_limit] := 0); end; {scope stack_procedures} SCOPE TIPCOUNT_PROCEDURES = begin {F u n c t i o n s} name Emptystack from stack_procedures; name tstack_eq from stack_procedures; name Isleaf from tree_abstraction; name Leftson from tree_abstraction; name Pop from stack_procedures; name Rightson from tree_abstraction; function Tips(btree:binarytree):integer = begin exit (assume PROGRAM EXAMPLES Page E-12 Use as Program Description Language tips(btree) = if isleaf(btree) then 1 else tips(leftson(btree)) + tips(rightson(btree)) fi); end; function Tipsinstack(tstk:treestack):integer = begin exit (assume result = if tstk = emptystack then 0 else tipsinstack(pop(tstk)) + tips(top(tstk)) fi); end; name Top from stack_procedures; function Undercount(num_tips:integer; btree:binarytree):boolean = begin exit (assume undercount(num_tips,btree) iff num_tips le tips(btree)); end; {P r o c e d u r e s} name Poptop from stack_procedures; name Pushon from stack_procedures; procedure Tipcount(var num_tips:integer; b_tree:binarytree) unless (cond bigtree) = begin exit case (is normal: num_tips = tips(b_tree); is bigtree: undercount(num_tips,b_tree)); var tstk:treestack := emptystack; var btree: binarytree := b_tree; cond stack_is_empty,stack_is_full; num_tips := 1; loop assert tips(b_tree) = num_tips - 1 + tips(btree) + tipsinstack(tstk); if isleaf(btree) then if tstk = emptystack then leave else num_tips := num_tips + 1; poptop(tstk,btree) unless (stack_is_empty); end; else pushon(tstk,rightson(btree)) unless (stack_is_full); btree := leftson(btree); end; when is stack_is_full: num_tips := num_tips + stack_limit + 2; signal bigtree; end; when is stack_is_empty: assert false; { This assertion says "We should never get here!" } end; PROGRAM EXAMPLES Page E-13 Use as Program Description Language {T y p e s} name Binarytree from tree_abstraction; name Stack_Limit from stack_procedures; name Treestack from stack_procedures; end; {scope tipcount_procedures} SCOPE TREE_ABSTRACTION = begin {F u n c t i o n s} name Emptystack from stack_procedures; function Isleaf(btree:binarytree):boolean = pending; function Leftson(btree:binarytree):binarytree = pending; function Rightson(btree:binarytree):binarytree = pending; function bitree_eq extends "=" (x,y: binarytree): boolean = pending; {T y p e s} type Binarytree = pending; name Treestack from stack_procedures; end; {scope tree_abstraction} PROGRAM EXAMPLES Page E-14 Use as Program Description Language II. Frequency Count (Full Program Description) SCOPE FREQ_COUNT = begin {F u n c t i o n s} function Frequency_Count(x_seq:seq_of_x):FreqTable = begin exit (assume all x:xobj, [frequency_count(null (seq_of_x)) = nulltable] and [lookup(x,frequency_count(x_seq))=occurrences(x,x_seq)]); end; function Include(x:xobj; ftab:FreqTable):FreqTable = begin exit (assume some x_seq:seq_of_x, ftab=frequency_count(x_seq) -> include(x,ftab)=frequency_count(x_seq <: x)); end; name Inithash from hash_abstraction; name Lookup from hashing_procedures; function Nulltable: FreqTable = begin exit all x:xobj, lookup(x,nulltable) = 0; result := initHash end; function Occurrences(x:xobj; x_seq:seq_of_x):integer = begin exit (assume occurrences(x,x_seq) = if x_seq = null (seq_of_x) then 0 else if x=first(x_seq) then 1+occurrences(x,nonfirst(x_seq)) else occurrences(x,nonfirst(x_seq)) fi fi); end; function Under_Count(ftab:freqtable; x_seq:seq_of_x): boolean = begin exit (assume all x:xobj, x in x_seq -> lookup(x, ftab) le occurrences(x, x_seq)); end; PROGRAM EXAMPLES Page E-15 Use as Program Description Language {P r o c e d u r e s} procedure Compute_Freq_Table(var ftab:FreqTable; xseq:seq_of_x) unless (cond table_overflow) = begin exit case( is normal: ftab = frequency_count(xseq); is table_overflow: under_count(ftab,xseq)); cond count_err; var x_seq: seq_of_x := xseq; ftab := nulltable; loop assert some r:seq_of_x, r @ x_seq = xseq and ftab = frequency_count(r); if x_seq = null (seq_of_x) then leave else count_x(first(x_seq),ftab) unless (count_err); x_seq := nonfirst(x_seq); end; when is count_err: signal table_overflow; end; end; procedure Count_X(x:xobj; var ftab:FreqTable) unless ( cond cant) = begin exit case( is normal: ftab = include(x,ftab'); is cant: ftab=ftab'); insert (x,ftab, lookup (x,ftab) + 1) unless ( cant) end; name Insert from hashing_procedures; {T y p e s} type FreqTable initially (Nulltable) = HashTable; name hash_eq from hash_abstraction; name Hashtable from hash_abstraction; type Seq_of_X = sequence(100) of xobj; type Xobj = integer {for example}; end; {scope freq_count} PROGRAM EXAMPLES Page E-16 Use as Program Description Language III. Hash Table (Full Program Description) { This is the hash table abstraction used by the Frequency Count example just preceeding. } SCOPE HASH_ABSTRACTION = begin {C o n s t a n t s} const Table_Size: integer = pending; {F u n c t i o n s} function All_Reachable (htab: HashTable) : boolean = begin cexit (assume all i:bounds, htab[i].flag = used -> no_fresh(htab,htab[i].key,i)); end; function All_Unique (htab: HashTable) : boolean = begin cexit (assume all lo,hi: bounds, all_unique (htab) iff ((htab(lo).flag=used and htab(hi).flag=used and (lo ne hi)) -> (htab(lo).key ne htab(hi).key))); end; name Cyclic_Path from hashing_procedures; function Hash(item: xobj): bounds = pending; function In_Table (key: xobj; table: HashTable ): boolean = begin exit in_table(key,table) iff (lookup(key,table) ne 0); result := lookup (key, table) ne 0 end; function Index_Of (htab: HashTable; key: xobj): bounds = begin centry some i: bounds, is_entry(htab(i), key); cexit (assume some i: bounds, index_of(htab, key) = i); end; function InitHash: HashTable = begin cexit all j: bounds, initHash(j).flag=fresh; var i: bounds:=1; loop result(i).flag:=fresh; assert all j:bounds, j le i -> result(j).flag = fresh; if i=Table_Size then leave end; i:=i+1 end; end; PROGRAM EXAMPLES Page E-17 Use as Program Description Language name Initscan from hashing_procedures; function Is_Entry (hentry: HashEntry; key: xobj): boolean = begin exit (assume is_entry (hentry,key) iff (hentry.key=key and hentry.flag=used)); end; name Lookup from hashing_procedures; function No_Entry(table: HashTable; key: xobj; index: bounds):boolean= begin cexit (assume all i: bounds, i in cyclic_path (val(initscan(key)), index) -> not is_entry(table(i), key)); end; function No_Fresh (htab: HashTable; key: xobj; stop: bounds):boolean = begin cexit (assume no_fresh(htab,key,stop) iff all i: bounds, (i in Cyclic_path(val(initScan(key)), stop) -> htab(i).flag ne fresh)); end; function hash_eq extends "="(x,y: hashtable): boolean = begin exit result iff all k: xobj, lookup(k,x) = lookup(k,y); end; name Val from hashing_procedures; {T y p e s} type Bounds = integer (1..Table_Size); type HashEntry = record (flag: HashFlags; key: xobj; count: integer); type HashFlags = (fresh,used,deleted); name insert,delete from hashing_procedures; type HashTable = begin htab: array(bounds) of HashEntry; hold all key: xobj, all_unique(htab) and (some i: bounds, is_entry(htab(i), key) -> no_fresh(htab, key, index_of(htab, key))); end; PROGRAM EXAMPLES Page E-18 Use as Program Description Language name Xobj from freq_count; end; {scope hash_abstraction} SCOPE HASHING_PROCEDURES= begin {C o n s t a n t s} name Table_Size from hash_abstraction; {F u n c t i o n s} function Cyclic_Path (lo, hi: bounds): boundseq = begin exit (assume Cyclic_path (lo, hi) = if lo=hi then [seq:lo] else lo :> Cyclic_path(next(lo), hi) fi); end; name Hash from hash_abstraction; name In_Table from hash_abstraction; function InitScan(item: xobj): CyclicScan = begin cexit result = initial(cyclicscan) with (.value := hash(item); .start := hash(item) ); result.value := hash(item); result.start := hash(item); end; name Is_Entry from hash_abstraction; function Lookup(key: xobj; table: HashTable): integer = begin cexit some j: bounds, if is_entry(table(j), key) then lookup(key,table) = table[j].count else lookup(key,table)=0 fi; var cscan: CyclicScan:=initScan(key); result:=0; loop case table(val(cscan)).flag is fresh: leave; is deleted: ; is used: if table(val(cscan)).key=key then result:=table(val(cscan)).count; leave end; end; assert no_fresh (table, key, val(cscan)) PROGRAM EXAMPLES Page E-19 Use as Program Description Language and no_entry (table, key, val(cscan)); step_scan(cscan); if stop(cscan) then leave end; end; assert if is_entry (table(val(cscan)), key) then table(val(cscan)).count=result else not no_fresh(table, key, val(cscan)) and no_entry(table, key, val(cscan)) fi; end; function Next(i:bounds): bounds = begin { linear rehash } exit (assume next(i) = ((i + 1) mod Table_Size) + 1); end; name No_Entry from hash_abstraction; name No_Fresh from hash_abstraction; function Stop(cscan: CyclicScan): boolean = begin cexit result iff (cscan.value=cscan.start); result := cscan.value = cscan.start end; function Val(cscan: CyclicScan): bounds = begin cexit result=cscan.value; result := cscan.value end; {P r o c e d u r e s} procedure Delete (key:xobj; var table:HashTable) unless (cond notfound) = begin exit case( is normal: (all k:xobj, k ne key -> lookup(k,table) = lookup(k,table')) and not in_table(key,table); is notfound: not in_table(key,table) and table = table'); cexit case( is normal: all j:bounds, table[j].flag = used -> table[j].key ne key; is notfound: all j:bounds, table[j].flag = used -> table[j].key ne key); pending; end; procedure Insert(key: xobj; var table: hashtable; PROGRAM EXAMPLES Page E-20 Use as Program Description Language count: integer) unless (cond overflow) = begin exit case( is normal: lookup (key, table) = count and (all x: xobj, x ne key -> lookup (x, table) = lookup (x, table')); is overflow: table = table'); cexit case ( is normal: some j: bounds, (table(j)=initial(hashentry) with (.flag := used; .key := key; .count := count) and all k: bounds, j ne k -> table(k) = table'(k)); is overflow: table=table'); var cscan: CyclicScan:=initScan(key); loop case table(val(cscan)).flag is fresh, deleted: table(val(cscan)):= table(val(cscan)) with (.flag := used; .key := key; .count := count); leave; is used: if table(val(cscan)).key=key then table(val(cscan)).count:=count; leave end; end; assert no_fresh (table, key, val(cscan)) and no_entry(table,key, val(cscan)); step_scan(cscan); if stop(cscan) then signal overflow end; end; assert no_fresh(table, key, val(cscan)) and is_entry (table(val(cscan)), key) and table(val(cscan)).count=count; end; procedure Step_Scan(var cscan:CyclicScan) = begin cexit cscan =cscan' with (.value := next (cscan'.value) ); cscan.value:= ((cscan.value+1) mod Table_Size) + 1 end; {T y p e s} name Bounds from hash_abstraction; type Boundseq = sequence of bounds; type CyclicScan = record (value,start: bounds); name HashEntry from hash_abstraction; PROGRAM EXAMPLES Page E-21 Use as Program Description Language name HashTable from hash_abstraction; name Hashflags from hash_abstraction; name hash_eq from hash_abstraction; name Xobj from freq_count; end; {scope hashing_procedures} PROGRAM EXAMPLES Page E-22 Use as Program Description Language IV. A Communication System (ACS) (Full Program Description) SCOPE DECODE_ENCODE_PROCEDURES = begin {F u n c t i o n s} name Decode_Message from message_abstraction; function Decode_Seq(mssg_seq:message_sequence):message_sequence = begin exit (assume Decode_seq(mssg_seq) = if mssg_seq=null(message_sequence) then null(message_sequence) else Decode_seq(nonlast(mssg_seq)) <: Decode_message(last(mssg_seq)) fi; assume all r,s:message_sequence, r sub s -> Decode_seq(r) sub Decode_seq(s)); end; function Decode_To_User(A_switch_port: external_port; A_net_port: internal_port; a_id: activationid): boolean = begin exit (assume Decode_to_user(A_switch_port,A_net_port,a_id) iff OutTo(A_net_port.OutLine, a_id) sub Decode_seq(InFrom(A_switch_port.OutLine, a_id))); end; name Destination from message_abstraction; name Encode_Message from message_abstraction; function Encode_To_Switch(A_net_port: internal_port; a_switch_port: external_port; a_id: activationid): boolean = begin exit (assume Encode_to_switch(A_net_port,A_switch_port,a_id) iff Decode_seq(OutTo(A_switch_port.InLine, a_id)) sub InFrom(A_net_port.Inline, a_id)); end; name Make_Message from message_abstraction; name Source from message_abstraction; PROGRAM EXAMPLES Page E-23 Use as Program Description Language {P r o c e d u r e s} procedure Decoder(var A_switch_port: External_port; var A_net_port:Internal_port; u_id:user_id) = begin block Decode_to_user(A_switch_port,A_net_port, myId); exit false; var mssg:message := Make_message(u_id,u_id,null(charstring)); cond Destination_err, SendError, ReceiveError; keep Destination(mssg) = u_id otherwise Destination_err; loop assert Decode_to_user(A_switch_port,A_net_port, myId); begin receive mssg from A_switch_port.OutLine; send Decode_message(mssg) to A_net_port.OutLine; when is Destination_err,SendError,ReceiveError: end; end; end; procedure Encoder(var A_net_port: Internal_port; var A_switch_port:External_port; u_id:user_id) = begin block Encode_to_switch(A_net_port,A_switch_port, myId); exit false; var mssg:message:=Make_message(u_id,u_id,null(charstring)); cond Source_err, senderror,receiveerror; keep Source(mssg) = u_id otherwise Source_err; loop assert Encode_to_switch(A_net_port,A_switch_port, myId); begin receive mssg from A_net_port.InLine; send Encode_message(mssg) to A_switch_port.InLine; when is Source_err,SendError,ReceiveError: end; end; end; {T y p e s} name Charstring from message_abstraction; name External_Port from port_buffer_types; name Internal_Port from port_buffer_types; name Message from message_abstraction; PROGRAM EXAMPLES Page E-24 Use as Program Description Language name Message_Sequence from message_abstraction; name message_eq from message_abstraction; name User_Id from port_buffer_types; end; {scope decode_encode_procedures} SCOPE MESSAGE_ABSTRACTION = begin {F u n c t i o n s} function Decode_Message(mssg:message):message = begin exit Source(mssg) = Source(Decode_message(mssg)) and Destination(mssg) = Destination(Decode_message(mssg)); pending; end; function Destination(mssg:message):User_id = begin cexit Destination(mssg) = mssg.user2; result := mssg.user2; end; function Encode_Message(mssg:message):message = begin exit Source(Encode_message(mssg)) = Source(mssg) and Destination(Encode_message(mssg)) = Destination(mssg); pending; end; function Make_Message(user1,user2:User_id; cstring:charstring):message = begin cexit Make_message(user1,user2,cstring) = initial(message) with (.user1:=user1; .user2:=user2; .cstring:=cstring); result.user1 := user1; result.user2 := user2; result.cstring := cstring; end; function Message_Eq extends "=" (mssg1,mssg2:message):boolean = begin cexit message_eq(mssg1,mssg2) iff (mssg1.user1=mssg2.user1) and (mssg1.user2=mssg2.user2) and (mssg1.cstring=mssg2.cstring); result := (mssg1.user1=mssg2.user1) and (mssg1.user2=mssg2.user2) and (mssg1.cstring=mssg2.cstring); end; PROGRAM EXAMPLES Page E-25 Use as Program Description Language function Source(mssg:message):User_id = begin cexit Source(mssg) = mssg.user1; result := mssg.user1; end; function Text(mssg:message):charstring = begin cexit Text(mssg) = mssg.cstring; result := mssg.cstring; end; {L e m m a s} lemma Message_Req(user1,user2: user_id; cstring: charstring; mssg: message)= Source(Make_message(user1,user2,cstring)) = user1 and Destination(Make_message(user1,user2,cstring)) = user2 and Text(Make_message(user1,user2,cstring)) = cstring and Decode_message(Encode_message(mssg)) = mssg; {T y p e s} type Charstring = sequence(100) of character; type Message = record(user1,user2:User_id; cstring:charstring); type Message_Sequence = sequence of message; name User_Id from port_buffer_types; end; {scope message_abstraction} SCOPE NETWORK_PROCEDURES = begin {C o n s t a n t s} name Nusers from port_buffer_types; {F u n c t i o n s} name Destination from message_abstraction; name Decode_To_User from decode_encode_procedures; name Encode_To_Switch from decode_encode_procedures; name message_eq from message_abstraction; PROGRAM EXAMPLES Page E-26 Use as Program Description Language function Mail(mssg_seq:message_sequence; u_id1, u_id2: user_id): message_sequence = begin exit (assume Mail(mssg_seq,u_id1,u_id2) = if mssg_seq = null (message_sequence) then null (message_sequence) else if Source(last(mssg_seq)) = u_id1 and Destination(last(mssg_seq)) = u_id2 then Mail(nonlast(mssg_seq),u_id1,u_id2) <: last(mssg_seq) else Mail(nonlast(mssg_seq),u_id1,u_id2) fi fi); end; function Proper_Delivery(int_port: internal_port_array; u_id1, u_id2: user_id; a_id: activationid) : boolean = begin exit (assume Proper_delivery(Int_port,u_id1,u_id2,a_id) iff Mail(OutTo(Int_port[u_id2].OutLine, a_id),u_id1,u_id2) sub Mail(InFrom(Int_port[u_id1].InLine, a_id),u_id1,u_id2)); end; name Source from message_abstraction; {P r o c e d u r e s} name Decoder from decode_encode_procedures; name Encoder from decode_encode_procedures; procedure Node(var A_net_port: Internal_port; var A_switch_port:External_port; u_id:User_id) = begin block Encode_to_switch(A_net_port,A_switch_port, myId) and Decode_to_user(A_switch_port,A_net_port, myId); exit false; cobegin Encoder(A_net_port,A_switch_port,u_id); Decoder(A_switch_port,A_net_port,u_id); end; end; PROGRAM EXAMPLES Page E-27 Use as Program Description Language procedure Switch(var Switch_port:Internal_port_array) = begin entry Nusers ge 1; block all u_id1, u_id2:User_id, proper_delivery(switch_port, u_id1, u_id2, myid); exit false; var mssg:message; cond SendError, ReceiveError; loop assert all u_id1,u_id2:User_id, proper_delivery(switch_port, u_id1, u_id2, myid); await each k: [1..nusers], on receive mssg from Switch_port[k].InLine then if Source(mssg) = k then send mssg to Switch_port[Destination(mssg)].OutLine; end; when is SendError,ReceiveError: end; end; end; {T y p e s} name External_Port from port_buffer_types; name Internal_Port from port_buffer_types; name Internal_Port_Array from port_buffer_types; name Message from message_abstraction; name Message_Sequence from message_abstraction; name User_Id from port_buffer_types; end; {scope network} SCOPE PORT_BUFFER_TYPES = begin {C o n s t a n t s} const Bufsize:integer = PENDING; const Nusers:integer = PENDING; {T y p e s} type External_Port = record ( InLine: Line ; OutLine: Line ); PROGRAM EXAMPLES Page E-28 Use as Program Description Language type Internal_Port = record ( InLine: Line ; OutLine: Line ); type Internal_Port_Array = array(user_Id) of Internal_port; type Line = buffer(bufsize) of message; name Message from message_abstraction; type Port = record(InLine,OutLine:Line); type Port_Array = array[User_id] of Port; type User_Id = integer[1..Nusers]; end; {scope port_buffer_types} SCOPE TOP_LAYER_NETWORK = begin {C o n s t a n t s} name Nusers from port_buffer_types; {F u n c t i o n s} name Proper_Delivery from network_procedures; {P r o c e d u r e s} procedure Network(var Net_port:Internal_port_array) = begin block all u_id1,u_id2:User_id, proper_delivery(net_port, u_id1, u_id2, myid); exit false; var Switch_port:Port_array; cobegin each u_id1:[1..nusers], Node(Net_port[u_id1],Switch_port[u_id1],u_id1); Switch(Switch_port); end; end; name Node from network_procedures; name Switch from network_procedures; {T y p e s} name Internal_Port_Array from port_buffer_types; name Port_Array from port_buffer_types; name User_Id from port_buffer_types; PROGRAM EXAMPLES Page E-29 Use as Program Description Language end; {scope top_layer_network} APPENDIX F F APPENDIX G G APPENDIX H H APPENDIX I INDEX Page Index-1 INDEX Abnormal termination . . . . . . . . 4-3 Abstract external specifications . . 4-11 Abstract type . . . . . . . . . . . 7-5 to 7-6 initial value . . . . . . . . . . 7-5 Abstract types basetype . . . . . . . . . . . . . 7-9 constants . . . . . . . . . . . . 4-6 equality . . . . . . . . . . . . . 4-5, 7-9, 9-7 initial value . . . . . . . . . . 7-6, 7-8 lemmas . . . . . . . . . . . . . . 6-1 value . . . . . . . . . . . . . . 7-8 Access lists . . . . . . . . . . . . 3-6 composition access list . . . . . 7-5 to 7-6 reference access list . . . . . . 3-3 Activationid type . . . . . . . . . 7-36 Actual parameters conditions . . . . . . . . . . . . 8-4 data . . . . . . . . . . . . . . . 8-2 Adjoin(operator) . . . . . . . . . . 7-28, 9-6, 9-9 Aliasing . . . . . . . . . . . . . . 8-3 to 8-4 Allowedops . . . . . . . . . . . . . 7-6 Alteration clause . . . . . . . . . 9-15 Append(operator) . . . . . . . . . . 7-35, 9-6, 9-10 Before . . . . . . . . . . . . . . . 9-16 Behind . . . . . . . . . . . . . . . 9-16 Bounded simple type . . . . . . . . 7-14 Brackets . . . . . . . . . . . . . . 2-5 Buffer histories . . . . . . . . . . 7-41 Buffer restrictions . . . . . . . . 7-37 Buffer types . . . . . . . . . . . . 7-37 Case exit specification . . . . . . 4-12 Composition access list . . . . . . 7-4, 7-6 Concrete external specifications . . 4-12 Concrete representation . . . . . . 7-7 Concurrency . . . . . . . . . . . . 1-8, 10-17 Condition handling . . . . . . . . . 1-8, 10-20 Conditional expressions . . . . . . 9-18 Conditions actual condition parameters . . . 8-4 cond declaration . . . . . . . . . 4-15 formal condition parameter . . . . 4-6 in exit specification . . . . . . 4-12 Constant declaration local . . . . . . . . . . . . . . 5-1 Constant declarations . . . . . . . 5-1 global . . . . . . . . . . . . . . 5-1 Data abstraction . . . . . . . . . . 7-6 Difference(operator) . . . . . . . . 7-29, 7-32, 9-6, 9-10 Page Index-2 Dynamic external specification . . . 4-1 Dynamic structured types . . . . . . 7-26 give statement . . . . . . . . . . 10-9 move statement . . . . . . . . . . 10-7 remove statement . . . . . . . . . 10-6 Each clause alteration clause . . . . . . . . 9-15 await statement . . . . . . . . . 10-19 cobegin statement . . . . . . . . 10-18 Equality extension . . . . . . . . . 4-5, 9-7 Exit case . . . . . . . . . . . . . 4-12 Formal parameters conditions . . . . . . . . . . . . 4-6 data . . . . . . . . . . . . . . . 4-6 Function composition . . . . . . . . 9-3, 9-5, 9-11, 9-13 Global name . . . . . . . . . . . . 3-3 Hold specification . . . . . . . . . 7-7 to 7-8 Implementation defined units . . . . 3-7 Implementation requirements . . . . 1-7 Implicit parameters myid . . . . . . . . . . . . . . . 4-4, 7-36 result . . . . . . . . . . . . . . 4-6 In(operator) . . . . . . . . . . . . 7-28, 7-35, 9-7, 9-9 to 9-10 Incremental development . . . . . . 1-11 Initial . . . . . . . . . . . . . . 7-6 Initial value specification . . . . 7-5 Internal specification . . . . . . . 4-2 Intersect(operator) . . . . . . . . 7-29, 7-32, 9-6, 9-10 Keep specification . . . . . . . . . 4-10 Lemma declarations . . . . . . . . . 6-1 Local constant . . . . . . . . . . . 5-1 Local name . . . . . . . . . . . . . 3-3 to 3-5 Main program . . . . . . . . . . . . 8-5 Mapomit(operator) . . . . . . . . . 7-32, 9-16 Multiple condition error . . . . . . 10-22 Myid (implicit parameter) . . . . . 4-4, 7-36 Name declarations . . . . . . . . . 3-5 Name scopes . . . . . . . . . . . . 3-6 Nonvalidated expression . . . . . . 9-2 Normal termination . . . . . . . . . 4-3 Omit(operator) . . . . . . . . . . . 9-6, 9-9 Operation restrictions . . . . . . . 7-38 Operator axioms . . . . . . . . . . 9-7 Operator extension . . . . . . . . . 4-6 Overloaded . . . . . . . . . . . . . 10-5 Overloading . . . . . . . . . . . . 9-4 Page Index-3 Parameter passage . . . . . . . . . 7-2, 7-39, 8-3, 8-5 Parameters actual conditions . . . . . . . . 8-4 actual data . . . . . . . . . . . 8-2 formal condition . . . . . . . . . 4-6 formal data . . . . . . . . . . . 4-6 Pending . . . . . . . . . . . . . . 2-5, 7-5, 10-1 Process blockage . . . . . . . . . . 4-13, 10-2, 10-4, 10-10, 10-19 to 10-20 Program description . . . . . . . . 3-1 Proof directives . . . . . . . . . . 9-2 Quantified expressions . . . . . . . 9-19 Range . . . . . . . . . . . . . . . 7-11 Realizable programs . . . . . . . . 1-7 Reference access list . . . . . . . 3-3 Result (implicit parameter) . . . . 4-6 Routine calls . . . . . . . . . . . 8-1 Routine declarations . . . . . . . . 4-1 Routine header functions . . . . . . . . . . . . 4-5 procedures . . . . . . . . . . . . 4-3 Routineerror . . . . . . . . . . . . 8-2, 10-22 Scope declarations . . . . . . . . . 3-2 Selector clause . . . . . . . . . . 9-12 Seqomit(operator) . . . . . . . . . 9-16 Sequence constructors . . . . . . . 9-21 Set constructors . . . . . . . . . . 9-21 Shared type . . . . . . . . . . . . 7-10 Size restrictions . . . . . . . . . 7-27 Size(operator) . . . . . . . . . . . 9-10 Spaceerror . . . . . . . . . . . . . 7-26 Specification expression . . . . . . 9-2 Specifications . . . . . . . . . . . 1-9 assert statements . . . . . . . . 10-2 block . . . . . . . . . . . . . . 4-11, 4-13 case exit . . . . . . . . . . . . 4-12 cblock . . . . . . . . . . . . . . 4-12 centry . . . . . . . . . . . . . . 4-12 cexit . . . . . . . . . . . . . . 4-12 concrete . . . . . . . . . . . . . 4-12 dynamic external . . . . . . . . . 4-11 entry . . . . . . . . . . . . . . 4-11 exit . . . . . . . . . . . . . . . 4-11 hold . . . . . . . . . . . . . . . 7-7 to 7-8 internal . . . . . . . . . . . . . 4-10, 4-15, 10-1 keep . . . . . . . . . . . . . . . 4-10, 4-15 Standard conditions aliaserror . . . . . . . . . . . . 8-4 routineerror . . . . . . . . . . . 8-2, 10-22 spaceerror . . . . . . . . . . . . 7-26 valueerror . . . . . . . . . . . . 8-4 to 8-5 varerror . . . . . . . . . . . . . 8-4 to 8-5 Standard functions domain . . . . . . . . . . . . . . 7-31 Page Index-4 first . . . . . . . . . . . . . . 7-35 last . . . . . . . . . . . . . . . 7-35 lower . . . . . . . . . . . . . . 7-14 max . . . . . . . . . . . . . . . 7-13 min . . . . . . . . . . . . . . . 7-13 nonfirst . . . . . . . . . . . . . 7-35 nonlast . . . . . . . . . . . . . 7-35 null . . . . . . . . . . . . . . . 7-26, 9-10 ord . . . . . . . . . . . . . . . 7-15 pred . . . . . . . . . . . . . . . 7-15, 7-18, 7-21 range . . . . . . . . . . . . . . 7-31 scale . . . . . . . . . . . . . . 7-15 size . . . . . . . . . . . . . . . 7-28, 7-33 to 7-34 succ . . . . . . . . . . . . . . . 7-15, 7-18, 7-21 upper . . . . . . . . . . . . . . 7-14 Static external specification . . . 4-1 Sub(operator) . . . . . . . . . . . 9-7 Subrange . . . . . . . . . . . . . . 7-11 Subtype . . . . . . . . . . . . . . 7-3 Type compatability . . . . . . . . . 7-4 Type consistency . . . . . . . . . . 7-39 Types . . . . . . . . . . . . . . . 7-1 activationid . . . . . . . . . . . 7-36 allowedops . . . . . . . . . . . . 7-2, 7-11 to 7-12 basetype . . . . . . . . . . . . . 7-9, 7-11 bounded simple . . . . . . . . . . 7-14 initial value . . . . . . . . . . 7-2, 7-6, 7-8 to 7-9, 7-11 to 7-12 subrange . . . . . . . . . . . . . 7-11, 7-21 value . . . . . . . . . . . . . . 7-2, 7-8, 7-11 to 7-12 Union(operator) . . . . . . . . . . 7-28, 7-31, 9-6, 9-9 Unit declarations . . . . . . . . . 3-4 Unit name scope . . . . . . . . . . 3-4 Unrealizable programs . . . . . . . 1-7 Validation directive . . . . . . . . 9-2 Valueerror . . . . . . . . . . . . . 8-3 Values . . . . . . . . . . . . . . . 7-6 Var declaration . . . . . . . . . . 4-14 Varerror . . . . . . . . . . . . . . 8-3 Variable initialization . . . . . . 4-14 When clause . . . . . . . . . . . . 10-20 With clause(alteration clause) . . . 9-15