SB-MODULA(ID:7532/)

Development extensions to MODULA 

for Stony Brook Modula


Extensions to MODULA to permit hierarchical development and verification


References:
  • Bernstein, A. J.; and Ensor, J. R. "A MODULA based language supporting hierarchical development and verification" Softw. Pract. Exper. 11, 3 (March 1981), 237-255. view details
  • Wirth, N. review of Bernstein 1981 view details Abstract: In the last decade, programming language design has become strongly influenced by the insight that the languages should provide a set of structured features amenable to analytic verification. A typical example is the module, a collection of data and procedures governed by the rule that the data can be accessed only via these procedures, and therefore remain effectively hidden. The true reason for this rule is to enable the programmer to establish an invariant -- sometimes called verification condition -- a relation between the various members of the set of hidden data. The restriction of data access to these procedures guarantees the validity of the postulated invariant, once the programmer has established its truth upon exit from each procedure. Another, closely related, example is the monitor or interface module. The validity of the invariant is here upheld in a multiprocess environment by the strong rule of mutual exclusion of processes.

    This strong rule, however, poses scheduling problems, particularly in languages that contain the concept of process priority. Such a language is MODULA. In this paper, a variant, called SB-MODULA, is presented. Its modifications were dictated by considerations of verification and of lifting restrictions dictated by the desire to keep the implementation simple. As an example, signals -- here called conditions -- can be associated explicitly with a Boolean expression in their declaration. The meaning of a signal is that such an expression be true whenever the signal is sent. Its association by declaration allows a compiler to enforce this intention. For example, the declaration in MODULA

    bufferempty: SIGNAL; (*n = 0*)

    and the statements

    IF n = 0 THEN send(bufferempty) END

    and

    IF n = 0 THEN wait(bufferempty) END


    are expressed more briefly in SB-MODULA by

    bufferempty: CONDITION n = 0; send(bufferempty)

    wait(bufferempty)

    enforcing that n = 0 before signalling and after waiting for that condition.

    The other proposed variations concern the calling of procedures between interface modules. A distinction is made between an open call -- allowing other processes to enter the module and perhaps requiring a delay of the returning process -- and a closed call - - maintaining the virtual exclusion during execution of the called procedure. Moreover, the condition operators send and wait are supplemented by a mark operator that is similar to send; it marks a process waiting for that condition as ready for execution, but unlike send does not force it to be resumed immediately. This distinction accomodates a programmer's need to occasionally influence the process scheduler hidden in an implementation's kernel. This facility -- like the priority feature -- reveals the dilemma inherent in systems that pretend to describe multiprocessors, but must be able to hide the fact that a single processor is time-shared to execute the processes.

    The paper presents the results of a serious study and a wellstructured solution to a difficult problem in multiprogramming. It properly discusses the proposal in the light of program verification, and does not hesitate to present examples and to discuss the consequences for implementations. It should be studied carefully by anyone interested in the design of languages for multiprogramming.
          in ACM Computing Reviews 22(07) July 1981 view details