%!PS-Adobe-1.0
%%BoundingBox: 0 0 612 792
%%Creator: KDE 2.1 HTML Library
%%Title: file:/home/baford/pers/log/MIT/6.897-StateMachines/Dict.html
%%CreationDate: Thu May 17 16:55:48 2001
%%Orientation: Portrait
%%Pages: 9
%%DocumentFonts: Helvetica-Bold Helvetica Helvetica-Italic Lucidatypewriter
%%EndComments
%%BeginProlog
% Prolog copyright 1994-2000 Trolltech. You may copy this prolog in any way
% that is directly related to this document. For other use of this prolog,
% see your licensing agreement for Qt.
/d/def load def/D{bind d}bind d/d2{dup dup}D/B{0 d2}D/W{255 d2}D/ED{exch d}D/D0
{0 ED}D/LT{lineto}D/MT{moveto}D/ND/.notdef d/S{stroke}D/F{setfont}D/SW{
setlinewidth}D/CP{closepath}D/RL{rlineto}D/NP{newpath}D/CM{currentmatrix}D/SM{
setmatrix}D/SC{aload pop setrgbcolor}D/BSt 0 d/LWi 1 d/PSt 1 d/Cx 0 d/Cy 0 d
/WFi false d/OMo false d/BCol[1 1 1]d/PCol[0 0 0]d/BkCol[1 1 1]d/LArr[[][][10 3
][3 10][3 3][3 3][5 3 3 3][3 5 3 3][5 3 3 3 3 3][3 5 3 3 3 3]]d/GPS{PSt 1 ge
PSt 5 le and{{LArr PSt 1 sub 2 mul get}{LArr PSt 2 mul 1 sub get}ifelse}{[]}
ifelse}D/QS{PSt 0 ne{LWi SW gsave PCol SC true GPS 0 setdash S OMo PSt 1 ne and
{grestore BkCol SC false GPS dup 0 get setdash S}{grestore}ifelse}if}D/BDArr[
0.06 0.12 0.37 0.50 0.63 0.88 0.94]d/defM matrix d/BF{gsave BSt 1 eq{BCol SC
WFi{fill}{eofill}ifelse}if BSt 2 ge BSt 8 le and{BDArr BSt 2 sub get setgray
fill}if BSt 9 ge BSt 14 le and{WFi{clip}{eoclip}ifelse defM SM pathbbox 3 index
3 index translate 4 2 roll 3 2 roll exch sub/h ED sub/w ED OMo{NP 0 0 MT 0 h RL
w 0 RL 0 h neg RL CP BkCol SC fill}if BCol SC 0.3 SW NP BSt 9 eq BSt 11 eq or{0
4 h{dup 0 exch MT w exch LT}for}if BSt 10 eq BSt 11 eq or{0 4 w{dup 0 MT h LT}
for}if BSt 12 eq BSt 14 eq or{w h gt{0 6 w h add{dup 0 MT h sub h LT}for}{0 6 w
h add{dup 0 exch MT w sub w exch LT}for}ifelse}if BSt 13 eq BSt 14 eq or{w h gt
{0 6 w h add{dup h MT h sub 0 LT}for}{0 6 w h add{dup w exch MT w sub 0 exch LT
}for}ifelse}if S}if BSt 24 eq{}if grestore}D/mat matrix d/w D0/h D0/x D0/y D0/C
D0/R{/h ED/w ED/y ED/x ED NP x y MT 0 h RL w 0 RL 0 h neg RL CP BF QS}D/ACR{/h
ED/w ED/y ED/x ED x y MT 0 h RL w 0 RL 0 h neg RL CP}D/CLSTART{/clipTmp matrix
CM d defM SM NP}D/CLEND{clip NP clipTmp SM}D/E{/h ED/w ED/y ED/x ED mat CM pop
x w 2 div add y h 2 div add translate 1 h w div scale NP 0 0 w 2 div 0 360 arc
mat SM BF QS}D/CRGB{255 div 3 1 roll 255 div 3 1 roll 255 div 3 1 roll}D/BC{
CRGB BkCol astore pop}D/BR{CRGB BCol astore pop/BSt ED}D/WB{1 W BR}D/NB{0 B BR}
D/PE{setlinejoin setlinecap CRGB PCol astore pop/LWi ED/PSt ED LWi 0 eq{0.25
/LWi ED}if}D/P1{1 0 5 2 roll 0 0 PE}D/ST{defM setmatrix concat}D/qtfindfont{
true exch{exch pop dup 0 get dup findfont dup/FontName get 3 -1 roll eq{exit}{
pop}ifelse}forall exch}d/qtdefinefont{dup 1 get/fxscale exch def 2 get/fslant
exch def exch/fencoding exch def[fxscale 0 fslant 1 0 0]makefont fencoding
false eq{}{dup maxlength dict begin{1 index/FID ne{def}{pop pop}ifelse}forall
/Encoding fencoding def currentdict end}ifelse definefont pop}d/MF{qtfindfont
qtdefinefont}D/MSF{findfont exch/slant exch d[1 0 slant 1 0 0]makefont
definefont pop}D/DF{findfont/FONTSIZE 3 -1 roll d[FONTSIZE 0 0 FONTSIZE -1 mul
0 0]makefont d}D/ty 0 d/Y{/ty ED}D/T{PCol SC ty MT 1 index dup length exch
stringwidth pop 3 -1 roll exch sub exch div exch 0 exch ashow}D/QI{/C save d
pageinit/Cx 0 d/Cy 0 d/OMo false d}D/QP{C restore showpage}D
%%EndProlog
%%BeginSetup
/pageinit {
% lazy-margin hack: QPrinter::setFullPage(FALSE)
36 22 translate
% 191*264mm (portrait)
0 748 translate 1 -1 scale/defM matrix CM d } d
% Fonts and encodings used
/Helvetica-BoldList [
[ /Helvetica-Bold 1.0 0.0 ]
[ /Helvetica-Bold 0.936266 0 ]
] d
% No embeddable font for Helvetica-Bold found
/FE0[/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND
/ND/ND/ND/ND/ND/ND/ND/ND/space/exclam/quotedbl/numbersign/dollar/percent
/ampersand/quotesingle/parenleft/parenright/asterisk/plus/comma/hyphen/period
/slash/zero/one/two/three/four/five/six/seven/eight/nine/colon/semicolon/less
/equal/greater/question/at/A/B/C/D/E/F/G/H/I/J/K/L/M/N/O/P/Q/R/S/T/U/V/W/X/Y/Z
/bracketleft/backslash/bracketright/asciicircum/underscore/grave/a/b/c/d/e/f/g
/h/i/j/k/l/m/n/o/p/q/r/s/t/u/v/w/x/y/z/braceleft/bar/braceright/asciitilde/ND
/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND/ND
/ND/ND/ND/ND/ND/ND/space/exclamdown/cent/sterling/currency/yen/brokenbar
/section/dieresis/copyright/ordfeminine/guillemotleft/logicalnot/hyphen
/registered/macron/degree/plusminus/twosuperior/threesuperior/acute/mu
/paragraph/periodcentered/cedilla/onesuperior/ordmasculine/guillemotright
/onequarter/onehalf/threequarters/questiondown/Agrave/Aacute/Acircumflex/Atilde
/Adieresis/Aring/AE/Ccedilla/Egrave/Eacute/Ecircumflex/Edieresis/Igrave/Iacute
/Icircumflex/Idieresis/Eth/Ntilde/Ograve/Oacute/Ocircumflex/Otilde/Odieresis
/multiply/Oslash/Ugrave/Uacute/Ucircumflex/Udieresis/Yacute/Thorn/germandbls
/agrave/aacute/acircumflex/atilde/adieresis/aring/ae/ccedilla/egrave/eacute
/ecircumflex/edieresis/igrave/iacute/icircumflex/idieresis/eth/ntilde/ograve
/oacute/ocircumflex/otilde/odieresis/divide/oslash/ugrave/uacute/ucircumflex
/udieresis/yacute/thorn/ydieresis]d
/F1 FE0 Helvetica-BoldList MF
/F2 17/F1 DF
/F3 FE0 Helvetica-BoldList MF
/F4 13/F3 DF
/F5 FE0 Helvetica-BoldList MF
/F6 11/F5 DF
/HelveticaList [
[ /Helvetica 1.0 0.0 ]
[ /Helvetica 0.987625 0 ]
] d
% No embeddable font for Helvetica found
/F7 FE0 HelveticaList MF
/F8 10/F7 DF
/F9 FE0 Helvetica-BoldList MF
/F10 10/F9 DF
/Helvetica-ItalicList [
[ /Helvetica-Italic 1.0 0.0 ]
[ /Helvetica-Oblique 0.987625 0 ]
] d
% No embeddable font for Helvetica-Italic found
/F11 FE0 Helvetica-ItalicList MF
/F12 10/F11 DF
/LucidatypewriterList [
[ /Lucidatypewriter 1.0 0.0 ]
[ /Courier 1 0 ]
] d
% No embeddable font for Lucidatypewriter found
/F13 FE0 LucidatypewriterList MF
/F14 10/F13 DF
%%EndSetup
%%Page: 1 1
%%BeginPageSetup
QI
%%EndPageSetup
W BC
/OMo false d
[1 0 0 1 0 0]ST
CLSTART
0 0 540 748 ACR
CLEND
0 0 B 0 0 PE
WB
0 0 540 748 R
B P1
NB
F2 F
41 Y(Dictionary Abstractions and Implementations in)409 10 T
62 Y(Isabelle/HOL)109 10 T
F4 F
93 Y(Bryan Ford)72 10 T
F6 F
146 Y(Introduction)66 10 T
F8 F
171 Y(This case study examines a very basic object-oriented abstraction: the dictionary. Fundamentally, a dictionary is)514 10 T
184 Y(a collection of (name, value) associations, generally allowing only one value for a given name. The standard)490 10 T
197 Y(minimum set of operations that any dictionary can be expected to support is as follows:)402 10 T
F10 F
236 Y(Insert(n, v))55 50 T
F8 F
(: enter a new (name, value) pair, or if the name already has an association, replace its)391 105 T
249 Y(existing association with a new value.)172 50 T
1 B BR
36 229 7 7 E
F10 F
262 Y(Remove(n))54 50 T
F8 F
(: remove any association that may exist for a given name.)264 104 T
36 255 7 7 E
F10 F
275 Y(Lookup(n))50 50 T
F8 F
(: find the value currently associated with the given name, if one exists.)323 100 T
36 268 7 7 E
298 Y(Of course, in practice dictionaries often provide additional capabilities, such as to iterate over all the \(name,)491 10 T
311 Y(value\) pairs in the dictionary, to remove and return an arbitrary entry, or even to compose multiple dictionaries)506 10 T
324 Y(together or split them apart. However, in this case study, I only deal with the minimal set of methods above.)500 10 T
350 Y(There are a tremendous number of ways in which dictionaries can be implemented, with a wide variety of)477 10 T
363 Y(performance characteristics; a huge body of fundamental computer science theory is devoted solely to)468 10 T
376 Y(implementing this one abstraction efficiently. In this case study I used the Isabelle/HOL theorem prover to)488 10 T
389 Y(formalize and prove the operational correctness of three different well-known methods of implementing)480 10 T
402 Y(dictionaries: lists, hash tables, and binary search trees. First I will describe how the dictionary abstraction itself is)520 10 T
415 Y(formalized, then how each of the implementations in turn is formalized and proven correct.)417 10 T
441 Y(In this formalization, I currently)143 10 T
F12 F
(only)19 156 T
F8 F
(deal with correctness, and not with complexity \(runtime and storage)314 178 T
454 Y(characteristics\). I would like to do so at some point, and with its growing support library for real numbers I)492 10 T
467 Y(expect this to become practical in Isabelle before too long; however, at the moment Isabelle's library does not yet)520 10 T
480 Y(have the exponential/logarithmic machinery needed to formalize worst-case complexity properties of algorithms)514 10 T
493 Y(such as these, let alone the probabiility theory that would be needed to formalize average-case behavior.)481 10 T
F6 F
534 Y(The Dictionary Abstraction)142 10 T
F8 F
559 Y(The first task of course was to formalize the notion of "dictionary" as an abstraction. In Isabelle/HOL, the)486 10 T
572 Y(obvious choice seemed to be to model a dictionary as a function from names to values. More specifically, a)489 10 T
585 Y(dictionary is an object with the following type in Isabelle/HOL \(declared in)337 10 T
F10 F
(Dict.thy)38 350 T
F8 F
(\):)7 388 T
F14 F
611 Y(types ('a,'b) dict = "'a => 'b option")228 10 T
F8 F
637 Y(In other words,)72 10 T
F10 F
(dict)18 85 T
F8 F
(is a function type parameterized by two type variables -)257 106 T
F10 F
('a)9 366 T
F8 F
(, representing whatever type is)143 375 T
650 Y(used for names, and)93 10 T
F10 F
('b)9 106 T
F8 F
(, representing the type used for values. The function representing a dictionary takes a)395 115 T
663 Y(name and returns the type)121 10 T
F10 F
('b option)43 134 T
F8 F
(, which is a basic parameterized type supported by Isabelle's standard library)350 177 T
676 Y(which formalizes the notion of an "optional value": i.e., a value which can be either present \(expressed ')474 10 T
F10 F
(Some v)37 484 T
F8 F
('\))7 521 T
689 Y(or absent \(expressed as ')117 10 T
F10 F
(None)26 127 T
F8 F
('\). The function representing a dictionary returns the value associated with the)362 153 T
702 Y(requested name, if any, or returns)155 10 T
F10 F
(None)26 168 T
F8 F
(if there is no association for that name.)181 197 T
728 Y(Given this type definition, the three fundamental methods for dictionary objects are naturally formalized in)486 10 T
741 Y(Isabelle/HOL as higher-order function definitions:)230 10 T
QP
%%Page: 2 2
%%BeginPageSetup
QI
%%EndPageSetup
[1 0 0 1 0 -718]ST
[1 0 0 1 0 -718]ST
CLSTART
0 0 540 748 ACR
CLEND
0 0 B 0 0 PE
WB
0 718 540 748 R
B P1
1 B BR
F8 F
728 Y(Given this type definition, the three fundamental methods for dictionary objects are naturally formalized in)486 10 T
741 Y(Isabelle/HOL as higher-order function definitions:)230 10 T
F14 F
767 Y(constdefs)54 10 T
780 Y( dict_cons :: "('a,'b) dict")210 10 T
793 Y( "dict_cons == (%n. None)")198 10 T
819 Y( dict_insert :: "['a, 'b, ('a,'b) dict] => ('a,'b) dict")378 10 T
832 Y( "dict_insert n v D == (%n'. if n' = n then Some v else D n')")414 10 T
858 Y( dict_remove :: "['a, ('a,'b) dict] => ('a,'b) dict")354 10 T
871 Y( "dict_remove n D == (%n'. if n' = n then None else D n')")390 10 T
897 Y( dict_lookup :: "['a, ('a,'b) dict] => 'b option")336 10 T
910 Y( "dict_lookup n D == D n")192 10 T
F8 F
936 Y(Note that the percent sign is the lambda operator in Isabelle/HOL.)304 10 T
F10 F
(dict_cons)47 317 T
F8 F
(is simply the empty dictionary -)145 367 T
949 Y(i.e., the dictionary that returns)140 10 T
F10 F
(None)26 153 T
F8 F
(regardless of the name queried for;)161 182 T
F10 F
(dict_insert)53 346 T
F8 F
(constructs a new dictionary)127 402 T
962 Y(in which queries for the new name)157 10 T
F10 F
(n)6 170 T
F8 F
(will return the given value)117 179 T
F10 F
(v)6 299 T
F8 F
(and all other queries will be passed along to the)217 308 T
975 Y(previous dictionary;)90 10 T
F10 F
(dict_remove)61 103 T
F8 F
(similarly constructs a new dictionary in which queries for the removed name will)363 167 T
988 Y(cause)25 10 T
F10 F
(None)26 38 T
F8 F
(to be returned. The)91 67 T
F10 F
(dict_lookup)57 161 T
F8 F
(method, of course, is trivial: it simply invokes the dictionary as a)293 221 T
1001 Y(function with the appropriate name.)165 10 T
1027 Y(Strictly speaking, the)97 10 T
F10 F
(dict)18 110 T
F8 F
(type defined in the)86 131 T
F10 F
(types)28 220 T
F8 F
(statement above is actually a supertype of the type of)246 251 T
1040 Y(dictionaries we are actually interested in reasoning about: specifically, the)333 10 T
F10 F
(dict)18 346 T
F8 F
(type includes)59 367 T
F12 F
(all)9 429 T
F8 F
(possible functions)83 441 T
1053 Y(from names to values, whereas we are actually only interested in reasoning about dictionaries that can be)480 10 T
1066 Y(constructed from an empty dictionary from some sequence of insert and remove method calls - i.e., finite)484 10 T
1079 Y(dictionaries. To express this constraint, I use Isabelle's inductive set definition mechanism to construct an)486 10 T
1092 Y(explicit set representing all possible finite dictionaries:)246 10 T
F14 F
1118 Y(consts)36 10 T
1131 Y( dictset :: "('a,'b) dict set")222 10 T
1144 Y(inductive "dictset")114 10 T
1157 Y( intros)60 10 T
1170 Y( empty: "dict_cons : dictset")222 10 T
1183 Y( insert: "[| D : dictset; dict_lookup n D = None |])348 10 T
1196 Y( ==> dict_insert n v D : dictset")294 10 T
F8 F
1222 Y(Note that this set is built conservatively in the sense that it only builds dictionaries through sequences of)481 10 T
F10 F
1235 Y(dict_insert)53 10 T
F8 F
(operations which insert values for names that weren't already in the dictionary. I later prove the)443 66 T
1248 Y(stronger result that any dictionary resulting from any sequence of)301 10 T
F12 F
(arbitrary)38 314 T
F8 F
(insertions)45 355 T
F12 F
(and)16 403 T
F8 F
(removals is still in this)100 422 T
1261 Y(set - i.e., that)65 10 T
F10 F
(dictset)34 78 T
F8 F
(indeed represents the closure of all possible finite dictionaries. Of course, the set could)400 115 T
1274 Y(have been defined under the latter, stronger conditions in the first place. However, I found that defining the)502 10 T
F10 F
1287 Y(dictset)34 10 T
F8 F
(more conservatively in this way makes it much easier subsequently to prove interesting properties about)476 47 T
1300 Y(the elements of this set, because inductive proofs over the set only have to deal with insertions, and only)484 10 T
1313 Y(non-colliding insertions at that.)147 10 T
1339 Y(One final step I could have taken, but didn't out of pure laziness \(and lack of necessity for the purposes of this)508 10 T
1352 Y(project\), would be to use this)134 10 T
F10 F
(dictset)34 147 T
F8 F
(to declare a new Isabelle data type representing finite dictionaries. This)326 184 T
1365 Y(way, the)39 10 T
F10 F
(dict)18 52 T
F8 F
(type could actually represent the)148 73 T
F12 F
(exact)25 224 T
F8 F
(abstraction we're trying to deal with, rather than an)239 252 T
1378 Y(inclusive supertype.)89 10 T
1404 Y(Note that)45 10 T
F12 F
(all)9 58 T
F8 F
(of the above definitions, including the hypothetical "strict" finite dictionary data type if I had defined)460 70 T
1417 Y(one, are purely conservative extensions: i.e., they are guaranteed by Isabelle to be logically sound and consistent)518 10 T
1430 Y(as long as the basic HOL system is.)163 10 T
1456 Y(Based on these definitions, I proved a variety of basic properties of the dictionary abstraction, many of which)505 10 T
1469 Y(are also useful as lemmas in future proofs about dictionaries and dictionary implementations. The vast majority of)517 10 T
QP
%%Page: 3 3
%%BeginPageSetup
QI
%%EndPageSetup
[1 0 0 1 0 -1436]ST
[1 0 0 1 0 -1436]ST
CLSTART
0 0 540 748 ACR
CLEND
0 0 B 0 0 PE
WB
0 1436 540 748 R
B P1
1 B BR
F8 F
1456 Y(Based on these definitions, I proved a variety of basic properties of the dictionary abstraction, many of which)505 10 T
1469 Y(are also useful as lemmas in future proofs about dictionaries and dictionary implementations. The vast majority of)517 10 T
1482 Y(the proofs are handled almost entirely automatically by Isabelle, simply by unfolding a few definitions and invoking)520 10 T
1495 Y(the automatic reasoner (which uses a combination of simplification and natural deduction). A few examples of)504 10 T
1508 Y(the types of properties of interest are:)177 10 T
1534 Y(Result of lookups after various modification operations - e.g., looking up a name immediately after)449 50 T
1547 Y(inserting a value for that name, or looking up a name after inserting a value for a)368 50 T
F12 F
(different)39 421 T
F8 F
(name.)27 463 T
36 1527 7 7 E
1560 Y(Equivalence of dictionaries constructed by consecutive modifications referring to the same name - e.g.,)475 50 T
1573 Y(the notion that inserting values for the same name twice causes the first value to be "forgotten.")444 50 T
36 1553 7 7 E
1586 Y(Order-independence of modification operations for different names.)316 50 T
36 1579 7 7 E
1609 Y(Most of these lemmas naturally form simplification rules, which I feed to Isabelle's voracious simplifier by tagging)514 10 T
1622 Y(them with ')52 10 T
F10 F
([simp])32 62 T
F8 F
(' in the source code; this causes them to be used automatically during future proofs.)383 94 T
1648 Y(The only proofs in the abstract dictionary theory that weren't completely trivial were the proofs mentioned earlier)520 10 T
1661 Y(of the closedness of the)112 10 T
F10 F
(dictset)34 125 T
F8 F
(: i.e., that)44 159 T
F12 F
(all)9 206 T
F8 F
(possible sequences of arbitrary insertions and removals produce)294 218 T
1674 Y(finite dictionaries that are still in)146 10 T
F10 F
(dictset)34 159 T
F8 F
(. These proofs still couldn't be called hard by any means, however; they)330 193 T
1687 Y(mainly just involved invoking the appropriate induction rule initially \(which Isabelle conveniently generated)482 10 T
1700 Y(automatically when the)104 10 T
F10 F
(dictset)34 117 T
F8 F
(was defined in the first place\) and leading the theorem prover through the)342 154 T
1713 Y(appropriate sequence of case analyses.)178 10 T
F6 F
1754 Y(The List Implementation)129 10 T
F8 F
1779 Y(The first and simplest concrete, more-or-less realistic dictionary implementation is formalized in)439 10 T
F10 F
(ListDict.thy)57 452 T
F8 F
(. It)16 509 T
1792 Y(defines another type alias,)120 10 T
F10 F
(listdict)34 133 T
F8 F
(, and a corresponding set of functions representing the method)294 167 T
1805 Y(implementations, prefixed by)132 10 T
F10 F
(ld_)15 145 T
F8 F
(instead of)46 163 T
F10 F
(dict_)24 212 T
F8 F
(to distinguish them from the abstract dictionary's methods.)274 239 T
F14 F
1831 Y(types ('a,'b) listdict = "('a * 'b) list")246 10 T
1857 Y(constdefs)54 10 T
1870 Y( ld_cons :: "('a,'b) listdict")222 10 T
1883 Y( "ld_cons == []")138 10 T
1909 Y( ld_remove :: "['a, ('a,'b) listdict] => ('a,'b) listdict")390 10 T
1922 Y( "ld_remove n D == filter (%(n',v). (n' ~= n)) D")336 10 T
1948 Y( ld_insert :: "['a, 'b, ('a,'b) listdict] => ('a,'b) listdict")414 10 T
1961 Y( "ld_insert n v D == (n,v) # ld_remove n D")300 10 T
1987 Y( ld_lookup :: "['a, ('a,'b) listdict] => 'b option")348 10 T
2000 Y( "ld_lookup n D ==)150 10 T
2013 Y( \(if \(EX v. \(\(n,v\) : set D\)\))258 10 T
2026 Y( then Some (SOME v. ((n,v) : set D)))312 10 T
2039 Y( else None\)")168 10 T
F8 F
2065 Y(The formalization of this implementation takes advantage of Isabelle's powerful)361 10 T
F10 F
(list)16 374 T
F8 F
(data type, which is)86 393 T
2078 Y(parameterized to support finite lists of any desired type. In this case, a)326 10 T
F10 F
(listdict)34 339 T
F8 F
(is actually a list of (name, value))144 376 T
2091 Y(pairs. The)47 10 T
F10 F
(ld_remove)52 60 T
F8 F
(method uses)58 115 T
F10 F
(filter)24 176 T
F8 F
(, a library function that filters a list using an arbitrary boolean function,)324 200 T
2104 Y(to remove any elements referring to the name in question. The)288 10 T
F10 F
(ld_insert)44 301 T
F8 F
(method first removes any existing)157 348 T
2117 Y(element(s) with the same name from the list, and then prepends a new element to the list with the new name and)519 10 T
2130 Y(value. The)48 10 T
F10 F
(ld_lookup)48 61 T
F8 F
(implementation presented here is, strictly speaking, not very practical from an)356 112 T
2143 Y(implementation perspective: it uses Isabelle's)204 10 T
F10 F
(set)16 217 T
F8 F
(function, which takes a list and returns the set of all elements it)290 236 T
2156 Y(contains (ignoring any duplicates), and chooses an arbitrary element with a matching name from that set, on the)516 10 T
2169 Y(hope that there's at most one. I don't have any great excuse for defining this method this way: it would have)506 10 T
2182 Y(been more realistic, and probably not much harder, if any, to definite it in a more standard functional)460 10 T
2195 Y(programming style using a primitive-recursive function definition. But this way seemed a bit easier when I was)507 10 T
QP
%%Page: 4 4
%%BeginPageSetup
QI
%%EndPageSetup
[1 0 0 1 0 -2154]ST
[1 0 0 1 0 -2154]ST
CLSTART
0 0 540 748 ACR
CLEND
0 0 B 0 0 PE
WB
0 2154 540 748 R
B P1
1 B BR
F8 F
2156 Y(contains (ignoring any duplicates), and chooses an arbitrary element with a matching name from that set, on the)516 10 T
2169 Y(hope that there's at most one. I don't have any great excuse for defining this method this way: it would have)506 10 T
2182 Y(been more realistic, and probably not much harder, if any, to definite it in a more standard functional)460 10 T
2195 Y(programming style using a primitive-recursive function definition. But this way seemed a bit easier when I was)507 10 T
2208 Y(first starting to work on this theory, and I never got around to going back and fixing it.)404 10 T
2234 Y(Given these definitions, it is just as trivial to prove most of the basic properties we would expect as it was for)504 10 T
2247 Y(the abstract dictionary. The main exception is that the order-independence results that apply to the abstract)503 10 T
2260 Y(dictionary type do not carry over to list-based dictionaries: i.e., inserting values for two different names in two)511 10 T
2273 Y(different orders)73 10 T
F12 F
(do not)30 86 T
F8 F
(produce identical)77 119 T
F10 F
(listdict)34 199 T
F8 F
(s, since the resulting lists will have their elements in a different)286 233 T
2286 Y(order. However, this is OK because what we're really interested in verifying is that the implementation)471 10 T
F12 F
(behaves)37 484 T
F8 F
2299 Y(correctly for all possible sequences of method calls, and order-independence is not necessary in order to do)497 10 T
2312 Y(that.)22 10 T
2338 Y(So finally we reach the Big Kahuna: proving that the list-based dictionary is behaviorally equivalent to the)486 10 T
2351 Y(dictionary abstraction. The goal, as I formulated it, is to prove that after all possible sequences of modification)507 10 T
2364 Y(operations, the result of any query will be the same for)250 10 T
F10 F
(dict)18 263 T
F8 F
(and)17 284 T
F10 F
(listdict)34 304 T
F8 F
(. Isabelle's support for inductive sets)172 338 T
2377 Y(serves this purpose very well; I simply used it to define a simulation relation associating each possible)461 10 T
F10 F
(listdict)34 474 T
F8 F
2390 Y(resulting from a given sequence of operations to a corresponding abstract)342 10 T
F10 F
(dict)18 355 T
F8 F
(:)3 373 T
F14 F
2416 Y(consts)36 10 T
2429 Y( dict_ld_rel :: "(('a,'b) dict * ('a,'b) listdict) set")372 10 T
2442 Y(inductive "dict_ld_rel")138 10 T
2455 Y( intros)60 10 T
2468 Y( init: "(dict_cons, ld_cons) : dict_ld_rel")312 10 T
2481 Y( insert: "(D,L) : dict_ld_rel)216 10 T
2494 Y( ==> (dict_insert n v D, ld_insert n v L) : dict_ld_rel")432 10 T
2507 Y( remove: "(D,L) : dict_ld_rel)216 10 T
2520 Y( ==> (dict_remove n D, ld_remove n L) : dict_ld_rel")408 10 T
F8 F
2546 Y(Note that the single colon \()127 10 T
F10 F
(:)3 137 T
F8 F
(\) operator is Isabelle's set membership operator. Once this relation is defined,)359 140 T
2559 Y(proving behavioral equivalence is simply a matter of showing that)300 10 T
F10 F
(lookup)33 313 T
F8 F
(operations on corresponding elements)177 349 T
2572 Y(in this relation always yield the same result:)196 10 T
F14 F
2598 Y(theorem "(D,L) : dict_ld_rel ==> dict_lookup n D = ld_lookup n L")390 10 T
2611 Y( apply (erule dict_ld_rel.induct))198 10 T
2624 Y( apply (simp))90 10 T
2637 Y( apply (case_tac "n = na"))162 10 T
2650 Y( apply (simp_all))108 10 T
2663 Y( apply (case_tac "n = na"))156 10 T
2676 Y( apply (simp_all))102 10 T
F8 F
2702 Y(It is convenient that the dictionary abstraction, as formulated here, is completely deterministic: i.e., after any)496 10 T
2715 Y(given set of modifications \("input actions"\), there is one and only one valid result for each query method \(the)500 10 T
2728 Y("output actions"\). If, on the other hand, the dictionary abstraction was enhanced to support iteration over the)511 10 T
2741 Y(contents of the dictionary, then the abstraction would presumably allow the contents to be returned in any)491 10 T
2754 Y(order, and then the implementation-abstraction correspondence would not be one-to-one, but the possible)501 10 T
2767 Y(outputs of the implementation would have to be shown to be a subset of the possible outputs of the abstraction:)520 10 T
2780 Y(i.e., a full-fledged I/O Automata-style simulation relation. Implementing iteration support should not be too hard)517 10 T
2793 Y(given Isabelle's facilities; doing so is left as an exercise for the reader. :-\))336 10 T
F6 F
2834 Y(The Hash Table Implementation)168 10 T
F8 F
2859 Y(The second dictionary implementation I formalized in Isabelle is the classic hash table \()392 10 T
F10 F
(Hash.thy)44 402 T
F8 F
(\). This)31 446 T
2872 Y(implementation assumes that the hash table size is fixed for the lifetime of the dictionary \(i.e., it does not support)520 10 T
2885 Y(dynamically growing and shrinking hash tables\). However, it is parameterized by both the hash table size and)503 10 T
2898 Y(the hash function, so it is guaranteed to be operationally correct for all possible hash table sizes and hash)484 10 T
2911 Y(functions. The basic types and methods are defined as follows:)291 10 T
QP
%%Page: 5 5
%%BeginPageSetup
QI
%%EndPageSetup
[1 0 0 1 0 -2872]ST
[1 0 0 1 0 -2872]ST
CLSTART
0 0 540 748 ACR
CLEND
0 0 B 0 0 PE
WB
0 2872 540 748 R
B P1
1 B BR
F8 F
2872 Y(implementation assumes that the hash table size is fixed for the lifetime of the dictionary \(i.e., it does not support)520 10 T
2885 Y(dynamically growing and shrinking hash tables\). However, it is parameterized by both the hash table size and)503 10 T
2898 Y(the hash function, so it is guaranteed to be operationally correct for all possible hash table sizes and hash)484 10 T
2911 Y(functions. The basic types and methods are defined as follows:)291 10 T
F14 F
2937 Y(types 'a hashfunc = "'a => nat";)192 10 T
2963 Y(types ('a,'b) hashtab = "('a,'b) dict list";)264 10 T
2989 Y(constdefs)54 10 T
3002 Y( ht_cons :: "nat => ('a,'b) hashtab")258 10 T
3015 Y( "ht_cons l == SOME H. \(length H = l &)270 10 T
3028 Y( \(ALL i. \(i < l --> H!i = dict_cons\)\)\)")420 10 T
3054 Y( ht_remove :: "['a, ('a,'b) hashtab, 'a hashfunc] => ('a,'b) hashtab")456 10 T
3067 Y( "ht_remove n H F == list_update H (F n) (dict_remove n (H!(F n)))")444 10 T
3093 Y( ht_insert :: "['a, 'b, ('a,'b) hashtab, 'a hashfunc] => ('a,'b) hashtab")480 10 T
3106 Y( "ht_insert n v H F == list_update H (F n) (dict_insert n v (H!(F n)))")468 10 T
3132 Y( ht_lookup :: "['a, ('a,'b) hashtab, 'a hashfunc] => 'b option")420 10 T
3145 Y( "ht_lookup n H F == dict_lookup n (H!(F n))")312 10 T
F8 F
3171 Y(There are a couple oddities to this formalization worth noting. First, each method takes the hash function as a)507 10 T
3184 Y(separate argument, whereas strictly speaking it would probably be conceptually cleaner to encapsulate it in the)503 10 T
3197 Y(hash table data type. The only reason I didn't do it that way was because this way seemed slightly easier to work)518 10 T
3210 Y(with since it doesn't require building and taking apart pairs during every operation; in other words, sheer)480 10 T
3223 Y(laziness.)38 10 T
3249 Y(The other interesting thing to notice is that the hash table "implementation" actually uses the abstract dictionary:)516 10 T
3262 Y(specifically, each entry in the hash table is actually an abstract dictionary, into which the hash table)452 10 T
3275 Y(implementation simply "blindly tosses" all elements that happen to map to the same table entry. This formalization)520 10 T
3288 Y(essentially skirts around the issue of handling hash collisions by punting the problem)386 10 T
F12 F
(back)20 399 T
F8 F
(up to the original)78 422 T
3301 Y(high-level abstraction. It can certainly be argued that in doing this I haven't)352 10 T
F12 F
(completely)47 365 T
F8 F
(implemented a hash)90 415 T
3314 Y(table, since in practice some concrete method will have to be used to deal with hash table collisions. However, I)513 10 T
3327 Y(believe that this is in fact an excellent way to formalize the hash table "implementation" because)437 10 T
F12 F
(fully)18 450 T
F8 F
3340 Y(implementing a hash table merely involves instantiating the hash table code as defined above, then recursively)503 10 T
3353 Y(implementing the abstract dictionaries used in the hash table implementation by instantiating some other)478 10 T
3366 Y(dictionary imlpementation such as the simple)203 10 T
F10 F
(listdict)34 216 T
F8 F
(. However, since the exact implementation for these)243 250 T
3379 Y(sub-dictionaries isn't specified here,)167 10 T
F12 F
(any)16 180 T
F8 F
(such implementation can be instantiated as long as it satisfies the basic)325 199 T
3392 Y(properties that dictionaries must have: for example, hash collisions could instead be handled by building colliding)514 10 T
3405 Y(elements into a binary tree. Thus, this formulation provides a good separation of concerns and in that way)490 10 T
3418 Y(leverages the abstraction/implementation distinction to yield greater flexibility.)357 10 T
3444 Y(The definition of)75 10 T
F10 F
(ht_cons)39 88 T
F8 F
(above, which simply constructs a hash table (list) of the appropriate length in which)386 130 T
3457 Y(every entry is the empty dictionary, was probably not the easiest way to do this; it probably would have both)501 10 T
3470 Y(been simpler and had a closer correspondence to a practical implementation if I had defined it as a primitive)490 10 T
3483 Y(recursive function using Isabelle's)153 10 T
F10 F
(primrec)37 166 T
F8 F
(facility. As it was, it turned out that the most complicated proof)295 206 T
3496 Y(required in the whole theory was the rather mundane proof that such a list as)355 10 T
F10 F
(ht_cons)39 368 T
F8 F
(tries to create actually)100 410 T
3509 Y(exists. Ah, the virtues of hindsight.)166 10 T
3535 Y(Not too surprisingly, many of the proofs for the standard dictionary properties depend on a couple key)474 10 T
3548 Y(invariants, which are encoded in those theorems as assumptions:)299 10 T
3574 Y(The same hash function is used for all consecutive operations on the hash table.)366 50 T
36 3567 7 7 E
3587 Y(The hash function only returns values in the correct range given the size of the hash table.)415 50 T
36 3580 7 7 E
3610 Y(After the standard properties are proved, I again prove behavioral equivalence by defining an inductive set that)511 10 T
3623 Y(functions more or less as a simulation relation. The definition of the simulation relation is restricted according to)513 10 T
QP
%%Page: 6 6
%%BeginPageSetup
QI
%%EndPageSetup
[1 0 0 1 0 -3590]ST
[1 0 0 1 0 -3590]ST
CLSTART
0 0 540 748 ACR
CLEND
0 0 B 0 0 PE
WB
0 3590 540 748 R
B P1
1 B BR
F8 F
3610 Y(After the standard properties are proved, I again prove behavioral equivalence by defining an inductive set that)511 10 T
3623 Y(functions more or less as a simulation relation. The definition of the simulation relation is restricted according to)513 10 T
3636 Y(the invariants above, so that proofs using the relation automatically have those invariants available as premises.)512 10 T
3649 Y(In addition, since as I mentioned earlier the hash function is passed to all of the manipulation methods as a)487 10 T
3662 Y(separate parameter, the simulation "relation" actually consists of triples rather than pairs, so that the correct)496 10 T
3675 Y(hash function is always "carried along" with a given hash table. Given this definition, the actual proof of)479 10 T
3688 Y(behavioral equivalence was entirely identical to the proof used for list-based dictionaries.)408 10 T
F6 F
3729 Y(The Binary Search Tree Implementation)209 10 T
F8 F
3754 Y(The final dictionary implementation I formalized is the classic binary search tree. In the implementation)467 10 T
3767 Y(I formalized, no balancing of any kind is done; extending this formalization to some of the popular balancing)495 10 T
3780 Y(variants such as treaps, red-black trees, or splay trees should make for fun and interesting "future work." The)506 10 T
3793 Y(formalization of the basic tree structure uses of Isabelle's ML-style discriminated union data type facility:)479 10 T
F14 F
3819 Y(datatype ('a,'b) bt = Node "('a,'b) bt" "'a" "'b" "('a,'b) bt" | NoNode)426 10 T
F8 F
3845 Y(In other words, a binary tree is either an empty leaf node \()268 10 T
F10 F
(NoNode)40 278 T
F8 F
(\), or consists of a left subtree, a name, a)186 318 T
3858 Y(value, and a right subtree, respectively.)179 10 T
3884 Y(Most of the method implementations use Isabelle's built-in support for well-founded primitive recursive function)517 10 T
3897 Y(definition in order to operate recursively over this data type, which requires types to be declared separately from)516 10 T
3910 Y(the definitions themselves:)123 10 T
F14 F
3936 Y(consts)36 10 T
3949 Y( bt_cons :: "('a::linorder,'b) bt")294 10 T
3962 Y( bt_lookup :: "['a::linorder, ('a,'b) bt] => 'b option")408 10 T
3975 Y( bt_insert :: "['a::linorder, 'b, ('a,'b) bt] => ('a,'b) bt")438 10 T
3988 Y( bt_remove :: "['a::linorder, ('a,'b) bt] => ('a,'b) bt")414 10 T
4001 Y( bt_scan :: "('a::linorder,'b) bt => ('a * 'b) set")396 10 T
4027 Y( (* Internal helpers *))180 10 T
4040 Y( bt_merge :: "[('a::linorder,'b) bt, ('a,'b) bt] => ('a,'b) bt")462 10 T
4053 Y( bt_ltall :: "['a::linorder, ('a,'b) bt] => bool")378 10 T
4066 Y( bt_gtall :: "['a::linorder, ('a,'b) bt] => bool")378 10 T
4079 Y( bt_sorted :: "('a::linorder,'b) bt => bool")342 10 T
4105 Y(defs)24 10 T
4118 Y( bt_cons_def:)120 10 T
4131 Y( "bt_cons == NoNode")210 10 T
4157 Y(primrec)42 10 T
4170 Y( "bt_lookup n' (Node l n v r) =)228 10 T
4183 Y( \(if n' = n then Some v)258 10 T
4196 Y( else if n' < n then bt_lookup n' l)306 10 T
4209 Y( else bt_lookup n' r\)")318 10 T
4222 Y( "bt_lookup n' (NoNode) = None")228 10 T
4248 Y(primrec)42 10 T
4261 Y( "bt_insert n' v' (Node l n v r) =)246 10 T
4274 Y( \(if n' = n then Node l n v' r)300 10 T
4287 Y( else if n' < n then Node (bt_insert n' v' l) n v r)402 10 T
4300 Y( else Node l n v \(bt_insert n' v' r\)\)")414 10 T
4313 Y( "bt_insert n' v' (NoNode) = Node NoNode n' v' NoNode")366 10 T
4339 Y(primrec)42 10 T
QP
%%Page: 7 7
%%BeginPageSetup
QI
%%EndPageSetup
[1 0 0 1 0 -4308]ST
[1 0 0 1 0 -4308]ST
CLSTART
0 0 540 748 ACR
CLEND
0 0 B 0 0 PE
WB
0 4308 540 748 R
B P1
1 B BR
F14 F
4313 Y( "bt_insert n' v' (NoNode) = Node NoNode n' v' NoNode")366 10 T
4339 Y(primrec)42 10 T
4352 Y( bt_remove_Node:)138 10 T
4365 Y( "bt_remove n' (Node l n v r) =)228 10 T
4378 Y( \(if n' = n then bt_merge l r)294 10 T
4391 Y( else if n' < n then Node (bt_remove n' l) n v r)384 10 T
4404 Y( else Node l n v \(bt_remove n' r\)\)")396 10 T
4417 Y( "bt_remove n' (NoNode) = NoNode")240 10 T
F8 F
4443 Y(In addition,)52 10 T
F10 F
(bt_remove)53 65 T
F8 F
(requires a helper function,)119 121 T
F10 F
(bt_merge)47 243 T
F8 F
(, which merges the two disjoint subtrees)186 290 T
4456 Y("orphaned" when a node is removed into a single tree, in this case iby inserting the right subtree into the left:)502 10 T
F14 F
4482 Y(primrec)42 10 T
4495 Y( "bt_merge (Node l n v r) y = Node l n v (bt_merge r y)")378 10 T
4508 Y( "bt_merge NoNode y = y")186 10 T
F8 F
4534 Y(Finally, although these are all the methods that would theoretically be needed in a practical implementation of a)505 10 T
4547 Y(basic binary search tree, a few additional helper functions are very useful for proving stuff:)416 10 T
F14 F
4573 Y(primrec)42 10 T
4586 Y( "bt_ltall n' (Node l n v r) =)222 10 T
4599 Y( (n' < n & bt_ltall n' l & bt_ltall n' r)")342 10 T
4612 Y( "bt_ltall n' (NoNode) = True")222 10 T
4625 Y(primrec)42 10 T
4638 Y( "bt_gtall n' (Node l n v r) =)222 10 T
4651 Y( (n < n' & bt_gtall n' l & bt_gtall n' r)")342 10 T
4664 Y( "bt_gtall n' (NoNode) = True")222 10 T
4677 Y(primrec)42 10 T
4690 Y( "bt_sorted (Node l n v r) =)210 10 T
4703 Y( \(bt_gtall n l & bt_sorted l &)270 10 T
4716 Y( bt_ltall n r & bt_sorted r\)")270 10 T
4729 Y( "bt_sorted (NoNode) = True")210 10 T
F8 F
4755 Y(Essentially these functions define predicates which are used in the following correctness proofs to express the)509 10 T
4768 Y(critical invariants that allow the binary search tree algorithm to function properly. The most important is)478 10 T
4781 Y(obviously the last one, which builds on the first two: it expresses the property of a binary tree being properly)502 10 T
4794 Y(sorted for searching.)97 10 T
4820 Y(Note that in the type definitions in the)177 10 T
F10 F
(consts)33 190 T
F8 F
(section above, the)85 226 T
F10 F
('a)9 314 T
F8 F
(type for each method, which represents the)202 326 T
4833 Y(type used for names, is constrained to the)194 10 T
F10 F
(linorder)38 207 T
F8 F
(axiomatic type class (second-order type). This Isabelle)253 248 T
4846 Y(feature is analogous to Haskell's type classes, except that in this case type classes can be specified to have)493 10 T
4859 Y(arbitrary mathematical properties: in this case,)211 10 T
F10 F
(linorder)38 224 T
F8 F
(is the class of all types for which an ordering relationship)262 265 T
4872 Y(is defined on all members via the ')155 10 T
F10 F
(<)5 165 T
F8 F
(' operator, and the ordering relationship satisfies the standard properties)337 170 T
4885 Y(expected for total orders (reflexivity, transitivity, etc.). The same effect could have been accomplished without)510 10 T
4898 Y(the use of type classes by parameterizing the binary tree implementation with an explicit ordering function)485 10 T
4911 Y(assumed to have the desired properties (analogous to the hash function used in the hash table implementation);)513 10 T
4924 Y(however, given Isabelle's direct support for axiomatic type classes, doing it this way was naturally the simplest)506 10 T
4937 Y(approach, not to mention the most cool. :-\))204 10 T
4963 Y(Unsurprisingly, proving that all of the desired dictionary-like properties hold for this binary tree implementation)512 10 T
4976 Y(was not nearly as trivial as it was for the list and hash table implementations, but it was not that difficult either;)510 10 T
4989 Y(mostly it involved figuring out the right intermediate lemmas to prove in the right order. Naturally, a good chunk)517 10 T
5002 Y(of lemmas had to be proved right up front about the basic sortedness predicates above before anything)479 10 T
5015 Y(interesting could be proven about the actual dictionary operations. However, once that was done, most of the)510 10 T
5028 Y(proofs came fairly readily.)117 10 T
5054 Y(As usual, I finally defined a simulation relation between binary trees and abstract dictionaries using an inductive)505 10 T
5067 Y(set and proved that for all corresponding modification sequences the result of a lookup in the two models is)495 10 T
QP
%%Page: 8 8
%%BeginPageSetup
QI
%%EndPageSetup
[1 0 0 1 0 -5026]ST
[1 0 0 1 0 -5026]ST
CLSTART
0 0 540 748 ACR
CLEND
0 0 B 0 0 PE
WB
0 5026 540 748 R
B P1
1 B BR
F8 F
5028 Y(proofs came fairly readily.)117 10 T
5054 Y(As usual, I finally defined a simulation relation between binary trees and abstract dictionaries using an inductive)505 10 T
5067 Y(set and proved that for all corresponding modification sequences the result of a lookup in the two models is)495 10 T
5080 Y(identical. This proof itself turned out to be no more difficult than it was for the previous implementations; all the)515 10 T
5093 Y(real work happened in proving the basic properties of binary trees.)307 10 T
5119 Y(Isabelle does have one niggly problem that got in the way a few times: its automatic reasoning sometimes does)507 10 T
5132 Y(not deal too well with fairly trivial inequalities. For example, it never could seem to figure out automatically that a)514 10 T
5145 Y(proof goal with "a < b; b < a" as its premises is trivially valid. This is perhaps a likely area for future improvement)514 10 T
5158 Y(in the tool. :-\))67 10 T
F6 F
5199 Y(Undoable Dictionaries)117 10 T
F8 F
5224 Y(Finally, in order to extend the basic dictionary abstraction a bit in a way that seemed interesting at the time)491 10 T
5237 Y((though admittedly may not be particularly realistic in this precise formulation), I created an extended "undoable)509 10 T
5250 Y(document" abstraction \()111 10 T
F10 F
(Undo.thy)44 121 T
F8 F
(\) and a corresponding implementation \()181 165 T
F10 F
(LogDoc.thy)55 346 T
F8 F
(\). Essentially, a "document")128 401 T
5263 Y(in this model is simply a dictionary with one additional method:)286 10 T
F10 F
(undo)24 299 T
F8 F
(. Each call to a modification method \()174 323 T
F10 F
(insert)29 497 T
F8 F
5276 Y(or)10 10 T
F10 F
(remove)37 23 T
F8 F
(\) not only performs the appropriate modification operation but also saves a record of the modification)469 60 T
5289 Y(so that any previous version of the "document" can be recovered at any time by invoking the)427 10 T
F10 F
(undo)24 440 T
F8 F
(method one)55 467 T
5302 Y(or more times.)66 10 T
5328 Y(The difference between the abstraction and the implementation is simply in how this logging is done. In the)494 10 T
5341 Y(abstract implementation, a "document" is simply a list of complete versions of the dictionary, so that after a valid)516 10 T
5354 Y(sequence of modifications the head of the list is always the latest version and the tail is always the empty)481 10 T
5367 Y(dictionary (the "original version"). The)177 10 T
F10 F
(undo)24 190 T
F8 F
(method in this case simply pops the first item off the list.)262 217 T
5393 Y(In the more interesting implementation of this abstraction, a document consists of only the current)454 10 T
5406 Y((head) version of the dictionary, in conjunction with an RCS-style "reverse change log" containing all of the)498 10 T
5419 Y(information needed to get back to any previous version of the document. Each change log entry is represented)514 10 T
5432 Y(by this discriminated union data type:)171 10 T
F14 F
5458 Y(datatype ('a,'b) logentry =)162 10 T
5471 Y( LogInsert 'a (* Insert, not present *))342 10 T
5484 Y( | LogUpdate 'a 'b (* Insert, already present *))366 10 T
5497 Y( | LogRemove 'a 'b (* Remove, present *))318 10 T
5510 Y( | LogNull (* Remove, not present *))342 10 T
F8 F
5536 Y(The first two entry types are created by)182 10 T
F10 F
(insert)29 195 T
F8 F
(operations and the other two are created by)204 227 T
F10 F
(remove)37 434 T
F8 F
(operations.)52 474 T
5549 Y(The appropriate type of entry is selected in each case according to whether an association already existed for the)519 10 T
5562 Y(given name before the modification operation: if so, then the previous value is saved along with the affected)498 10 T
5575 Y(name. The)49 10 T
F10 F
(LogNull)38 62 T
F8 F
(entry type, created when a name is removed that was not already in the dictionary anyway,)417 103 T
5588 Y(reflects the design philosophy that each "requested change" should create a new version, regardless of whether)514 10 T
5601 Y(the operation really caused any)141 10 T
F12 F
(effective)40 154 T
F8 F
(change. Of course, this is one of those endlessly debatable fine points.)328 197 T
5627 Y(As with the basic dictionary abstraction and implementations, I proved behavioral equivalence between these)499 10 T
5640 Y(models by first proving a number of basic critical properties for each model individually, and then defining a)491 10 T
5653 Y(simulation relation between them and inductively proving that the result of a query is the same after any possible)515 10 T
5666 Y(sequence of modifications. Since it's all just more of the same, I won't bore you with details.)424 10 T
F6 F
5707 Y(Conclusion)61 10 T
F8 F
5732 Y(Formalized a couple marginally interesting object-oriented data abstractions and implementation algorithms. Had)519 10 T
5745 Y(fun. Isabelle is cool.)92 10 T
5771 Y(As far as making this case study available to others, I plan to submit it (with all the code) to the Isabelle folks in)509 10 T
5784 Y(case they want to include it in the Isabelle distribution as another example theory.)373 10 T
QP
%%Page: 9 9
%%BeginPageSetup
QI
%%EndPageSetup
[1 0 0 1 0 -5744]ST
[1 0 0 1 0 -5744]ST
CLSTART
0 0 540 748 ACR
CLEND
0 0 B 0 0 PE
WB
0 5744 540 748 R
B P1
1 B BR
F8 F
5745 Y(fun. Isabelle is cool.)92 10 T
5771 Y(As far as making this case study available to others, I plan to submit it (with all the code) to the Isabelle folks in)509 10 T
5784 Y(case they want to include it in the Isabelle distribution as another example theory.)373 10 T
5810 Y(Cheers,)36 10 T
5823 Y(Bryan)27 10 T
QP
%%Trailer
%%EOF