Alphard(ID:634/alp010)

Pascal with data abstraction 


named for the brightest star in Hydra

Wulf, Shaw and London, CMU 1974.

Pascal-like language for data abstraction and verification. Used the 'form', which combines a specification and an implementation. Took the generator from PL and made it a general case.

Development of the compiler was curtailed in 1979 "When it became clear that another iteration on the language design was necessary"

Places
People:
Related languages
IPL-V => Alphard   Influence
Pascal => Alphard   Based on
Alphard => CAMIL   Influence
Alphard => CLU   Influence
Alphard => LUKKO   Influence
Alphard => PLAIN   Influence
Alphard => TEMPO   Influence

References:
  • Wulf, W. A., and Shaw, M., "Global Variable Considered Harmful," SIGLPAN Notices 8(2), February 1973 view details
  • Wulf, William A. "Alphard: Toward a Language to Support Structured Programs". Dept. of Computer Science Tech Report AD-785 417, Carnegia-Mellon University, Pittsburgh, April 1974. view details
  • Wulf, W. A., "Some Thoughts on the Next Generation of Programming Languages" view details
          in CMU/CSD Tenth Anniversary Symposium, Prentice-Hall. 1975 view details
  • Horning, J. J. "Some desirable properties of data abstraction facilities" pp60-62 view details Extract: Euclid Modules
    2 Euclid Modules
    The module in Euclid is an encapsulation mechanism whereby the representation of an abstract object and the implementation of associated operations can be hidden from the enclosing scope. Multiple instances of an abstraction can be realized from the definition of a module type by declaring variables of that type. Closed scopes, and modules in particular, provide explicit control over the visibility of identifiers. Objects, operations, and types defined within the module must be explicitly exported in order to be used; similarly, values of variables declared outside a module must be imported explicitly to be known inside.
    Extract: Modules as Abstraction Mechanisms
    2.1 Modules as Abstraction Mechanisms
    A data type is defined by a set of values and a set of operations on those values. An abstract data type is a data type with a representat ion-independent definition. Thus, abstract data types permit access by outside routines only to the abstract values and operations, and not to any of the underlying representation. In this sense, clusters in CLU [Liskov et ai.77] and forms in Alphard [Wulf et al. 76] are abstract data types, whereas classes in Simula 67 [Dahl et al.68] are not, since all data structures in the outermost scope of a class are accessible. Palm, [73] has shown, however, how the necessary protection could be added to Simula 67 in a straightforward way.
    For reasons similar to those for Simula 67 classes, Euclid modules are not true abstract data types. Access to identifiers within a module is severely restricted by the import and export clauses as well as the Euclid scope rules~ but access is allowed. Euclid modules can be used, hoverers to implement abstract data types. This would require additional programmer disciplines unenforceable by the language itself to ensure that the only entities accessible to outside routines are those abstract entities being defined.

          in SIGPLAN Notices 11(02) February 1976 also Proceedings of the SIGPLAN '76 Conference on Data: Abstraction, Definition and Structure, Salt Lake City, Utah, USA, March 22-24, 1976 view details
  • London, Ralph L., Shaw, Mary and Wulf, Wm. A. "Abstraction and Verification in Alphard: A Symbol Table Example." Carnegie-Mellon Univ 29 Dec 76 AFOSR-TR-77-0324 view details Abstract: The design of the Alphard programming language has been strongly influenced by ideas from the areas of programming methodology and formal program verification. In this paper we design, implement, and verify a general symbol table mechanism. This example is rich enough to allow us to illustrate the use as well as the definition of programmer-defined abstractions. The verification illustrates the power of the form to simplify proofs by providing strong specifications of such abstractions.
          in SIGPLAN Notices 11(02) February 1976 also Proceedings of the SIGPLAN '76 Conference on Data: Abstraction, Definition and Structure, Salt Lake City, Utah, USA, March 22-24, 1976 view details
  • Shaw, Mary "Research directions in abstract data structures" view details
          in SIGPLAN Notices 11(02) February 1976 also Proceedings of the SIGPLAN '76 Conference on Data: Abstraction, Definition and Structure, Salt Lake City, Utah, USA, March 22-24, 1976 view details
  • Wulf, W.A., London, R.L., and Shaw, M., "Abstraction and verification in Alphard: Introduction to language and methodology" USC Information Science Institute Technical Report, University of Southern California, Los Angeles (1976). view details
          in SIGPLAN Notices 11(02) February 1976 also Proceedings of the SIGPLAN '76 Conference on Data: Abstraction, Definition and Structure, Salt Lake City, Utah, USA, March 22-24, 1976 view details
  • Wulf, William A.; London, Ralph L.; Shaw, Mary "An introduction to the construction and verification of Alphard programs" view details Abstract: Alphard is a programming language whose goals include supporting both development of well-structured programs and formal verification of these programs. This paper attempts to capture the symbiotic influence of these two goals on the design of the language. The language description is interleaved with the presentation of a proof technique and discussion of programming methodology. Examples to illustrate both the language and the verification technique are included.
          in Proceedings of the 10th International Conference on Software Engineering, IEEE Computer Society Press, 1988 view details
  • Foster, J. M. and Foster, P. D. Abstract data and functors pp161-167 view details
          in Proceedings of the Strathclyde ALGOL 68 conference Glasgow, Scotland 1977 view details
  • Mary Shaw, William A. Wulf, "Abstraction and verification in Alphard: defining and specifying iteration and generators" view details Abstract: The Alphard “form” provides the programmer with a great deal of control over the implementation of abstract data types. In this paper the abstraction techniques are extended from simple data representation and function definition to the iteration statement, the most important point of interaction between data and the control structure of the language itself. A means of specializing Alphard's loops to operate on abstract entities without explicit dependence on the representation of those entities is introduced. Specification and verification techniques that allow the properties of the generators for such iterations to be expressed in the form of proof rules are developed. Results are obtained that for common special cases of these loops are essentially identical to the corresponding constructs in other languages. A means of showing that a generator will terminate is also provided.
          in [ACM] CACM 20(08) (Aug 1977) view details
  • Wulf W.A. et al "Report on the ALPHARD language", Dept. of Computer Science, Carnegie-Mellon Univ., 1977. view details
          in [ACM] CACM 20(08) (Aug 1977) view details
  • Bentley, J.L. and M. Shaw, An Alphard Specification of a Correct and Efficient Transformation on Data Structures, Specifications of Reliable Software Proceedings, pp222-237, IEEE, April 1979 view details
          in [ACM] CACM 20(08) (Aug 1977) view details
  • Shaw, Mary (ed.) "Alphard: Form and Content", Springer-Verlag, New York, 1981 view details
          in [ACM] CACM 20(08) (Aug 1977) view details
  • Brinch Hansen, Per "Monitors and concurrent Pascal: a personal history" pp1-35 view details
          in [ACM SIGPLAN] SIGPLAN Notices 28(03) March 1993 The second ACM SIGPLAN conference on History of programming languages (HOPL II) view details
  • Library of Congress Subject Headings A254 view details
          in [ACM SIGPLAN] SIGPLAN Notices 28(03) March 1993 The second ACM SIGPLAN conference on History of programming languages (HOPL II) view details