Re: [isabelle] I need a fixed mutable array

On 14-06-18 16:19, Peter Lammich wrote:
On Di, 2014-06-17 at 10:56 -0500, Gottfried Barrow wrote:
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:
However, there is Imperative_HOL, which has a heap monad supporting
mutable arrays.


Thanks for the info. I never consider using anything but Isabelle/HOL, since it has the biggest user base. Limitations can sometimes be a good thing, by forcing me to figure out how to do things different.

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.

I searched on "array" at the AFP site before, but I didn't find that, since it's buried in the tar file. It's good that I didn't, but it's good to see it now, and see how they're implementing things with lists.

It might come in handy later, and the collections in general.

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.

I just need something to give me a decent model for the use a subset of assembly language instructions, which involves reading and writing to memory.

List and nat, they're part of the foundation of HOL. They're used a lot, so there's a lot of development around them. Proof can be a scary thought, so I try to play it safe, and keep things simple with lists, when I can.


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