Changeset 3557 for Papers/jarassembler2015
 Timestamp:
 Apr 24, 2015, 1:31:35 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/jarassembler2015/boenderjar2015.tex
r3555 r3557 241 241 A central design decision in our formalisation is the choice of how to encode memory. 242 242 The MCS51 has various memory spaces and registers that can be addressed with bytes and words. 243 \begin{lstlisting} 244 inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] := 245 Leaf: A > BitVectorTrie A O 246  Node: $\forall$n: nat. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n) 247  Stub: $\forall$n: nat. BitVectorTrie A n. 248 \end{lstlisting} 243 Using a complete associative map to capture an entire memory space, including large swathes of uninitialised data, would be incredibly inefficient and make any proof incredibly difficult due to the strain placed on Matita. 244 However, using a na\"ive data structured like an associationlist to encode memory would lead to inefficiencies when stepping through the semantics of a machine code program inside Matita. 245 We therefore use an indexed type, \texttt{BitVectorTrie}, to efficiently represent a memory space that may have `holes' of uninitialised or unspecified data: 246 \begin{lstlisting} 247 inductive BitVectorTrie (A: Type[0]): $\mathbb{N}$ $\rightarrow$ Type[0] := 248 Leaf: A $\rightarrow$ BitVectorTrie A O 249  Node: $\forall$n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n) 250  Stub: $\forall$n. BitVectorTrie A n. 251 \end{lstlisting} 252 The $\mathbb{N}$ index of the \texttt{BitVectorTrie} family records the maximum length of any path to stored data through the tree. 253 For a dependentlytyped encoding of a trie data structure, the \texttt{Leaf} and \texttt{Node} constructors are standard. 254 The novelty of \texttt{BitVectorTrie} lies in the \texttt{Stub} constructor, which intuitively represents a `hole' in the tree, and can appear 249 255 250 256 % Trie data structure and use of dependent types
Note: See TracChangeset
for help on using the changeset viewer.