Read/Write Spec

Read/write memory

The simplest form of read/write memory is a single read/write register, say of type V (for value), with arbitrary initial value. The following Spec module describes this (a lot of boilerplate for a simple variable, but we can extend it in many interesting ways): MODULE Register [V] EXPORT Read, Write = VAR m: V % arbitrary initial value APROC Read() - V = <> APROC Write(m) = <> END Register Now we give a spec for a simple addressable memory with elements of type V. This is like a collection of read/write registers, one for each address in a set A. In other words, it’s a function from addresses to data values. For variety, we include new Reset and Swap operations in addition to Read and Write. MODULE Memory [A, V] EXPORT Read, Write, Reset, Swap = TYPE M = A - V VAR m := Init() APROC Init() - M = <> RET m' % Choose an arbitrary function that is defined everywhere. FUNC Read(a) - V = <> APROC Write(a, v) = <><m(a) :="v"> APROC Reset(v) = <> v} % Set all memory locations to v. APROC Swap(a, v) - V = <> % Set location a to the input value and return the previous value. END Memory The next three sections describe code for Memory. </></></m(a)></></></></></>