diff options
author | Norbert Preining <norbert@preining.info> | 2019-09-02 13:46:59 +0900 |
---|---|---|
committer | Norbert Preining <norbert@preining.info> | 2019-09-02 13:46:59 +0900 |
commit | e0c6872cf40896c7be36b11dcc744620f10adf1d (patch) | |
tree | 60335e10d2f4354b0674ec22d7b53f0f8abee672 /web/spiderweb/src/dijkstra |
Initial commit
Diffstat (limited to 'web/spiderweb/src/dijkstra')
-rw-r--r-- | web/spiderweb/src/dijkstra/README | 3 | ||||
-rw-r--r-- | web/spiderweb/src/dijkstra/binary.web | 267 | ||||
-rw-r--r-- | web/spiderweb/src/dijkstra/d.spider | 155 | ||||
-rw-r--r-- | web/spiderweb/src/dijkstra/make | 2 | ||||
-rw-r--r-- | web/spiderweb/src/dijkstra/sp.web | 28 |
5 files changed, 455 insertions, 0 deletions
diff --git a/web/spiderweb/src/dijkstra/README b/web/spiderweb/src/dijkstra/README new file mode 100644 index 0000000000..ab315905a0 --- /dev/null +++ b/web/spiderweb/src/dijkstra/README @@ -0,0 +1,3 @@ +The spider file for Dijkstra's language of guarded commands isn't really +very good. One problem is that it's hard to come up with ASCII representations +of the operators Dijkstra uses. Suggestions will be appreciated. diff --git a/web/spiderweb/src/dijkstra/binary.web b/web/spiderweb/src/dijkstra/binary.web new file mode 100644 index 0000000000..b0b2ebe38d --- /dev/null +++ b/web/spiderweb/src/dijkstra/binary.web @@ -0,0 +1,267 @@ +\input itemize +\def\title{Binary tree insertion} +\def\topofcontents{\null\vfill + \titlefalse % include headline on the contents page + \def\rheader{\hfil} + \centerline{\titlefont Inserting into an ordered binary tree} + \vfill} + +@*Preliminaries. +Our object is to design a verified binary tree insertion routine. +To make our lives easier, we will employ some simplifications: +\itemize +\item We will use iteration instead of recursion. +\item We will use Dijkstra's language of guarded commands +\item We will assume the existence of a tree data type, such that + if |t| is a tree either |t| is empty (|t=emptyset|) or + |t| has a left subtree, a right subtree, and a datum + (|t=<<l,d,r>>|). If |t=<<l,d,r>>|, we may write |t.l| for |l|, +|t.d| for |d|, and |t.r| for |r|. +\item We will assume sequences; if |s| is a sequence then either |s| +is empty (|s=empty|) or |s| is an element followed by a sequence (|s=z +Z|). +\item We have a membership operator |member| that will test for +membership in sequences or trees. +\enditemize +@ We want to talk about ordered binary trees, so we'll want the +notion. +@c +ordered.emptyset == true; +ordered.<<l,d,r>>==ordered.l & ordered.r &@| +(forall y:y member l: y<=d) &@| (forall y: y member r: y>=d); + +@ Our mission is to insert a datum |x| into a binary tree |T| such that +the resulting tree is ordered. +We'll do this by creating a new tree |t| which is ordered and the +membership of which is the union of the membership of |t| with +$\{x\}$. +We don't care exactly what happens if |x| is already in the tree, +although we could add a postcondition |x member T ==> T=t|. + +If we state our problem formally, we have +@c +{PRE: ordered.T} +{POST: (forall y::y member t <=> y member T | y=x) & ordered.t} + +@ Let us develop some notion of ``insertion at a node.'' +Perhaps we can use that as a guide to weakening the postcondition and +finding a loop invariant. +In essence what we will want to do is select some empty subtree of +|T|, and replace it with the tree |<<emptyset,x,emptyset>>|. +Let us generalize, and imagine that we have a variable |s| that +represents |T| and points at some node of |T| ``to be replaced.'' +Let |attach.t.s| denote the result of substituting |T| for the subtree +whose root is that node. +In particular if |s| points to the root of |T|, then |attach.t.s=t|. + +@ How can we compute |attach|? We've already seen that if |s| points +to the root of |T|, then |attach.t.s=t|. +Suppose |s| does not point to the root of |T|. +Then there is an |s`| that points to the parent of the node pointed to by +|s|. +Then, there is some |t`| such that |attach.t.s=attach.t`.s`|, and, +furthermore, either |t`=<<t,d,u>>| or |t`=<<u,d,t>>|, for some |u| and +|d|. + +So, let |s| be a sequence of records, and let each record contain: +\itemize +\item A choice (|left| or |right|) +\item A datum |d| +\item A tree |u| +\enditemize +and define +@c +attach.t.empty == t; +attach.t.(<<left,d,u>> s) == attach.<<t,d,u>>.s; +attach.t.(<<right,d,u>> s) == attach.<<u,d,t>>.s; + +@ Now we can imagine our insertion problem as being broken into two +parts. +First, we find the right place to insert |x|. +This means computing an |s| such that +|attach.<<emptyset,x,emptyset>>.s| is what we want. +Second, we have to compute |t| so that +|t=attach.<<emptyset,x,emptyset>>.s|. + +Let's imagine that we already have an |s|. +Then, we can change our postcondition by substituting |attach.t.s| for +|t|, and make that our loop invariant. +We then start out with |t=<<emptyset,x,emptyset>>|, and write a loop +that adds to |t| while removing from |s|. + +Since |s=empty| at the end of the loop, and since |attach.t.empty=t|, the +invariant conjoined with the negation of the guard gives us the +postcondition. +I leave it for the reader to show that the loop body leaves the +quantity |attach.t.s| unchanged. +@c +t := <<emptyset,x,emptyset>>; +{invariant (forall y::y member attach.t.s <=> y member T | y=x) & + ordered.(attach.t.s)} +{bound #s} +do s != empty -> + let choice, data, tree, S satisfy <<choice,data,tree>> S = s; + if choice = left -> + t,s := <<t,data,tree>>, S + [] choice = right -> + t,s := <<tree,data,t>>, S + fi +od +{POST: (forall y::y member t <=> y member T | y=x) & ordered.t} +@ It remains for us to compute a suitable |s| in the first part of the +program. +Let us write |X| for |<<emptyset,x,emptyset>>|. +Then we must assign to |s|, establishing +$$\hbox{| (forall y::y member attach.X.s <=> y member T +|| y=x) & ordered.(attach.X.s)|.% +}$$ +Since |y=x <=> y member X|, that is equivalent to +$$\hbox{ +| (forall y::y member attach.X.s <=> y member T || y member X) & +ordered.(attach.X.s)|.}$$ + +Let us imagine we have a variable |t| such that |T=attach.t.s|. +Then we need +$$\hbox{|y member attach.X.s <=> y member attach.t.s || y member X|}$$ +Now we make use of a property of |attach|, viz.\ +|(forall X::y member attach.X.s <=> y member X || y member +attach.emptyset.s)|. +(The proof is by induction on the length of |s|.) +From this we can get $$ \hbox{ +|t=emptyset ==> (forall y::y member attach.X.s <=> y member +attach.t.s || y member X)|.}\eqno(1)$$ +This suggests the following code fragment: +@c +t,s := T,empty; +{invariant T=attach.t.s & ordered.(attach.X.s)} +do t != emptyset -> + /* loop body */@; +od +{t=emptyset & T=attach.t.s & ordered.(attach.X.s)} +/* which, by (1), implies */ +{(forall y::y member attach.X.s <=> y member T | y=x) & ordered.(attach.X.s)} + +@ The question is now what loop body will maintain the invariant. +Since in our earlier loop we made |t| larger and |s| smaller, we can +imagine inverting that loop to get the new loop. +We also invert the proof that the value of |attach.t.s| remains +unchanged. + +@c +{invariant T=attach.t.s & ordered.(attach.X.s)} +do t != emptyset -> + if <<@tfirst guard@>>>@; -> + t,s := t.l, <<left,t.d,t.r>> s + [] <<@tsecond guard@>>>@; -> + t,s := t.r, <<right,t.d,t.l>> s + fi +od +@ The question remains as to what the guards must be to make the whole +thing work. +Taking the first branch, the weakest precondition of +|ordered.(attach.X.s)| is +@c +ordered.(attach.X.(<<left,t.d,t.r>> s)) +!<=> +ordered.(attach.<<X,t.d,t.r>>.s) +!<= /* by a lemma to follow */ +ordered.(attach.X.s) & +ordered.(attach.t.s) & +x <= t.d +!<= +ordered.(attach.X.s) & +ordered.T & +T=attach.t.s & +x <= t.d + +@ So if we strengthen our invariant to include |ordered.T|, we can +make the first guard |x<=t.d|, and the second guard |x>=t.d|, giving +@c +{invariant T=attach.t.s & ordered.(attach.X.s) & ordered.T} +{bound depth.t} +do t != emptyset -> + if x <= t.d -> + t,s := t.l, <<left,t.d,t.r>> s + [] x >= t.d -> + t,s := t.r, <<right,t.d,t.l>> s + fi +od +{t=emptyset & T=attach.t.s & ordered.(attach.X.s)} +/* which, by (1), implies */ +{(forall y::y member attach.X.s <=> y member T | y=x) & ordered.(attach.X.s)} + +@ Now we have to finish the proof we started earlier. +We use a clever trick involving inorder traversals. +For reference, the inorder traversal is defined by +$$\eqalign{ +|in.emptyset|&|==empty|\cr +|in.<<l,d,r>>|&|==in.l d in.r|\cr +}$$ + +Suppose that +$$ (\forall s::( \exists l,r:: (\forall t:: + |in.(attach.t.s)=l in.t r|))) \eqno (2)$$ +(which we will show in just a moment). +Given |s|, choose such an |l| and |r|. Then we have the lemma we need: +@c +ordered.(attach.<<X,t.d,t.r>>.s) +!<=> /* by (2) */ +sorted.(l x t.d in.(t.r) r) +!<= +sorted.(l x r) & +sorted.(l in.(t.l) t.d in.(t.r) r) & +x <= t.d +!<=> +ordered.(attach.X.s) & +ordered.(attach.t.s) & +x <= t.d +@ We prove (2) by induction on the length of |s|. + +If |s=empty|, then |l=empty| and |r=empty| satisfy |in.(attach.t.s)=l +in.t r|. + +If |s!=empty|, then write |s=z Z|. +Our induction hypothesis is |(exists l`,r`:: (forall +t::in.(attach.t.Z)=l` in.t r`))|. +If |z=<<left,data,tree>>|, then let |l=l`| and |r=data in.tree r`|. +Then, for any |t|, +$$\eqalign{ +in.(attach.t.s) &= +|in.(attach.t.(<<left,data,tree>> Z))|\cr +&=|in.(attach.<<t,data,tree>>.Z)|\cr +&=|l` in.t data in.tree r`|\cr +&=|l in.t r|,\cr}$$ +and that's the induction step. + + +@*The finished program. +Here we put the whole program together: +@c +{PRE:ordered.T} +t,s,X := T, empty, <<emptyset,x,emptyset>>; +{invariant T=attach.t.s & ordered.(attach.X.s) & ordered.T} +{bound depth.t} +do t != emptyset -> + if x <= t.d -> + t,s := t.l, <<left,t.d,t.r>> s + [] x >= t.d -> + t,s := t.r, <<right,t.d,t.l>> s + fi +od; +{(forall y::y member attach.X.s <=> y member T | y=x) & ordered.(attach.X.s)} +t := X; +{invariant (forall y::y member attach.t.s <=> y member T | y=x) & + ordered.(attach.t.s)} +{bound #s} +do s != empty -> + let choice, data, tree, S satisfy <<choice,data,tree>> S = s; + if choice = left -> + t,s := <<t,data,tree>>, S + [] choice = right -> + t,s := <<tree,data,t>>, S + fi +od +{POST: (forall y::y member t <=> y member T | y=x) & ordered.t} +@*Index. + + diff --git a/web/spiderweb/src/dijkstra/d.spider b/web/spiderweb/src/dijkstra/d.spider new file mode 100644 index 0000000000..1ee5199b4f --- /dev/null +++ b/web/spiderweb/src/dijkstra/d.spider @@ -0,0 +1,155 @@ +# Copyright 1989 by Norman Ramsey, Odyssey Research Associates +# Not to be sold, but may be used freely for any purpose +# For more information, see file COPYRIGHT in the parent directory +language Dijkstra + +at_sign @ + +comment begin <"#"> end newline + +default translation <*> mathness yes + +token identifier category math mathness yes +token number category math mathness yes +token newline category ignore_scrap mathness maybe translation <> +token pseudo_semi category semi mathness maybe translation <> + +module definition math use math + +token + category unorbinop +token - category unorbinop +token * category binop +token / category binop +token < category binop +token > category binop +token = category binop +token . category binop +token , category binop translation <",\\,"> +token : category binop +token :: category binop translation <"\\CC"> +token ! category unop translation <"\\lnot"> +token & category binop translation <"\\land"> +token || category binop translation <"\\lor"> +token | category unop +token ( category open +token [ category open +token ) category close +token ] category close +token ` category unop translation <"'"> mathness yes +token { translation <"\\{"> category lbrace +token } translation <"\\}"> category close +token ; category semi +token # category unop translation <"\\#"> +token := category binop translation <"\\CE"> +token != name not_eq translation <"\\I"> category binop +token <= name lt_eq translation <"\\L"> category binop +token >= name gt_eq translation <"\\G"> category binop +token == name eq_eq translation <"\\S"> category binop +token <=> translation <"\\IFF"> category binop +token <-> translation <"\\IFF"> category binop +token >> translation <"\\rangle"> category close +token << translation <"\\langle"> category open +token [] category box translation <"[]"> +# two-characer tokens must have a translation!!!! FIX! +token -> category arrow translation <"\\RA"> +token => category binop translation <"\\RA"> +token ==> category binop translation <"\\LRA"> +token --> category arrow translation <"\\RA"> + +# The following tokens are used in writing proofs +token !<=> category shout translation <"\\IFF"> +token !<= category shout translation <"\\FF"> +token !== category shout translation <"\\S"> + +math <indent-force> shout <outdent-force> math --> math + + +macros begin +\def\LRA{\Longrightarrow} +\def\IFF{\Longleftrightarrow} +\def\FF{\Longleftarrow} +\def\DEF{\buildrel\triangle\over=} +\def\CE{\mathrel{{:}{=}}} +\def\CC{\mathrel{{:}{:}}} +\let\RA\rightarrow +\let\openbraces=\{ +\let\closebraces=\} +\def\{{\ifmmode\openbraces\else$\openbraces$\fi} +\def\}{\ifmmode\closebraces\else$\closebraces$\fi} +macros end + + +ilk if_like category if +ilk fi_like category fi + +reserved if ilk if_like +reserved fi ilk fi_like +reserved do ilk if_like +reserved od ilk fi_like + +ilk unop_like category unop translation <*-"\\"-space> +reserved let ilk unop_like +reserved invariant ilk unop_like +reserved bound ilk unop_like + +ilk binop_like category binop translation <"\\"-space-*-"\\"-space> +reserved satisfy ilk binop_like +reserved sat ilk binop_like + + +default mathness yes + +ilk math_like category math +reserved true ilk math_like +reserved false ilk math_like + +ilk member_like category math translation <"\\member"> +reserved member ilk member_like +macros begin +\def\member{\mathbin{\in}} +macros end + +ilk empty_like category math translation <"\\varepsilon"> mathness yes +reserved empty ilk empty_like + +ilk emptyset_like category math translation <"\\emptyset"> mathness yes +reserved emptyset ilk emptyset_like + +ilk cross_like category unop translation <"\\times"> +reserved cross + +ilk forall_like category unop translation <"\\forall"> +reserved forall + +ilk exists_like category unop translation <"\\exists"> +reserved exists + +ilk number_like category unop translation <"\\number"> +reserved number +macros begin +\def\number{{\bf N}} +macros end + + + + +math <"\\"-space> math --> math +math (binop|unorbinop) math --> math +math unop --> math +(unop|unorbinop) math --> math + +math semi <force> --> unop +math <force> lbrace --> lbrace +lbrace math close --> math +# lbrace math close <force> --> unop + +open math close --> math +open close --> math + +? ignore_scrap --> #1 + +if <"\\"-space> math arrow <indent-force> --> ifbegin +ifbegin math <outdent-force> box --> if +ifbegin math <outdent-force> fi --> math + + diff --git a/web/spiderweb/src/dijkstra/make b/web/spiderweb/src/dijkstra/make new file mode 100644 index 0000000000..2ddee7c9f9 --- /dev/null +++ b/web/spiderweb/src/dijkstra/make @@ -0,0 +1,2 @@ +/bin/make -f ../master/WebMakefile CPUTYPE=`cputype` \ + THETANGLE=dtangle THEWEAVE=dweave SPIDER=d.spider $* diff --git a/web/spiderweb/src/dijkstra/sp.web b/web/spiderweb/src/dijkstra/sp.web new file mode 100644 index 0000000000..9725b2ac10 --- /dev/null +++ b/web/spiderweb/src/dijkstra/sp.web @@ -0,0 +1,28 @@ +@*Dijkstra's shortest path. +Obviously the way to prove Dijkstra's algorithm is the way Dijsktra +would do it himself. +Consider +@u +@<Set |d[u]| to all $\infty$ for all |u| in |V| @>@; +d[v] := 0; +W := {v}; +@<For each |u| in |V-W| and $(v,u) \in E$ + let |d[u]| be the weight of $(v,u)$@>@; +{@tinvariant: $\forall u \in W$, + $d[u]$ is the shortest distance from $v$ to $u$@> & + @t$\forall u \in V-W$, $d[u] } +do |W| != |V| --> + @<Let |u| be a vertex in |V-W| with |d[u]| as small as possible@>@; + @<For each |w| in |V-W| and $(u,w) \in E$@>@; + if d[w] <= d[u] + c(u,w) --> skip + [] d [w] >= d[u] + c(u,w) --> d[w] := d[u] + c(u,w) + fi; + W := W @t$\cup$@> {u} +od + +@*Index. + + + + + |