module fixedSizeMemory [Addr, Data]

sig Memory {
	data: Addr -> one Data	
	}

-- non-deterministic initialization
pred init (m: Memory) {
	}

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

pred read (m: Memory, a: Addr, d: Data) {
	d = m.data [a]
	}

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