VTechWorks staff will be away for the winter holidays starting Tuesday, December 24, 2024, through Wednesday, January 1, 2025, and will not be replying to requests during this time. Thank you for your patience, and happy holidays!

Browsing by Author "Martin, Johannes J."

Now showing 1 - 11 of 11
  • Thumbnail Image
    Algebraic Specification of Complex Data Types
    Martin, Johannes J. (Department of Computer Science, Virginia Polytechnic Institute & State University, 1978)
    This paper discusses algebraic data type specifications that employ product sets as carriers. This leads to simplifications for certain data types. In particular, the method permits the specification of a complex type by the straight forward translation of an intuitive model of the type into a formal definition, provided that the model is conceived in terms of other well defined types. The concept is illustrated by two examples.
  • Thumbnail Image
    Conjunctive polymorphic type checking with explicit types
    Flannery, Kevin E. (Virginia Polytechnic Institute and State University, 1989)
    An expressive type language and the ability to do compile-time type inference are desirable goals in language design, but the attainment of the former may preclude the possibility of the latter. Specifically, the type conjunction operator (type intersection) induces a rich type language at the expense of decidability of the typeable expressions. Two extreme alternatives to this dilemma are to abandon type inference (and force the programmer to, essentially, supply a derivation for his type claims) or to abandon (or restrict) type conjunction. This work presents a third alternative in which the programmer, at times, may be required to supply explicit types in order for type inference to succeed. In this way, the power of conjunctive types is preserved, yet compile-time type inference can be done for a large class of polymorphic functions, including those typeable with parametric types. To this end, we introduce a simple combinator based language with typing rules based on type conjunction and a subtype relation, of sorts, called "weaker." The validity of the type rules with respect to the usual interpretation of "type" is shown, along with the undecidability of the type relation. It is shown how the computational portion of the language can be modified to accommodate explicit type information which may direct an automatic type derivation. This new language has the principal type property with respect to a decidable relation, although deciding this relation is shown to be an NP-Complete problem. The language is extended to accommodate type fixed points, and extended further to allow all expressions with parametric types to be typed automatically, and to accommodate integers, pairs, sums, and abstract types in the form of type generators.
  • Thumbnail Image
    A Domain For Functional Programming Systems
    Martin, Johannes J. (Department of Computer Science, Virginia Polytechnic Institute & State University, 1981)
    A domain for functional programming systems is proposed. This domain is the powerset of a set of items where items are either atomic or ordered pairs of items. The structure of the domain is detennined by the relation 'is weaker than' and by three basic operations, under which the domain is closed: Union, the cartesian product, and the operation of application.
  • Thumbnail Image
    FAD, a Functional Programming Language that Supports Abstract Data Types
    Martin, Johannes J. (Department of Computer Science, Virginia Polytechnic Institute & State University, 1980)
    The paper outlines the programming language FAD. FAD is a functional programming system of the kind described by Backus [Backus78]. FAD supports abstract data types, parameterized types, and generic functions. A single scope rule establishes the encapsulation requirements for data type specification and program structuring. Certain syntactic additions improve program readability as compared to pure functional notation.
  • Thumbnail Image
    Finiteness and Bounds of Complete Test Point Sets for Program Verification
    Martin, Johannes J. (Department of Computer Science, Virginia Polytechnic Institute & State University, 1976)
    It is proven that there exists a finite set of test points that suffices to establish the equivalence of two programs s and t if some finite set S of programs can be identified that contains both s and t. It is also proven that the expected number of those test points is bounded by the logarithm of the cardinality of S.
  • Thumbnail Image
    First Report on Epos: Aspects of Generality And Efficiency in Programming Language Implementation
    Martin, Johannes J. (Department of Computer Science, Virginia Polytechnic Institute & State University, 1974)
    No abstract available.
  • Thumbnail Image
    Generalized Structured Programming
    Martin, Johannes J. (Department of Computer Science, Virginia Polytechnic Institute & State University, 1973)
    In an effort to eliminate some inconveniences connected with Dijkstra's method of Structured Programming, a generalized set of basic flow graphs for structuring programs is suggested. These structures generate the set of all flow graphs that can be fully decomposed by Allen and Cocke's method of interval reduction. It will be shown that programs Composed of the proposed basic structures have most, if not all, of the Positive characteristics claimed for programs written with the classic rules of Structured Programming. Further, by extending Wirth's programming language PASCAL a set of new control constructs has been suggested that support the proposed set of flow structures.
  • Thumbnail Image
    Multi Safe -- a Modular Multiprocessing Approach to Secure Database Management
    Trueblood, Robert P.; Hartson, H. Rex; Martin, Johannes J. (Department of Computer Science, Virginia Polytechnic Institute & State University, 1980)
    This paper describes the configuration and inter-module communication of a MULTIprocessor system for supporting Secure Authorization with Full Enforcement (MULTISAFE) for database management. A modular architecture is described which provides secure, controlled access to shared data in a multiuser environment--with low performance penalties, even for complex protection policies. The primary mechanisms are structured and verifiable. The entire approach is immediately extendible to distributed protection of distributed data. The system includes a user and applications module (UAM), a data storage and retrieval module (SRM), and a protection and security module (PSM). The control of intermodule communication is based on a data abstraction approach. It is initially described in terms of function invocations. An implementation within a formal message system is then described. The discussion of function invocations begins with the single terminal case and extends to the multiterminal case. Some physical implementation aspects are also discussed, and some examples of message sequences are given.
  • Thumbnail Image
    On Data Types
    Martin, Johannes J. (Department of Computer Science, Virginia Polytechnic Institute & State University, 1983)
    A semantic model of types is proposed. This model interprets types as elements in an augmented domain constructed with the Smyth powerdomain constructor. In this domain types approximate the values of which they are types. Within this model, a type of an application f(x) is found by applying a type of f to a type of x. This becomes the basis of type checking and type inference. The model accomodates in a natural way type hierarchies, polymorphic functions, and recursive polymorphic types. A number of examples are worked out in some detail.
  • Thumbnail Image
    Program Testing and Conditional Correctness
    Martin, Johannes J. (Department of Computer Science, Virginia Polytechnic Institute & State University, 1976)
    It is shown that some beliefs about program testing are incorrect. A new notion of correctness, conditional correctness, is defined. It is then shown that conditional correctness, which can in principle be achieved by testing, is not accomplished by such methods as "testing all branches" or "testing all paths". The latter method is proven to be not only insufficient but also highly redundant. Rules for establishing conditional correctness by testing are given and illustrated by an example.
  • Thumbnail Image
    A Variant of the Fisher-Morris Garbage Compaction Algorithm
    Martin, Johannes J. (Department of Computer Science, Virginia Polytechnic Institute & State University, 1980)
    The garbage compactification algorithm described works in linear time and, for the most part, does not require any work space. It combines marking and compactification into a two-step algorithm. The first step marks all non-garbage cells and, at the same time, rearranges the pointers such that the cells can be moved, the second step performs the actual compatification.