\documentstyle[makeidx]{article}
\makeindex
%\setlength{\oddsidemargin}{.5in}
%\setlength{\evensidemargin}{.5in}
%\setlength{\textwidth}{5.8in}
\begin{document}
%\setlength{\parindent}{0pt}
%\newcounter{bean}
%\begin{list}{\arabic{bean}.}{\usecounter{bean}\setlength{\leftmargin}{0pt}\setlength{\rightmargin}{0pt}\setlength{\listparindent}{20pt}\setlength{\parsep}{5pt}}
%\item[]

\begin{verbatim}#|

 Copyright (C) 1994 by Yuan Yu.  All Rights Reserved.

 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.

 NO WARRANTY

 Yuan Yu PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS PROVIDED "AS IS"
 WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING, BUT NOT
 LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
 PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
 SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU ASSUME THE COST OF
 ALL NECESSARY SERVICING, REPAIR OR CORRECTION.

 IN NO EVENT WILL Yuan Yu BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST PROFITS,
 LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT
 OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT LIMITED TO LOSS
 OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY THIRD
 PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH DAMAGES, OR
 FOR ANY CLAIM BY ANY OTHER PARTY.

|#

\end{verbatim}
\noindent{\sc Event}:   Start with the library {\tt{"mc20-2"}} using the compiled version.

\addvspace{18pt}
\begin{verbatim};            Proof of the Correctness of a ZERO Program
#|

This program zeros an integer array.

/* zeros an array */
zero(a, n)
int a[], n;
{ 
  int i;
  for (i = 0; i < n; ++i)
    a[i] = 0;
}

Here, in symbolic form, is the above program in MC68k instructions. The 
machine code is produced by "gcc -O".

a6@8,  the first argument which is the starting address of the array A.
a6@12, the second argument which is the number of the elements we are zeroing. 
a6@-4, the local variable i which serves as a counter.

0x2328 <zero>:	        linkw a6,#0
0x232c <zero+4>:	moveal a6@(8),a0
0x2330 <zero+8>:	movel a6@(12),d1
0x2334 <zero+12>:	clrl d0
0x2336 <zero+14>:	cmpl d0,d1
0x2338 <zero+16>:	ble 0x2344 <zero+28>
0x233a <zero+18>:	clrl 0(a0)[d0.l*4]
0x233e <zero+22>:	addql #1,d0
0x2340 <zero+24>:	cmpl d0,d1
0x2342 <zero+26>:	bgt 0x233a <zero+18>
0x2344 <zero+28>:	unlk a6
0x2346 <zero+30>:	rts

The machine code of the above program is:

<zero>:      0x4e56  0x0000  0x206e  0x0008  0x222e  0x000c  0x4280  0xb280
<zero+16>:   0x6f0a  0x42b0  0x0c00  0x5280  0xb280  0x6ef6  0x4e5e  0x4e75

'(78      86      0       0       32      110     0       8
  34      46      0       12      66      128     178     128
  111     10      66      176     12      0       82      128
  178     128     110     246     78      94      78      117)
|#

