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
