[Haskell-cafe] Proving stuff about IORefs

[Ben Franksen]

I have a formal proof where I am stuck at a certain point.

Suppose we have a function

  f :: IORef a -> IO b

I want to prove that

  f r == do
    s1 <- readIORef r
    r' <- newIORef s1
    x <- f r'
    s3 <- readIORef r'
    writeIORef r s3
    return x

What happens here is that the temporary IORef r' takes the place of the
argument r, and after we apply f to it we take its content and store it in
the original r. This should be the same as using r as argument to f in the
first place.

How can I prove this formally?

Cheers
Ben