Re: [isabelle] I need a fixed mutable array



On Di, 2014-06-17 at 10:56 -0500, Gottfried Barrow wrote:
> Hi,
> 
> I did a few searches to find whether there are mutable arrays in 
> Isabelle. It appears there's not, though I found a little info:

HOL itself does not support mutable arrays. 

However, there is Imperative_HOL, which has a heap monad supporting
mutable arrays.

Then there is afp/Collections/Lib/Diff_Array, which provides an
implementation of arrays that behaves purely functional, but is
efficient if only the last version is accessed.

However, if you are not after *efficient* executability, but only
looking for an abstract model of a memory, it makes no sense using the
above types, as the efficiency comes at teh price of additional
formalization overhead. 

--
  Peter





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.