[Haskell-cafe] Proving stuff about IORefs

Ben Franksen ben.franksen at online.de
Sat Oct 16 21:21:03 EDT 2010


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



More information about the Haskell-Cafe mailing list