[Haskell-cafe] Proving stuff about IORefs
miguelimo38 at yandex.ru
Sun Oct 17 06:49:35 EDT 2010
On 17 Oct 2010, at 05:21, Ben Franksen wrote:
> 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
That is not true. Consider the following function:
g r1 r2 = writeIORef r1 0 >> writeIORef r2 1 >> readIORef r1
This function behaves differently depending on whether r1 and r2 are the same IORef or not. Therefore, the property you want to prove doesn't hold for the partially-applied function
f = g r1.
More information about the Haskell-Cafe