COMP 317: Semantics of Programming Languages

The Maude code:

• simple.maude (the programming language)
• simpleSemantics.maude (its semantics)

Exercises

1. The following is a specification of Natural Numbers in OBJ:

   
       obj PEANO is 
   
         sort Nat .
   
         op  0 : -> Nat .
         op  succ : Nat -> Nat .
         op  _+_ : Nat Nat -> Nat [prec 48] .
         op  _*_ : Nat Nat -> Nat [prec 40] .
   
         vars M N : Nat .
   
         eq  M + 0  =  M .
         eq  M + succ(N)  =  succ(M + N) .
   
         eq  M * 0  =  0 .
         eq  M * succ(N)  =  M + M * N .
       endo
   
   

   "[prec 48]" declares the precedence of _+_ to be 48; multiplication is declared to have a lower precedence, following standard conventions.
   1. One model of this specification (let's call it A) interprets the sort Nat as Booleans ({true, false}), and interprets _+_ as exclusive-or (inequality). Find interpretations of the other operations that really do make A into a model of PEANO.
      (Hint: think of false as 0 and true as 1, and do arithmetic modulo 2.)
   2. Cut and paste PEANO into a file, and load it into the OBJ interpreter ("obj3" at the command-line to start the OBJ interpreter; "in <filename>" at the OBJ prompt to load the file). Try reducing some terms ("reduce <term> ." - remember the dot!). Try typing

          set trace on .
      

      at the OBJ prompt and then reduce some more terms. Try typing

          set trace whole on .
      

      and reduce more terms. ("set trace off ." and "set trace whole off ." to make it shut up again, and "q" to exit the interpreter.)
   
    
2. Linked Lists are a data structure for storing sequences of integers. A linked list is either null (empty), or consists of an integer value (the "head") and a linked list (the "tail" - in imperative languages, this is usually implemented as a pointer to the tail of the list). Given a linked list, l, we can create a new linked list by adding an integer value at the start of the list (so that value becomes the head, and l becomes the tail of the new linked list). Give an OBJ specification of the Abstract Data Type of linked lists.

Review Questions

1. By the end of Week 6, we should have covered, at least:

   
       obj EXP is pr ZZ .
                  dfn Var is QID .
   
         sort  Exp .
         subsorts  Var Int < Exp .
   
         op  _+_  : Exp Exp -> Exp [prec 10] .
         op  _*_  : Exp Exp -> Exp [prec 8] .
         op  _-_  : Exp Exp -> Exp [prec 10] .
         op   -_  : Exp -> Exp .
   
       endo 
       
   
       th STORE is pr EXP .
   
         sort Store .
       
         op  _[[_]] : Store Exp -> Int [prec 65] . 
       
         var  S : Store . 
         vars E1 E2 : Exp . 
         var  I : Int . 
   
         eq  S[[E1 + E2]]  =  (S[[E1]]) + (S[[E2]]) . 
         eq  S[[E1 * E2]]  =  (S[[E1]]) * (S[[E2]]) . 
         eq  S[[E1 - E2]]  =  (S[[E1]]) - (S[[E2]]) .
         eq  S[[- E1]]  =  - (S[[E1]]) .
         eq  S[[I]]  =  I .
   
       endth
   
   

   "The denotational semantics of the earlier lectures gives a model of STORE."
   
   1. This is an intuitive and, perhaps, slightly vague statement. Show that it is nevertheless true, in as much detail as you can.
   2. This states that denotational semantics is correct with respect to the OBJ semantics. How might we relate the two semantics "the other way round", and show that the OBJ semantics is correct with respect to the denotational semantics?