CIS 425 Midterm II Solution

ML Datatypes

You are given the following datatype definitions that represent a simple network:

datatype machine = Machine of string

datatype network = 
    LAN of machine list
  | Connection of machine * network

Write an ML function search that takes two arguments: a machine and a network, checks whether the machine is part of the network, and returns true or false:

Solution

fun lookup m [] = false
  | lookup m (m'::ms) = (m=m') orelse (lookup m ms)

fun search m (LAN(ms)) = lookup m ms
  | search m (Connection(m',n)) = (m=m') orelse (search m n)

Types

Write a typechecker (in ML) for the following language.

datatype bop = PLUS | DIV | EQ

datatype Expression =
    Number of int
  | True | False
  | Binary of Expression * bop * Expression
  | Define of string * Expression * Expression 
  | Variable of string 

datatype ExpType = Integer | Boolean
exception TypeError

Solution

See solution to first midterm.

Proof Rules

The following proof rules can be used to prove partial correctness of small programs:

{P} S1 {Q}    {Q} S2 {R}
------------------------
   {P} S1;S2 {R}

      {P AND E} S {P}
------------------------------
{P} while (E) S {P AND (NOT E)

Using the rules prove that: {r=p-x*y} (while (x <> 0) { r:= r+y; x=x-1; }) {r=p}

Why does the proof only establish partial correctness?

Solution

{r=p-x*y AND x<>0} r:= r+y {r=p-(x+1)*y}   {r=p-(x+1)*y} x=x-1; {r=p-x*y}
-------------------------------------------------------------------------
     {r=p-x*y AND x<>0} r:= r+y; x=x-1; {r=p-x*y}
----------------------------------------------------------------
{r=p-x*y} (while (x <> 0) { r:= r+y; x=x-1; }) {r=p-x*y AND x=0}

The proof only establishes partial correctness because it says nothing about whether the loop terminates.

Higher-Order Functions

let fun f (x) = x+x
in f (7)
end 
------------------------
let fun f (x) = x+x
    val x = 3
in f (7) 
end
------------------------
let val x = 3
   fun f (x) = x+x
in f (7)
end
------------------------
let val x = 3
   fun f (y) = x+y
in f (7)
end
------------------------
let val x = 3
    fun f (y) = x+y
in let val x = 5
   in f (7)
   end
end 
------------------------
let val g = let val x = 3
                fun f (y) = x+y
            in f 
            end
in let val x = 5
   in g (7)
   end 
end
------------------------
let val x = 3
    fun f (y) = x+y
in let val x = 4
       fun g (h) = h (h (7))
   in g (f)
   end
end

Solution

Try them in SML.

Static Links

You are given a program with the following structure:

Main
  P
   Q
     R
  X
   Y

In one particular execution, the following procedures are called in the given order:

Main, X, Y, X, Y, Main, P, Q, R

None of the procedures returned yet. Draw the stack after the call to R. Your figure should include all activation records on the stack, and for each activation record, the name of the procedure being called, and the activation record to which the static link points.

Solution

Stack should contain frames for each of the procedures with the following links starting from the last call: R's link points to Q, Q's link points to P, P's link points to the immediately preceding frame for Main, Main's link points nowhere, Y's link points to the immediately preceding X, X's link points to the original Main, Y's link points to the immediately preceding X, X's link points to the immediately preceding Main, Main's link points nowhere.

Visited

times since September 21, 1999 (or the last crash).

sabry@cs.uoregon.edu