We present a framework for formalizing the semantics of expression evaluation using Abstract State Machines. Many programming languages allow some non-determinism for evaluating expressions. The semantics only have in common that arguments are evaluated before an operator is applied. The evaluation of one argument may be interleaved with the evaluation of the other arguments. However, programming languages usually restrict this most liberal evaluation order. For example, the expression evaluation may take into account short-circuit evaluation of boolean expressions which implies that right operands must not be evaluated before the complete left operand is evaluated. Our approach provides a generic expression evaluation semantics that only need to be instantiated adequatly. We demonstrate this approach by the example of Ada95, C, C++, Java, C#, and Fortran.

 

Online Copy

PDF (296 KB)

BibTeX Entry

@InProceedings{ZiDo03,
  author =       {Wolf Zimmermann and Axel Dold},
  title =        {A Framework for Modelling the Semantics of Expression Evaluation 
                  with Abstract State Machines},
  booktitle =    {Abstract State Machines - Advances in Theory and Applications
                  10th International Workshop, ASM 2003}, 
  pages =        {391-406},
  year =         2003,
  editor =       {Egon Boerger, Angelo Gargantini, Elvinia Riccobene},
  volume =       2589,
  series =       LNCS,
  publisher =    {Springer Verlag}
}