Go home now Header Background Image
Search
Submission Procedure
share: |
 
Follow us
 
 
 
 
Volume 3 / Issue 5

available in:   PDF (76 kB) PS (24 kB)
 
get:  
Similar Docs BibTeX   Write a comment
  
get:  
Links into Future

J.UCS Special ASM Issue. Part II.

Egon Börger (Universitá di Pisa, Italy)
boerger@di.unipi.it

In J.UCS 3.4 we have explained the context of "Ten Years of Gurevich's Abstract State Machines" of the special ASM issue for which Part II is appearing now. As announced at the end of Part I, this second part is devoted to applications of ASMs to classical problems of programming and software engineering. Two papers deal with semantics of programming languages, two papers with methods for building correct compilers and three papers with integrating ASMs into the software development life cycle.

Before I summarize the papers appearing here let me provide some technical data on this special ASM issue of J.UCS. An international call for submission of papers has been distributed in the first half of 1996, the deadline was December 1996. The first round of the reviewing process was finished at the beginning of March, the second round at the beginning of May 1997. Assisted by 76 review reports (ideally four per submission) I have accepted 7 papers for the April issue and 7 for the May issue, out of 21 submissions. One paper is still in the reviewing process and may appear in the next issue of J.UCS.

In the paper Montages Specifications of Realistic Programming Languages by P. Kutter and A. Pierantonio the successful application of ASMs to the description of the dynamics of real programming languages like Prolog, C, Occam, VHDL, C++ is enhanced by a semi-visual formalism that allows one to integrate into the ASM specification method a transparent formalization of the relevant static programming language features. In the paper The Formal Specification of Oberon the same authors illustrate their method through a formal but relatively compact ASM specification of the semantics of Oberon which includes both the dynamic and the static aspects (including the syntax).

The paper On the Construction of Correct Compiler Back-Ends: An ASM Approach by W. Zimmermann and T. Gaul uses ASMs for provably correct bottom-up rewriting systems specifications for back-end compilers which translate intermediate languages (basic block graphs) into binary machine code of a register based RISC processor with performance of the same order of magnitude as code generated by non-optimizing unverified C-compilers. The proofs are general in the sense that they make no specific assumptions on the instruction set of the intermediate language and of the target machine so that really a generator is defined which is parameterized by a term rewrite system, the intermediate and the target language and a register assignement algorithm. It is remarkable that all proofs in this paper have been machine checked using PVS, thus showing in particular that PVS can be put to use in a fruitful way to machine check ASM based reasoning on program development.

The paper Correctness Proof of a Distributed Implementation of Prolog by Means of ASMs by L. Araujo specifies an extension of the WAM for (AND- and OR-) parallel execution of Prolog on distributed memory and proves its correctness. The construction illustrates nicely the rather typical reusability property of ASM specifications and verifications: it

builds upon and extends the specification and correctness proof of the sequential WAM for ISO standard Prolog developed in [Börger and Rosenzweig 1994].

The three last papers deal with Integrating ASMs into the Software Development Life Cycle as the title of the paper by myself and L. Mearelli says. This paper presents a structured software engineering method which allows the software engineer to control efficiently the modular development and the maintenance of well documented, formally inspectable and smoothly modifiable code out of rigorous ASM models for requirement specifications. It defines an ASM model for the requirement specifciation and refines it (in a way which is proved to be correct) to a model which in the paper Refining an ASM Specification of the Production Cell to C++ Code by L. Mearelli is then refined to C++ code which has been validated through extensive experimentation. The paper also shows that the code properties of interest (like correctness, safety, liveness and performance conditions) can be proved at high levels of abstraction by traditional and reusable mathematical arguments which have been computer verified by a model checking approach for ASMs developed by K. Winter and illustrated in her paper Model Checking for Abstract State Machines.

We hope the reader will benefit from the ASM papers appearing here and will be tempted to try the method for his next challenging application problem.

References

[Börger and Rosenzweig 1994] E. Börger and D. Rosenzweig: ``The WAM Definition and Compiler Correctness''; C.Beierle, L.Plümer (Eds.), Logic Programming: Formal Methods and Practical Applications, North-Holland, Series in Computer Science and Artificial Intelligence (1994), 20-90