waashk/acm huggingface dataset:
composition and refinement of discrete real-time systems  reactive systems exhibit ongoing, possibly nonterminating, interaction with the environment. real-time systems are reactive systems that must satisfy quantitative timing constraints. this paper presents a structured compositional design method for discrete real-time systems that can be used to combat the combinatorial explosion of states in the verification of large systems. a composition rule describes how the correctness of the system can be determined from the correctness of its modules, without knowledge of their internal structure. the advantage of compositional verification is clear. each module is both simpler and smaller than the system itself. composition requires the use of both model-checking and deductive techniques. a refinement ruleguarantees that specifications of high-level modules are preserved by their implementations. the statetime toolset is used to automate parts of compositional designs using a combination of model-checking and simulation. the design method is illustrated using a reactor shutdown system that cannot be verified using the statetime toolset (due to the combinatorial explosion of states) without compositional reasoning. the reactor example also illustrates the use of the refinement rule.  jonathan s. ostroff
extending object oriented programming in smalltalk  smalltalk is an object oriented programming language with behavior invoked by passing messages between objects. objects with similar behavior are grouped into classes. these classes form a hierarchy. when an object receives a message, the class or one of its superclasses provides the corresponding method to be executed. we have built an experimental personal information environment (pie) in smalltalk that extends this paradigm in several ways. a pie object, called a node, can have multiple perspectives, each of which provides independent specialized behaviors for the object as a whole, thus providing multiple inheritance for nodes. nodes have metadescription to guide viewing of the objects during browsing, provide default values, constrain the values of attributes, and define procedures to be run when values are sought or set. all nodes have unique names which allow objects to migrate between users and machines. finally attribute lookup for nodes is context sensitive, thereby allowing alternative descriptions to be created and manipulated.  this paper first reviews smalltalk, then discusses our implementation of each of the above capabilities within pie, a smalltalk system for representing and manipulating designs. we then describe our experience with pie applied to software development and technical writing. our conclusion is that the resulting hybrid is a viable offspring for exploring design problems.  ira p. goldstein daniel g. bobrow
professional development seminars: introduction to pascal  this intensive one-day tutorital introduces the concepts and abstractions upon which pascal is based, current methods for specifying the syntax of a language, pascal's relation to software engineering, and the status of the pascal standardization activity.  a multimedia environment is used to develop pascal programs on-line. at the end of the session, participants should be able to read and analyze pascal code, differentiate between "true pascal" and non-conforming pascal-like code, and have a working knowledge of the syntactic definitions of pascal: bnf, railroad diagrams, and a pascal standard.  a. winsor brown
a certifying compiler for java  this paper presents the initial results of a project to determine ifthe techniques of  proof- carrying code and certifying compilers can be applied to programming languages of realistic size and complexity. the experiment shows that: (1) it is possible to implement a certifying native-code compiler for a large subset of the java programming language; (2) the compiler is freely able to apply many standard local and global optimizations; and (3) the pcc binaries it produces are of reasonable size and can be rapidly checked for type safety by a small proof- checker. this paper also presents further evidence that pcc provides several advantages for compiler development. in particular, generating proofs of the target code helps to identify compiler bugs, many of which would have been difficult to discover by testing.  christopher colby peter lee george c. necula fred blau mark plesko kenneth cline
proposal for a prototyping kit  the three-levelled ansi/sparc architecture for database systems forms a framework on which software prototypes can be built. the external level corresponds to screen panels, the conceptual level to the data model, and the internal level to the stored files of the prototype. the paper identifies prototype design tools and building- blocks with respect to this architecture. a screen design tool illustrates ideas using nested arrays. a novel aspect is, that the paper takes a step towards an operational formulation of the prototyping approach by emphasizing the computerized implementation.  jan jantzen
war on the workspace!: supporting continuously changing commercial software using a relational database we describe a relatively simple but effective set of techniques that is used to support a commercial computer application maintained by several developers and used by several thousand businesses. the techniques allow for complete control over a system that is in a continuous state of maintenance and enhancement. all functions and data are controlled by a proprietary relational database written in apl with almost no reliance on the contents of the workspace. the workspace contains only the few functions required to initialize the application and utility functions that are there simply to avoid defining them at load time. all other functions are defined as they are needed by specific user commands and erased thereafter. edward j. shaw
an integrated system for program testing using weak mutation and data flow analysis  the idea of weak mutation testing is to construct test data which would force program components such as expressions and variable references to produce a wrong 'result' if they were to contain certain types of error, for example, off-by-a-constant or wrong-variable. the idea of data flow driven testing is to construct test data which forces the execution of different interactions between variable definitions and references in a program.  this paper describes a tool for fortran 77 programs which has been developed to help a user apply the weak mutation and data flow testing techniques. the tool instruments a given source program and collects a program execution history. it is then able to report on the completeness of the test data with respect to weak mutation and a family of data flow path selection criteria. some preliminary experiments with use of the tool are described.  m. r. girgis m. r. woodward
ts: an optimizing compiler for smalltalk  ts (typed smalltalk) is a portable optimizing compiler that produces native machine code for a typed variant of smalltalk, making smalltalk programs much faster. this paper describes the structure of ts, the kinds of optimizations that it performs, the constraints that it places upon smalltalk, the constraints placed upon it by an interactive programming environment, and its performance.  ralph e. johnson justin o. graver laurance w. zurawski
a taxonomy of coordination mechanisms used by real-time processes a taxonomy of the coordination mechanisms for the synchronization and communication of concurrent processes is proposed. the taxonomy deals with the issues of a real-time software architecture that are application domain independent. the taxonomy will help the designer select the best coordination mechanism for a particular situation.a software reuse domain analysis methodology has been used to develop the taxonomy. while ada is the programming language that has been considered here, some of the attributes and guidelines are still valid for other programming languages. jose l. fernandez
integrated program measurement and documentation tools  this paper describes an attempt to integrate the collection and the efficient utilisation of measurements in the development and the use of programs. the work presented consists in three parts:  \\- the design of both static and dynamic measurement tools,  \\- examples of data processing on measurements collected on a sample of pascal programs,  \\- the design of a quantitative documentation of a program, which is automatically built as measurements are collected.  the first and third steps have been developed inside an existing programming environment, mentor, and we shall discuss the advantages we found in integrating the tools in such an environment.  anne schroeder
an automatic trace analysis tool generator for estelle specifications this paper describes the development of tango, an automatic generator of backtracking trace analysis tools for single-process specifications written in the formal description language, estelle. a tool generated by tango automatically checks the validity of any execution trace against the given specification, and supports a number of checking options. the approach taken was to modify an estelle-to-c++ compiler. discussion about nondeterministic specifications, multiple observation points, and on-line trace analysis follow. trace analyzers for the protocols lapd and tp0 have been tested and performance results are evaluated. issues in the analysis of partial traces are also discussed. s. alan ezust gregor v. bochmann
static analysis of upper and lower bounds on dependences and parallelism  existing compilers often fail to parallelize sequential code, even when a program can be manually transformed into parallel form by a sequence of well- understood transformations (as in the case for many of the perfect club benchmark programs). these failures can occur for several reasons: the code transformations implemented in the compiler may not be sufficient to produce parallel code, the compiler may not find the proper sequence of transformations, or the compiler may not be able to prove that one of the necessary transformations is legal.  when a compiler fails to extract sufficient parallelism from a program, the programmer may try to extract additional parallelism. unfortunately, the programmer is typically left to search for parallelism without significant assistance. the compiler generally does not give feedback about which parts of the program might contain additional parallelism, or about the types of transformations that might be needed to realize this parallelism. standard program transformations and dependence abstractions cannot be used to provide this feedback.  in this paper, we propose a two-step approach to the search for parallelism in sequential programs. in the first step, we construct several sets of constraints that describe, for each statement, which iterations of that statement can be executed concurrently. by constructing constraints that correspond to different assumptions about which dependences might be eliminated through additional analysis, transformations, and user assertions, we can determine whether we can expose parallelism by eliminating dependences. in the second step of our search for parallelism, we examine these constraint sets to identify the kinds of transformations needed to exploit scalable parallelism. our tests will identify conditional parallelism and parallelism that can be exposed by combinations of transformations that reorder the iteration space (such as loop interchange and loop peeling).  this approach lets us distinguish inherently sequential code from code that contains unexploited parallelism. it also produces information about the kinds of transformations needed to parallelize the code, without worrying about the order of application of the transformations. furthermore, when our dependence test is inexact we can identify which unresolved dependences inhibit parallelism by comparing the effects of assuming dependence or independence. we are currently exploring the use of this information in programmer-assisted parallelization.  william pugh david wonnacott
a gesture based user interface prototyping system  gid, for gestural interface designer, is an experimental system for prototyping gesture-based user interfaces. gid structures an interface as a collection of "controls": objects that maintain an image on the display and respond to input from pointing and gesture-sensing devices. gid includes an editor for arranging controls on the screen and saving screen layouts to a file. once an interface is created, gid provides mechanisms for routing input to the appropriate destination objects even when input arrives in parallel from several devices. gid also provides low level feature extraction and gesture representation primitives to assist in parsing gestures.  r. b. dannenberg d. amon
compiler and tool support for debugging object protocols  we describe an extension to the java programming language that supports static conformance checking and dynamic debugging of object "protocols," i.e., sequencing constraints on the order in which methods may be called. our java protocols have a statically checkable subset embedded in richer descriptions that can be checked at run time. the statically checkable subtype conformance relation is based on nierstrasz' proposal for regular (finite- state) process types, and is also very close to the conformance relation for architectural connectors in the wright architectural description language by allen and garlan. richer sequencing properties, which cannot be expressed by regular types alone, can be specified and checked at run time by associating predicates with object states. we describe the language extensions and their rationale, and the design of tool support for static and dynamic checking and debugging.  sergey butkevich marco renedo gerald baumgartner michal young
implementation of event handling in gna95gp gnat ada 95 graphics package (gna95gp) is a 2d graphics library that supports graphics application development in ada 95. it provides support for 2d drawing, event handling and storage of graphics primitives. this paper addresses the implementation of the event handling module of gna95gp under windows 3.1. using this event handling module, an user can write interactive programs under pc environment in ada 95 language. this event handling module is the result of an attempt to develop an event handling package using microsoft windows functions and ada 95 programming language features. this paper describes event handling and its implementation in gna95gp. similar to other graphics packages such as gks, srgp, and phigs, event handling is an important part in gna95gp. shan kuang k. m. george lan li
a note on "on the conversion of indirect to direct recursion"  in the article "on the conversion of indirect to direct recursion"(acm lett. program. lang. 2, 1-4. pp. 151-164), a method was introduced to convert indirect to direct recursion. it was claimed that for any call graph, there is a mutual-recursion elimination sequence if and only if no strongly connected component contains two node-disjoint circuits. we first give a counterexample and then provide a correction.  ting yu owen kaser
reasoning about object-oriented programs that use subtypes  programmers informally reason about object-oriented programs by using subtype relationships to classify the behavior of objects of different types and by letting supertypes stand for all their subtypes. we describe formal specification and verification techniques for such programs that mimic these informal ideas. our techniques are modular and extend standard techniques for reasoning about programs that use abstract data types. semantic restrictions on subtype relationships guarantee the soundness of these techniques.  gary t. leavens william e. weihl
interactive system for structured program production  the automation of program development procedures is one of the important subjects to be solved for improving productivity. the documentation of program specification and coding process involve many mechanical operations. presently, however, they are done mostly by human efforts. this greatly hinders the improvement of both productivity and program quality.  for the purpose of solving all the problems, we developed an experimental system sdl/pad. upon receipt of the specifications described in a structured form which has been defined in accordance with structured design, the sdl/pad. system automatically generates programs written with a computer language such as pl/m or the like and specification documents.  this system eliminates the troublesome inconsistency between documents and source programs.  h. maezawa m. kobayashi k. saito y. futamura
transporting a portable operating system: unix to an ibm minicomputer  the "portable" unix operating system was transported to an ibm series/1 minicomputer. the process of transporting is described with emphasis on (1) adapting to the target machine architecture; (2) the selection of the approach taken to transporting; (3) a description of the problems encountered; (4) the degree of portability of the unix system; and (5) a summary of the portability lessons learned.  paul j. jalics thomas s. heines
some uses of truncated boolean vectors in analysis  the truncated first occurrence vector (tfov) is a data construct which the author has found useful in a variety of application areas. it is based on comparisons of adjacent items in a set ordered by some criterion.  the use of the tfov and its several derivatives improve efficiency and reduce the load on system resources. a contributing factor in performance improvement is the algorithm used in the apl implementations of monadic grade and its offshoot dyadic grade. it is interesting to note that an ordered set improves the efficiency of processes other than those utilizing the tfov. calculation of the range and median of a numeric set is an example of this.  as new primitives have been added to apl, construction and generation of the tfov has been simplified. the paper shows both the early and the later idioms used in programs. the techniques for calculating frequency distributions and the related statistical mode or modes are shown. the development of sub-totals by group in simple (single criterion) and hierarchical cases are illustrated. the generation of (ordered) defining subsets and "arrival" and "departure" sequences are shown. along with the ordered defining subset (ods) a pointer to the ods can be developed. this technique has been found useful in applications requiring data compaction.  the tfov has proven useful in the development of control vectors for formatting tables especially for insertion of sub-total. a function for pagination of documents which eliminates "widows" has been developed, as have functions for reformatting paragraphs in text processing. in these latter cases, while the ordering algorithm is simply that of position, the concept is a direct outgrowth of experience with the tfov.  the techniques and concepts discussed in this paper are not intended to be exhaustive but are intended to stimulate programmers in considering an approach often overlooked. it is interesting to note that, while these ideas are applicable in other languages, their recognition required the primitives and arrays of apl.  howard j. smith
the designer as user: building requirements for design tools from design practice  software tools that support the design and development of interactive computing systems are an exciting possibility. the potential pay- off is great: user interface management systems, for example, promise not only to speed the process of specifying, implementing and maintaining user interface code, but also to guide the content of the user interfaces they support. as for any tool intended for human use, however, the success of software design tools will hinge on a thorough understanding of the problems they seek to address---design as it is practiced in the real world.  mary beth rosson wendy kellogg susanne maass
multitasking without comprimise: a virtual machine evolution the multitasking virtual machine (called from now on simply mvm) is a modification of the java virtual machine. it enables safe, secure, and scalable multitasking. safety is achieved by strict isolation of application from one another. resource control augment security by preventing some denial-of-service attacks. improved scalability results from an aggressive application of the main design principle of mvm: share as much of the runtime as possible among applications and replicate everything else. the system can be described as a 'no compromise'approach --- all the known apis and mechanisms of the java programming language are available to applications. mvm is implemented as a series of carefully tuned modifications to the java hotspot virtual machine, including the dynamic compiler. this paper presents the design of mvm, focusing on several novel and general techniques: an in-runtime design of lightweight isolation, an extension of a copying, generational garbage collector to provide best-effort management of a portion of the heap space, and a transparent and automated mechanism for safe execution of user-level native code. mvm demonstrates that multitasking in a safe language can be accomplished with a high degree of protection, without constraining the language, and and with competitive performance characteristics grzegorz czajkowski laurent daynes
analysis of queueing network models with population size constraints and delayed blocked customers  queueing network models - qnm's with population size constraints and delayed blocked customers occur due to multiprogramming level - mpl constraints in computer systems and window flow- control mechanisms in computer communication networks - ccn's. the computational cost of existing algorithms is unacceptable for large numbers of chains and high population sizes. a fast approximate solution technique based on load concealment is presented to solve such qnm's. the solution procedure is non-iterative in the case of fixed rate poisson arrivals, while iteration is required in the case of quasi-random arrivals. each iteration requires the solution of a single chain network of queues comprised of stations visited by each chain. we then present an algorithm to detect saturated chains and determine their maximum throughput. a fast solution algorithm due to reiser for closed chains is also extended to the case of quasi-random arrivals. the accuracy of the proposed solution techniques is compared to previous techniques by applying it to a test case, reported in the literature, and a set of randomly generated examples.  alexander thomasian paul bay
the maintenance of intermediate values in goal-directed evaluation  in programming languages that support goal-directed evaluation to make use of alternative results, an expression can produce a value, suspend, and later be resumed to produce another value. this causes control backtracking to earlier points in a computation and complicates the maintenance of intermediate values. this paper presents a space-efficient algorithm computing the lifetimes of intermediate values that is used by an optimizing compiler for the icon programming language. the algorithm is applicable to other programming languages that employ goal-directed evaluation.  kenneth walker ralph e. griswold
"transitioning an asis application: version 1 to ada95 2.0" asis (ada semantic interface specification) applications written to the "version 1" standard or subsequent 1.x permutations of this standard (such as version 1.1.1) were developed with and for ada83. porting such applications to the ada95 asis standard, version 2.0, is a non-trivial task. such an effort needs to address the major changes to the semantic abstractions of the language as represented by the version 2.0 ada95 asis specification.this paper is an experience report that documents an approach used to port several version 1.0 asis applications to version 2.0 compliance. a methodology for "finding" the mappings between the two specifications is documented along with the results (a mapping table of the asis queries) of that approach. joseph r. wisniewski