Rapide is an event-based, concurrent, object-oriented language specifically designed for prototyping system architectures. Two principle design goals are: (1) to provide constructs for defining executable prototypes of architectures and (2) to adopt an execution model in which the concurrency, synchronization, dataflow, and timing properties of a prototype are explicitly represented. This paper describes the partially ordered event set (poset) execution model and outlines with examples some of the event-based features for defining communication architectures and relationships between architectures. Various features of Rapide are illustrated by excerpts from a prototype of the X/Open distributed transaction processing reference architecture.>

This paper discusses general requirements for architecture definition languages, and describes the syntax and semantics of the subset of the Rapide language that is designed to satisfy these requirements. Rapide is a concurrent event-based simulation language for defining and simulating the behavior of system architectures. Rapide is intended for modelling the architectures of concurrent and distributed systems, both hardware and software in order to represent the behavior of distributed systems in as much detail as possible. Rapide is designed to make the greatest possible use of event-based modelling by producing causal event simulations. When a Rapide model is executed it produces a simulation that shows not only the events that make up the model's behavior, and their timestamps, but also which events caused other events, and which events happened independently. The architecture definition features of Rapide are described: event patterns, interfaces, architectures and event pattern mappings. The use of these features to build causal event models of both static and dynamic architectures is illustrated by a series of simple examples from both software and hardware. Also we give a detailed example of the use of event pattern mappings to define the relationship between two architectures at different levels of abstraction. Finally, we discuss briefly how Rapide is related to other event-based languages.>

RAPIDE is a programming language framework designed for the development of large, concurrent, real-time systems by prototyping. The framework consists of a type language and default executable, specification and architecture languages, along with associated programming tools. We describe the main features of the type language, its intended use in a prototyping environment, and rationale for selected design decisions.

RAPIDE is a concurrent, object-oriented language specifically designed for prototyping large concurrent systems. One of the principle design goals has been to adopt a computation model in which the synchronization, concurrency, data flow, and timing aspects of a prototype are explicitly represented and easily accessible both to the prototype itself and to the prototyper. This article describes the partially ordered event set (poset) computation model and the features of RAPIDE for using posets in reactive prototypes and for automatically checking posets. An example prototyping scenario illustrates uses of the poset computation model, with and without timing.

article Free Access Share on Object-oriented megaprogramming (panel) Authors: Peter Wegner View Profile , William Scherlis View Profile , James Purtilo View Profile , David Luckham View Profile , Ralph Johnson View Profile Authors Info & Claims ACM SIGPLAN NoticesVolume 27Issue 10Oct. 1992 pp 392–396https://doi.org/10.1145/141937.141968Published:31 October 1992Publication History 1citation258DownloadsMetricsTotal Citations1Total Downloads258Last 12 Months9Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Abstract Adam is a high‐level language for parallel processing. It is intended for programming resource scheduling applications, in particular supervisory packages for run‐time scheduling of multiprocessing systems. An important design goal was to provide support for implementation of Ada and its run‐time environment. Adam has been used to implement Ada task supervision and also as a high‐level target language for compilation of Ada tasking. Adam provides facilities corresponding to the Ada sequential constructs (including subprograms, packages, exceptions, generics). In addition, it provides specialized module constructs for implementation of packages that may be shared between parallel processes, and new predefined types for scheduling. The parallel processing constructs of Adam are more primitive than Ada tasking. Strong restrictions are enforced on the ways in which parallel processes can interact. A compiler for Adam has been implemented in MacLisp on DEC PDP‐10 computers. Runtime support packages in Adam for scheduling (on a single CPU) and I/O are also provided. The compiler contains a library manipulation facility for separate compilation. The Adam compiler has been used to build an Ada compiler for most of the July 1980 Ada, including task types and rendezvous constructs. This was achieved by implementing the translation of Ada tasking into Adam parallel processing as a preprocessor to the Adam compiler. This present Ada compiler, which has been operational since December 1980, uses a procedure call implementation of tasking. It can be easily modified to other implementations. Compilation of Ada tasking into a high‐level target language such as Adam facilitates studying questions of correctness and efficiency of various compilation algorithms, and code optimizations specific to tasking, e.g. elimination of unnecessary threads of control. This paper gives an overview of Adam and examples of its use. Emphasis is placed on the differences from Ada. Experience using Adam to build the experimental Ada system is evaluated. Design of a run‐time supervisor in Adam is discussed in detail.

A method of documenting exception propagation and handling in Ada programs is proposed. Exception propagation declarations are introduced as a new component of Ada specifications, permitting documentation of those exceptions that can be propagated by a subprogram. Exception handlers are documented by entry assertions. Axioms and proof rules for Ada exceptions given. These rules are simple extensions of previous rules for Pascal and define an axiomatic semantics of Ada exceptions. As a result, Ada programs specified according to the method can be analyzed by formal proof techniques for consistency with their specifications, even if they employ exception propagation and handling to achieve required results (i.e., nonerror situations). Example verifications are given.

A practical method is presented for automating in a uniform way the verification of Pascal programs that operate on the standard Pascal data structures Array, Record, and Pointer. New assertion language primitives are introduced for describing computational effects of operations on these data structures. Axioms defining the semantics of the new primitives are given. Proof rules for standard Pascal operations on data structures are then defined using the extended assertion language. An axiomatic rule for the Pascal storage allocation operation, NEW, is also given. These rulers have been implemented in the Stanford Pascal program verifier. Examples illustrating the verification of programs which operate on list structures implemented with pointers and records are discussed. These include programs with side effects.

One objective of the study of schemes for computation is that of finding general methods for checking or verifying a given program against its specifications. If one views the program and its specification as presenting two supposedly equivalent schemes for a computation, then the objective reduces to one of finding general methods for determining whether, in fact, the two schemes are equivalent. Unfortunately, for many classes of schemes which are sufficiently powerful, this “equivalence problem” is not decidable, i.e. there are no general methods capable of determining, in all cases, whether two schemes in the class are equivalent. In this report we investigate the question of which classes of schemes have decidable equivalence problems, or, in otherwords the question of for which classes of schemes there exist general methods capable of determining equivalence.

This paper studies a number of logically complete search strategies (refinements) for improving the performance of automatic theorem-proving programs based on the resolution principle. These strategies restrict the number of deductions generated by the program at the expense of sometimes missing the shortest proof. By considering elementary proof-preserving transformations on resolution proof trees, (i) it is shown that the conjunction of set-of-support, resolution-with-merging, and linear form deduction is again a complete refinement; (ii) bounds are obtained on the possible increase in complexity of the proof trees when the linear form and resolution-with-merging refinements are imposed. Finally, examples are given which demonstrate the savings in time and storage when refinements are used to prove some theorems of moderate difficulty in group theory and ternary boolean algebra.

In the original example of a transfinite hierarchy of degrees of unsolvability, a predicate Ha is associated with each a in the set 0 of ordinal notations. (See Kleene [K1], Spector [S1], and the references there to Davis and Mostowski.) The predicates are defined by means of induction over the partial well-ordering relation ≤0 on the set 0 of notations for the recursive ordinals. The usefulness of this hierarchy of predicates is enhanced by Spector's proof [S1] of the “uniqueness” property: viz. that the degree of Ha depends only on the ordinal |a| for which a is a notation.