module abstractMemory [Addr, Data]

sig Memory {
	data: Addr -> lone Data
	}

pred init (m: Memory) {
	no m.data
	}

pred write (m, m': Memory, a: Addr, d: Data) {
	m'.data = m.data ++ a -> d
	}

pred read (m: Memory, a: Addr, d: Data) {
	let d' = m.data [a] | some d' implies d = d'
	}

fact Canonicalize {
	no disj m, m': Memory | m.data = m'.data
	}

assert WriteRead {
	all m, m': Memory, a: Addr, d1, d2: Data |
		write (m, m', a, d1) and read (m', a, d2) => d1 = d2
	}
check WriteRead

assert WriteIdempotent {
	all m, m', m": Memory, a: Addr, d: Data |
		write (m, m', a, d) and write (m', m", a, d) => m' = m"
	}
check WriteIdempotent