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 something like PRIME(t - SINCE_LAST_RESET(t)) might do it.
The point is that Mike's original approach, using recursive domain equations, apparently concealed the internal state completely. Mike wrote a remarkable technical report in 1981, with interesting discussion e.g. on page 8. His discussion of "machines" is already HOL-like, but his actual theory is still couched in terms of domains. Mike's report can temporarily be downloaded from here: http://www.cl.cam.ac.uk/~lp15/tmp/1981.pdf Many thanks! Larry > On 24 Apr 2018, at 07:22, Konrad Slind <konrad.sl...@gmail.com> wrote: > > 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-CL-TR-91.pdf > > There is a sequential circuit example in that tech. report, which may help. > > Konrad. > > > On Mon, Apr 23, 2018 at 9:09 AM, Lawrence Paulson <l...@cam.ac.uk> wrote: >> 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 >> represents time. >> >> But what if we have a primitive that doesn't expose its full state to the >> outside? Imagine a device that contains a counter that increments with every >> clock tick, but the counter value is hidden and the output is only a single >> bit to tell us whether the value of the counter is a prime number or not. >> Surely in such a case the counter itself would have to be visible in the >> formalisation even if no device was allowed to connect to it? >> >> Larry Paulson >> >> >> >> >> ------------------------------------------------------------------------------ >> Check out the vibrant tech community on one of the world's most >> engaging tech sites, Slashdot.org! http://sdm.link/slashdot >> _______________________________________________ >> hol-info mailing list >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
