1<HTML> 2<HEAD> 3<TITLE>HolBddLib</TITLE> 4 5 6 7<LINK rel = stylesheet type="text/css" 8 href = "http://www.cl.cam.ac.uk/users/mjcg/style.css" 9 title = "style.css"> 10 11 12 13</HEAD> 14 15<BODY> 16 17 18<IMG ALT="Picture of Lake Kananaskis + a picture of a BDD" 19 SRC="doc/HolBdd.jpg"> 20 21<H1>HolBddLib</H1> 22 23<UL> 24 25<LI> <A HREF="http://cvs.sourceforge.net/cgi-bin/viewcvs.cgi/hol/hol98/src/HolBdd/"> 26<TT>HolBddLib</TT> Version 2</A> is now available as part 27of <A HREF="http://www.cl.cam.ac.uk/~mjcg/InstallKananaskis.html">HOL98 [Kananaskis 0]</A>. 28 29<LI><A HREF="http://cvs.sourceforge.net/cgi-bin/viewcvs.cgi/~checkout~/hol/hol98/src/HolBdd/doc/HolBdd.ps.gz"> 30Compressed postscript documentation</A> from the 31<A HREF="http://cvs.sourceforge.net/cgi-bin/viewcvs.cgi/hol/hol98/src/HolBdd/doc/"> 32Documentation directory for <TT>HolBddLib</TT> Version 2</A> 33 34</UL> 35 36<P> 37<HR> 38<P> 39 40 41<H1>Edited extracts from the preface to the Version 2 documentation</H1> 42 43<p> 44In the fully expansive (or LCF-style) approach to theorem proving, theorems are represented by an abstract type 45whose primitive operations are the axioms and inference rules of a 46logic. Theorem proving tools are implemented by composing together 47the inference rules using ML programs. 48 49<p> 50This idea can be generalised to computing valid judgements that 51represent other kinds of information. In particular, consider 52judgements <FONT color="red">(a,<font face="symbol">r</font>,t,b)</FONT>, 53where <FONT color="red">a</FONT> is a set of boolean terms 54(assumptions) that are assumed true, <FONT color="red"><font face="symbol">r</font></FONT> represents a variable 55order, <FONT color="red">t</FONT> is a boolean term all of whose free variables are boolean 56and <FONT color="red">b</FONT> is a BDD. Such a judgement is valid if under the assumptions 57<FONT color="red">a</FONT>, the BDD representing <FONT color="red">t</FONT> 58with respect to <FONT color="red"><font face="symbol">r</font></FONT> is <FONT color="red">b</FONT>, 59and we will write <FONT color="red">a <font face="symbol">r</font> t --> b</FONT> 60when this is the case. 61 62<p> 63The derivation of "theorems" like <FONT color="red">a <font face="symbol">r</font> t --> b</FONT> can be viewed 64as "proof" in the style of LCF by defining an abstract type <tt>term_bdd</tt> 65that models 66judgements 67<FONT color="red"><span class="roman">a</span> <font face="symbol">r</font> 68<span class="roman">t</span> --> <span class="roman">b</span></FONT> analogously 69to the way the type <tt>thm</tt> models theorems <FONT color="red"><tt>|-</tt> t</FONT>. 70 71<p> 72<tt>HolBddLib</tt> Version 2 provides a 73kernel of representation judgement rules as 74infrastructure for building fully-expansive 75combinations of HOL theorem proving and BDD-based symbolic calculation 76algorithms, like model checkers. 77<p> 78<tt>HolBddLib</tt> currently contains two main structures: <tt>PrimitiveBddRules</tt> 79which defines a protected type <tt>term_bdd</tt> and rules for generating 80values of this type, and <tt>DerivedBddRules</tt> that contains derived 81rules for performing simple fixed-point calculations. There is also a 82theory <tt>DerivedBddRulesTheory</tt> containing the theorems on 83reachability and fixed points needed by the derived rules, 84and two small subsidiary structures <tt>Varmap</tt> and <tt>PrintBdd</tt>. 85 86<p> 87The development of <tt>HolBddLib</tt> has gone through two phases. The 88first phase consisted in experiments with different ways of linking 89higher order logic terms to binary decision diagrams. 90These are described in the paper 91<A HREF="http://www.cl.cam.ac.uk/~mjcg/TPHOLs2000/TPHOLs2000Final.ps.gz"> 92<i>Reachability programming in HOL98 using BDDs</i></A>. 93 94<p> 95 96<tt>HolBddLib</tt> Version 2 provides a less developed interactive 97programming environment than 98<A HREF="http://www.cl.cam.ac.uk/users/mjcg/HolBddLib/index.version1.html">Version 1</A>. 99It is more oriented to 100providing a clean and simple API allowing implementers to create their 101own combinations of model checking and theorem 102proving. Such a combination could be a Voss-like verification 103platform. 104 105<P> 106<HR> 107<P> 108 109<ADDRESS> 110MICHAEL J. C. GORDON<BR> 111 112University of Cambridge<BR> 113<A HREF="http://www.cl.cam.ac.uk/home.html">Computer Laboratory</A><BR> 114<A HREF="http://www.cl.cam.ac.uk/site-maps/gates2.html">Room FE19</A><BR> 115<A HREF="http://www.cl.cam.ac.uk/site-maps/gates.html">William Gates Building</A><BR> 116JJ Thomson Avenue<BR> 117Cambridge CB3 0FD<BR> 118United Kingdom<BR> 119work phone: +44 1223 334627<BR> 120work fax: +44 1223 334678<BR> 121UK <A HREF="http://www.efax.com">eFax</A>: +44 870 1612485<BR> 122US <A HREF="http://www.efax.com">eFax</A>: (509) 692-9378<BR> 123home: +44 1223 362123<BR> 124email: <A HREF = "mailto:mjcg@cl.cam.ac.uk"><KBD>mjcg@cl.cam.ac.uk</KBD></A> 125</ADDRESS> 126 127 128 129</BODY> 130</HTML> 131 132 133
