Spring 2002, CSE 428: Assignment 2


Distributed: Jan 26.
Due: Feb 7 in class.
Total maximum score: 100 points.

The purpose of this assignment is to provide experience with interpretation of expressions and simple commands.
  1. [Points 20] Consider the following boolean expressions:

    
       (1) if x = 0 then true else (x = 1 or x > 1 or 1/x > 1).
       (2) x = 0 or x = 1 or x > 1 or 1/x > 1
    
    

    Assuming that x is declared as an integer, and that at the moment in which the expressions are evaluated x is associated to a non-negative number, say what are the results (true, false or error), depending on the value of x, of (1) and (2) when
    (a) "or" is interpreted as a strict operator
    and when
    (b) "or" is interpreted as a non-strict operator


  2. [Points 20] Assume that we want to enrich the language of boolean expressions with the boolean operator "implies" (logical implication), by adding the production

       Exp ::= Exp implies Exp
    

    and with the following meaning:

    
          r |- e1  eval  false 
       ---------------------------
         r |- (e1 implies e2) eval true
    
    

    
    
          r |- e1  eval  true     r |- e2  eval  v 
       ------------------------------------------------
                  r |- (e1 implies e2)  eval v
    
    

    Say what is the result (true, false or error) of the following expression, where x is declared as an integer:

       x > 0 implies (x = 1 or x > 1 or 1/x > 1)
    
    
  3. [Points 10] For each of the following three while commands, say for which initial values of x it eventually terminates. Assume that x is declared as an integer variable.

       (1) while x > 0 do x := x - 1
       (2) while not (x = 0) do  x := x - 1
       (3) while x > 0 do x := x + 1
    

    Note: we say that a while command "terminates" when the condition is or becomes false (sooner or later).


  4. [Points 20] Assume that we have the following type rules for a small language of expressions.

                           tm |- Exp1 : real   tm |- Exp2 : real  
    ________________      _______________________________________
    tm |-  x : tm(x)             tm |- Exp1 + Exp2 : real
    
    


    tm |- Exp : int        tm |- Exp1 : int   tm |- Exp2 : int  
    ________________       _______________________________________
    tm |- Exp : real              tm |- Exp1 + Exp2 : int
    
    

    Assume also that the variables x and y are also allowed as expressions. Write down all the type mappings, tm, such that tm assigns these two variables a type and such that

                   tm |- x + y : real
    

    is provable.

  5. [Points 30] Consider two looping constructions. The while loop is given an operational semantics in class and on page 59 of the textbook. Consider the repeat-until loop given by the following operational semantics. (This loop operator is inspired by one in Pascal and is sometimes called a do.)

    sigma1 |- Stm ==> sigma2     sigma2 |- Exp eval false
    _____________________________________________________
         sigma1 |- repeat Stm until Exp ==> sigma2
    

    sigma1 |- Stm ==> sigma0  
                sigma0 |- Exp eval true 
                           sigma0 |- repeat Stm until Exp ==> sigma2
    ________________________________________________________________
         sigma1 |- repeat Stm until Exp ==> sigma2
    

    (This last rules has three premises, listed over each other so it fits on a page better.) Do the following two things:

    1. Write an expression using sequencing (semicolon), conditional, and while that is equivalence to repeat-until.
    2. Write an expression using sequencing (semicolon), conditional, and repeat-until that is equivalence to while.

    If you wish, you may also use the skip statement, if necessary, which is defined as simply

    
    ___________________________
      sigma |- skip ==> sigma