Somebody asked me, how do we represent the state of a sequential device in HOL?
And I am not quite sure. Mike himself wrote that it is simply about
incorporating time into the model, so that if we have a counter then we can
describe it by C(t+1) = C(t)+1, where C is its (visible) output and t
r
In the way Mike and colleagues modelled hardware, a device is modelled
as a predicate over the external wires (ports) of the device.
Information hiding is achieved by existential quantification
(relational composition). The basics of this are laid out in
https://www.cl.cam.ac.uk/techreports/UCAM
Right. You might write
Implementation(out) ⇔
∃cout.
counter cout ∧ filter cout out
where
counter cout ⇔ ∀t. cout t = t
filter inp out ⇔ ∀t. out(t) ⇔ prime(inp(t))
as your description of the implementation (where the counter component is
indeed visible but "hidden"
Well, arguably you are describing an implementation. Maybe we can be more
abstract. If the device has no "reset" function, then I guess it can be
specified simply by the predicate PRIME, i.e. PRIME(t) is the output of the
device at time t. If we do have a reset function, then presumably somethin