; machine code for ZERO.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{zero-code} \\  
\=\+{\sc{zero-code}}\index{zero-code} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{78}}{\tt{ }}{\tt{86}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{110}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{34}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{178}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{111}} \\ 
{\tt{10}}{\tt{ }}{\tt{66}}{\tt{ }}{\tt{176}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{82}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{178}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{110}}{\tt{ }}{\tt{246}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{94}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{117}}{\tt{)}}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{clr-lst} \\  
\=\+{\rm{clr-lst}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{clr-lst} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n\/}}$\;\;${\bf then }{\rm{clr-lst}}\,($1\;+$ {\it{i\/}}, {\it{n\/}}, {\rm{put-nth}}\,({\tt{0}}, {\it{i\/}}, {\it{lst\/}})\index{put-nth})\index{clr-lst} \\ 
{\bf else }{\it{lst\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{zero1-t} \\  
\=\+{\rm{zero1-t}}\,({\it{i\/}}, {\it{n\/}})\index{zero1-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n\/}}$\;\;${\bf then }{\rm{splus}}\,({\tt{4}}, {\rm{zero1-t}}\,($1\;+$ {\it{i\/}}, {\it{n\/}})\index{zero1-t})\index{splus} \\ 
{\bf else }{\tt{4}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{zero-t} \\  
\=\+{\rm{zero-t}}\,({\it{n\/}})\index{zero-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{8}} \\ 
{\bf else }{\rm{splus}}\,({\tt{8}}, {\rm{zero1-t}}\,({\tt{1}}, {\it{n\/}})\index{zero1-t})\index{splus}$\;${\bf  endif}\-\-
\end{tabbing}
  
\begin{tabbing}{\sc Definition}:\index{zero-induct} \\  
\=\+{\rm{zero-induct}}\,({\it{s\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n\/}}$\;\;${\bf then }{\rm{zero-induct}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn}, $1\;+$ {\it{i\/}}, {\it{n\/}}, {\rm{put-nth}}\,({\tt{0}}, {\it{i\/}}, {\it{lst\/}})\index{put-nth})\index{zero-induct} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{zero-statep} \\  
\=\+{\rm{zero-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-statep} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{32}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{zero-code}}\index{zero-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{16}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{a\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}} $*$ {\it{n\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{16}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{read-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{4}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{read-mem}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ {\rm{iread-mem}}\,({\rm{add}}\,({\tt{32}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\tt{8}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{iread-mem}) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\tt{4}} $*$ {\it{n\/}}, {\tt{32}})\index{uint-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\in\;${\bf{N}}${}$))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{zero-s0p} \\  
\=\+{\rm{zero-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-s0p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{evenp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{evenp} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{24}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{32}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{24}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{zero-code}}\index{zero-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{16}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{a\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}} $*$ {\it{n\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{16}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{0}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-dn}}\,({\tt{32}}, {\tt{0}}, {\it{s\/}})\index{read-dn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-dn}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{read-dn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\tt{4}} $*$ {\it{n\/}}, {\tt{32}})\index{uint-rangep} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\leq$ {\it{n\/}}))\-\-
\end{tabbing}

\begin{verbatim}; from s to exit: s --> sn.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  zero-s-sn \\ \index{zero-s-sn}
\=\+({\rm{zero-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-statep} $\wedge$ ({\it{n\/}} $\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-pc} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn}, {\tt{4}})\index{add})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-s-sn-rfile \\ \index{zero-s-sn-rfile}
\=\+({\rm{zero-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-statep} $\wedge$ {\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} $\wedge$ ({\it{n\/}} $\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-s-sn-mem \\ \index{zero-s-sn-mem}
\=\+(\=\+{\rm{zero-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-statep} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{16}}, {\it{x\/}}, {\it{k\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\simeq {\tt{0}}$))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{verbatim}; from s to s0: s --> s0.		      
\end{verbatim}\begin{tabbing}{\sc Theorem}:  zero-s-s0 \\ \index{zero-s-s0}
\=\+({\rm{zero-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-statep} $\wedge$ ({\it{n\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;${\rm{zero-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn}, {\it{a\/}}, {\tt{1}}, {\it{n\/}}, {\rm{put-nth}}\,({\tt{0}}, {\tt{0}}, {\it{lst\/}})\index{put-nth})\index{zero-s0p}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-s-s0-other \\ \index{zero-s-s0-other}
\=\+({\rm{zero-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-statep} $\wedge$ ({\it{n\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{linked-a6} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub})\-)\-\-
\end{tabbing} 

\begin{tabbing}{\sc Theorem}:  zero-s-s0-rfile \\ \index{zero-s-s0-rfile}
\=\+({\rm{zero-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-statep} $\wedge$ {\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} $\wedge$ ({\it{n\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-s-s0-mem \\ \index{zero-s-s0-mem}
\=\+(\=\+{\rm{zero-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-statep} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{16}}, {\it{x\/}}, {\it{k\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\it{x\/}}, {\it{k\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not\simeq {\tt{0}}$))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{8}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{verbatim}; from s0 to exit:  s0 --> sn. By induction.
; base case: s0 --> sn, if i >= n.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  zero-s0-sn-base \\ \index{zero-s0-sn-base}
\=\+({\rm{zero-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-s0p} $\wedge$ ({\it{i\/}} $\not<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{mc-rfile})\index{read-rn} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{8}})\index{add})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-s0-sn-mem-base \\ \index{zero-s0-sn-mem-base}
\=\+({\rm{zero-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-s0p} $\wedge$ ({\it{i\/}} $\not<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-s0-sn-rfile-base \\ \index{zero-s0-sn-rfile-base}
\=\+({\rm{zero-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-s0p} $\wedge$ {\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} $\wedge$ ({\it{i\/}} $\not<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{verbatim}; induction case: s0 --> s0, if i < n.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  zero-s0-s0 \\ \index{zero-s0-s0}
\=\+({\rm{zero-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-s0p} $\wedge$ ({\it{i\/}} $<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{zero-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn}, {\it{a\/}}, $1\;+$ {\it{i\/}}, {\it{n\/}}, {\rm{put-nth}}\,({\tt{0}}, {\it{i\/}}, {\it{lst\/}})\index{put-nth})\index{zero-s0p} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\- \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-s0-s0-mem \\ \index{zero-s0-s0-mem}
\=\+({\rm{zero-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-s0p} $\wedge$ {\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\it{x\/}}, {\it{k\/}})\index{disjoint} $\wedge$ ({\it{i\/}} $<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-s0-s0-rfile \\ \index{zero-s0-s0-rfile}
\=\+({\rm{zero-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-s0p} $\wedge$ {\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} $\wedge$ ({\it{i\/}} $<$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable zero-statep.

\addvspace{18pt}

\noindent{\sc Event}:   Disable zero-s0p.

\addvspace{18pt}

\begin{verbatim}; put together: s0 --> sn.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  zero-s0-sn \\ \index{zero-s0-sn}
\=\+{\rm{zero-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-s0p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{zero1-t}}\,({\it{i\/}}, {\it{n\/}})\index{zero1-t})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{zero1-t}}\,({\it{i\/}}, {\it{n\/}})\index{zero1-t})\index{stepn})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{zero1-t}}\,({\it{i\/}}, {\it{n\/}})\index{zero1-t})\index{stepn})\index{mc-mem}, {\it{n\/}}, {\rm{clr-lst}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{clr-lst})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{zero1-t}}\,({\it{i\/}}, {\it{n\/}})\index{zero1-t})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{15}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{zero1-t}}\,({\it{i\/}}, {\it{n\/}})\index{zero1-t})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{8}})\index{add})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-s0-sn-mem \\ \index{zero-s0-sn-mem}
\=\+(\=\+{\rm{zero-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-s0p} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{16}}, {\it{x\/}}, {\it{k\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\it{x\/}}, {\it{k\/}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{zero1-t}}\,({\it{i\/}}, {\it{n\/}})\index{zero1-t})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} \\ 
$=$$\;\;\;\;${\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-s0-sn-rfile \\ \index{zero-s0-sn-rfile}
\=\+({\rm{zero-s0p}}\,({\it{s\/}}, {\it{a\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-s0p} $\wedge$ {\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{zero1-t}}\,({\it{i\/}}, {\it{n\/}})\index{zero1-t})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}

\begin{verbatim}; the correctness of the program ZERO.			       
\end{verbatim}\begin{tabbing}{\sc Theorem}:  zero-correctness \\ \index{zero-correctness}
\=\+{\rm{zero-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{zero-t}}\,({\it{n\/}})\index{zero-t})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{zero-t}}\,({\it{n\/}})\index{zero-t})\index{stepn})\index{mc-pc} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{zero-t}}\,({\it{n\/}})\index{zero-t})\index{stepn})\index{mc-mem}, {\it{n\/}}, {\rm{clr-lst}}\,({\tt{0}}, {\it{n\/}}, {\it{lst\/}})\index{clr-lst})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;$({\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\rm{stepn}}\,({\it{s\/}}, {\rm{zero-t}}\,({\it{n\/}})\index{zero-t})\index{stepn})\index{read-an} $=$ {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-an}}\,({\tt{32}}, {\tt{7}}, {\rm{stepn}}\,({\it{s\/}}, {\rm{zero-t}}\,({\it{n\/}})\index{zero-t})\index{stepn})\index{read-an} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{7}}, {\it{s\/}})\index{read-an}, {\tt{4}})\index{add})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-mem \\ \index{zero-mem}
\=\+(\=\+{\rm{zero-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-statep} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{16}}, {\it{x\/}}, {\it{k\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{a\/}}, {\tt{4}} $*$ {\it{n\/}}, {\it{x\/}}, {\it{k\/}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{zero-t}}\,({\it{n\/}})\index{zero-t})\index{stepn})\index{mc-mem}, {\it{k\/}})\index{read-mem} $=$ {\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{k\/}})\index{read-mem})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-rfile \\ \index{zero-rfile}
\=\+({\rm{zero-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{zero-statep} $\wedge$ {\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{zero-t}}\,({\it{n\/}})\index{zero-t})\index{stepn})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable zero-t.

\addvspace{18pt}

\begin{verbatim}; we next need to prove that clr-lst does clear the list.       
\end{verbatim}\begin{tabbing}{\sc Theorem}:  zero-lst-la1 \\ \index{zero-lst-la1}
({\it{j\/}} $<$ {\it{i\/}}) $\rightarrow$ ({\rm{get-nth}}\,({\it{j\/}}, {\rm{clr-lst}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{clr-lst})\index{get-nth} $=$ {\rm{get-nth}}\,({\it{j\/}}, {\it{lst\/}})\index{get-nth})
\end{tabbing}     

\begin{tabbing}{\sc Theorem}:  zero-lst-la2 \\ \index{zero-lst-la2}
\=\+{\rm{get-nth}}\,({\it{i\/}}, {\rm{clr-lst}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{clr-lst})\index{get-nth} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{n\/}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth}$\;${\bf  endif}\-\-
\end{tabbing}     

\begin{verbatim}; clr-lst does clear the list.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  clr-lst-clear \\ \index{clr-lst-clear}
(({\it{i\/}} $\leq$ {\it{j\/}}) $\wedge$ ({\it{j\/}} $<$ {\it{n\/}})) $\rightarrow$ ({\rm{get-nth}}\,({\it{j\/}}, {\rm{clr-lst}}\,({\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{clr-lst})\index{get-nth} $=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  clr-lst-clear-0 \\ \index{clr-lst-clear-0}
({\it{j\/}} $<$ {\it{n\/}}) $\rightarrow$ ({\rm{get-nth}}\,({\it{j\/}}, {\rm{clr-lst}}\,({\tt{0}}, {\it{n\/}}, {\it{lst\/}})\index{clr-lst})\index{get-nth} $=$ {\tt{0}})
\end{tabbing}
%\end{list}
\printindex
\end{document}
