[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