Alphard Programming language is used for the data abstraction and verification designed by William A. Wulf, Ralph L. London, and Mary Shaw. The syntax of the Alphard programming language is same as that of the Pascal programming language. The Alphard programming language was in research in the 1970 by the experts but never implemented. The main feature of the Alphard programming is the form data type. The Form data type is used to combines a specification and a procedural implementation. Alphard’s constructs allow a programmer to isolate an abstraction, specifying its behavior publicly while localizing knowledge about its implementation.
form istack(n: integer)= beginform specifications requires n>0; let istack = <. . . xi . .. > where xi is integer; invariant 0<length(istack)<n; initially istack=nullseq; function push(s: istack, x :integer) pre 0 < length(s) < n post s=s'-x, pop(s: istack) pre 0 < length(s) < n post s = leader(s'), top(s: istack) returns (x: integer) pre 0 < length(s) 6 n post x = last(s'), empty(s: istack) returns (b: boolean) post b = (s=nullseq);x representation . . .; implementation.. . endform;