nextupprevious
Next:ConclusionUp:Operational Semantics of Rewriting Previous:Hint about Specifying

Discussion


Lazy evaluation is fascinating because it often has a better termination behavior than eager evaluation, while it is much more difficult to implement efficiently lazy evaluation than eager evaluation. Therefore some compromises have been proposed. The functional strategy[10] is one of them, which is often used in the field of the implementation of functional languages such as Miranda and Haskell. The operational semantics of a rewrite step and the annotated functional strategy in Miranda is also given[10]. They claim that the formal specification in a functional language has two advantages besides the well-defined semantics. First, the partial correctness of the specification can be confirmed by an implementation of the description language. Second, the dynamic behavior of the specified algorithms can be observed. We can say that the operational semantics of rewriting with the on-demand E-strategy in CafeOBJ has the same advantages.

Kamperman and Walters have proposed a transformation method for TRSs and terms to be rewritten so that lazy evaluation can be simulated on an implementation of eager evaluation: lazy rewriting on eager machinery[9]. The method concisely expresses the intricate interaction between pattern matching and lazy evaluation. Our operational semantics concisely expresses the same thing by the third equation for pm in Semantics4, viz if the top symbol of a term is not seemingly equal to that of a pattern but the term has been marked with an on-demand flag, pm retries to match the term with the pattern after evaluating the term.

We introduce two more examples of semantics written in formal languages. One is the operational semantics of an organic programming language GAEA[5] in Maude[3] a specification language based on rewriting logic[11], and the other the algebraic semantics of imperative programs in OBJ3[6]. Ishikawa et al.[8] have written the operational semantics of GAEA in Maude as an instance through a study on declarative description of reflective concurrent systems. Goguen and Malcolm[7] give the algebraic semantics of imperative programs in OBJ3 so as to introduce Computing Science students to formal reasoning about imperative programs. They do not only write the algebraic semantics of an imperative programming language, but also prove assertions about the behavior of programs written in the imperative programming language.

We introduce one more example of semantics written in formal languages. Goguen and Malcolm[7] give the algebraic semantics of imperative programs in OBJ3 so as to introduce Computing Science students to formal reasoning about imperative programs. They do not only write the algebraic semantics of an imperative programming language, but also prove assertions about the behavior of programs written in the imperative programming language. In future we are going to verify some properties of rewriting with the on-demand E-strategy with the operational semantics.
 


nextupprevious
Next:ConclusionUp:Operational Semantics of Rewriting Previous:Hint about Specifying


 


Kazuhiro Ogata

Mon Nov 29 13:47:22 JST 1999