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
