Euclid(ID:756/euc001)Verifiable system software language(named for the Greek geometer, fl ca 300 BC.) A Pascal descendant for development of verifiable system software. No goto, no side effects, no global assignments, no functional arguments, no nested procedures, no floats, no enumeration types. Pointers are treated as indices of special arrays called collections. To prevent aliasing, Euclid forbids any overlap in the list of actual parameters of a procedure. Each procedure gives an imports list, and the compiler determines the identifiers that are implicitly imported. Iterators. The Euclid Project. Holt et al, University of Toronto, (1977-80). Project supported by Canadian and USA governments and by IBM to build a compiler for a systems programming language with verification facilities. Used at I.P. Sharp Associates (Toronto), MITRE Corp. (Boston) and various institutes for system programming and research in secure software. People: Structures: Related languages
References: 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 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 in Proceedings of an ACM conference on Language design for reliable software 1977, Raleigh, North Carolina view details in SIGPLAN Notices 12(02) February 1977 view details in SIGPLAN Notices 13(03) March 1978 view details in SIGPLAN Notices 13(03) March 1978 view details The programming language Euclid [Lampson et al. 77] was designed to support the writing of verifiable system software, with the subgoal as a near-term projects to differ from Pascal as little as possible. Hence Euclid was expressly intended to be a research vehicle for new ideas in programming languages. One notable exception the Euclid designers made was in the area of data abstraction. Virtually all data abstraction mechanisms claim lineage from the Simula 67 class [Dahl et al. 68]. Descendent data abstraction mechanisms have not in general been used long enough for us to have much experience with their user and as a result much of the area of data abstraction still belongs in the realm of research. Although it was not absolutely necessary for Euclid to provide a data abstraction facility, its designers felt that such a programming tool would greatly contribute to the ability to decompose large programs so that they could be verified with existing verification methodso A data abstraction mechanism also encourages writing modular and structured programs, and thus helps meet other Euclid design goals. ([Horning76] provides an excellent summary of the advantages provided by abstraction mechanisms, both data and procedural.) in SIGPLAN Notices 13(03) March 1978 view details intended for writing verifiable system protrams, The following is an index for the defininq report for Euclid [Lampson et al,77 ]. DOI in SIGPLAN Notices 13(03) March 1978 view details DOI in SIGPLAN Notices 13(03) March 1978 view details Euclid [Lampson et a~.77] is a programming Language based on Pascal and intended for writing verifiable system programs° The basic me%hod for verifying ~uclid programs is an inductive assertion one similar to %hat used for Pascal [ Hoare and Wirth73]. Those features present in both Euclid and Pascal~ but different in Euclid due to the verification requirements will be the focus of attention in %his paper° Constructs added to Euclid specifically for verification will not be discussed~ since %hey in general have no Pascal counterpart. in SIGPLAN Notices 13(03) March 1978 view details in Proceedings of the SIGPLAN symposium on Compiler construction, August 06-10, 1979, Denver, Colorado, United States view details in Acta Informatica 10(1) August 4, 1978 view details in Acta Informatica 10(1) August 4, 1978 view details in Computer Languages 4(3-4) view details in ACM Computing Reviews 21(01) January 1980 view details MODULA is a simple programming language proposed by Wirth (1977a) for use in programming areas still dominated by Assembly code, such as process control, computerised laboratory equipment and input/output device drivers. Coding exercises in MODULA by Wirth (1977b) and others (Holden and Wand, 1978) have shown that the language is quite successful in these areas of application and is particularly good for the expressioh of single programs that will run on dedicated computing equipment. However the language does have a number of drawbacks if it is to be used for the coding of operating systems kernels or for the writing of any software component where supervision plays an important part. In particular these difficulties centre upon (a) a process supervising other processes (b) a storage allocation process and (c) the general handling of error conditions at both the process and module level. It is interesting to note that these are all requirements of the so-called 'Ironman' language (1977). This paper examines extensions to MODULA which attempt to overcome these drawbacks. A new storage mechanism is proposed based upon a declared type called a region which is very similar to the implicit heap in PASCAL. For references into such storage, PASCAL-like pointers are proposed. In addition it is proposed that processes and their storage must be allocated within a region, although it is not suggested that device processes should be included in this new mechanism. Thereafter references to ordinary processes must be made via pointers, and, furthermore, when a process is run it can be executed for a given number of signal occurrences (usually originating from a device process) under the supervision of a parent process. By this mechanism supervisory processes can be constructed which can then make sure that a process can only run for a limited period and can subsequently terminate that process if necessary. An exception mechanism is proposed for transmitting error conditions; however the mechanism can be used quite generally. We suggest that these extensions will cause moderate complications in the language definition and in the compiler. The major run time complication is in the storage allocation mechanism which implies a PASCAL-like heap within every region, although with the simplification that any region is allocated within the storage space of the parent process. In conclusion we suggest that the facilities proposed will enable a MODULA-like language to be used for the coding of basic operating system components. Extract: Modula vs GYVE vs EUCLID Note that this proposal certainly lacks the flexibility of GYVE pointers (Schwartz and Shaw, 1976) or the completeness of the Euclid (Lampson et al., 1977) visibility rules. However it is suggested that the simple rules of MODULA, together with the modification suggested here, will deal with the majority of practical cases. in The Computer Journal 23(2) 1980 view details in SIGPLAN Notices 16(05) May 1981 view details in Proceedings of the 5th International Conference on Software Engineering 1981, March 09-12, 1981, San Diego, California, United States view details in TOPLAS 4(4) October 1982 view details in TOPLAS 4(4) October 1982 view details Resources
|