summaryrefslogtreecommitdiff
path: root/web/spiderweb/src/dijkstra
diff options
context:
space:
mode:
authorNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
committerNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
commite0c6872cf40896c7be36b11dcc744620f10adf1d (patch)
tree60335e10d2f4354b0674ec22d7b53f0f8abee672 /web/spiderweb/src/dijkstra
Initial commit
Diffstat (limited to 'web/spiderweb/src/dijkstra')
-rw-r--r--web/spiderweb/src/dijkstra/README3
-rw-r--r--web/spiderweb/src/dijkstra/binary.web267
-rw-r--r--web/spiderweb/src/dijkstra/d.spider155
-rw-r--r--web/spiderweb/src/dijkstra/make2
-rw-r--r--web/spiderweb/src/dijkstra/sp.web28
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.
+
+
+
+
+