\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{"strcmp"}} using the compiled version.

\addvspace{18pt}

\begin{verbatim};          Proof of the Correctness of the STRCOLL Function
#|
This is part of our effort to verify the Berkeley string library.  The 
Berkeley string library is widely used as part of the Berkeley Unix OS.

This is the source code of strcoll function in the Berkeley string library.

/*
 * Compare strings according to LC_COLLATE category of current locale.
 */
strcoll(s1, s2)
        const char *s1, *s2;
{
        /* LC_COLLATE is unimplemented, hence always "C" */
        return (strcmp(s1, s2));
}

The MC68020 assembly code of the C function strcoll on SUN-3 is given as 
follows.  This binary is generated by "gcc -O".

0x2388 <strcoll>:       linkw fp,#0
0x238c <strcoll+4>:     movel fp@(12),sp@-
0x2390 <strcoll+8>:     movel fp@(8),sp@-
0x2394 <strcoll+12>:    jsr @#0x2358 <strcmp>
0x239a <strcoll+18>:    unlk fp
0x239c <strcoll+20>:    rts

The machine code of the above program is:

<strcoll>:    0x4e56  0x0000  0x2f2e  0x000c  0x2f2e  0x0008  0x4eb9  0x0000
<strcoll+16>: 0x2358  0x4e5e  0x4e75

'(78     86      0       0       47      46      0       12
  47     46      0       8       78      185     0       0
  35     88      78      94      78      117)
|#

; in the logic, the above program is defined by (strcoll-code).
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strcoll-code} \\  
\=\+{\sc{strcoll-code}}\index{strcoll-code} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{78}}{\tt{ }}{\tt{86}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{47}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{185}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{-1}}{\tt{ }}{\tt{78}} \\ 
{\tt{94}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{117}}{\tt{)}}\-\-
\end{tabbing}

\begin{tabbing}{\sc Conservative Axiom}:  strcoll-load \\ \index{strcoll-load}
\=\+{\rm{strcoll-loadp}}\,({\it{s\/}})\index{strcoll-loadp} \\ 
$=$$\;\;\;\;$(\=\+{\rm{evenp}}\,({\sc{strcoll-addr}}\index{strcoll-addr})\index{evenp} \\ 
$\wedge$$\;\;\;\;$({\sc{strcoll-addr}}\index{strcoll-addr} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{nat-rangep}}\,({\sc{strcoll-addr}}\index{strcoll-addr}, {\tt{32}})\index{nat-rangep} \\ 
$\wedge$$\;\;\;\;${\rm{rom-addrp}}\,({\sc{strcoll-addr}}\index{strcoll-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{22}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\sc{strcoll-addr}}\index{strcoll-addr}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{strcoll-code}}\index{strcoll-code})\index{mcode-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{strcmp-loadp}}\,({\it{s\/}})\index{strcmp-loadp} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{pc-read-mem}}\,({\rm{add}}\,({\tt{32}}, {\sc{strcoll-addr}}\index{strcoll-addr}, {\tt{14}})\index{add}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}})\index{pc-read-mem} \\ 
$=$$\;\;\;\;${\sc{strcmp-addr}}\index{strcmp-addr})\-)\-\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbols {\it strcoll-loadp\/} and {\it strcoll-addr\/}.

\begin{tabbing}{\sc Theorem}:  stepn-strcoll-loadp \\ \index{stepn-strcoll-loadp}
{\rm{strcoll-loadp}}\,({\rm{stepn}}\,({\it{s\/}}, {\it{n\/}})\index{stepn})\index{strcoll-loadp} $=$ {\rm{strcoll-loadp}}\,({\it{s\/}})\index{strcoll-loadp}
\end{tabbing}

\begin{verbatim}; the computation time of the program.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strcoll-t} \\  
{\rm{strcoll-t}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcoll-t} $=$ {\rm{splus}}\,({\tt{4}}, {\rm{splus}}\,({\rm{strcmp-t}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp-t}, {\tt{2}})\index{splus})\index{splus}
\end{tabbing}

\begin{verbatim}; the preconditions of the initial state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strcoll-statep} \\  
\=\+{\rm{strcoll-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcoll-statep} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{strcoll-loadp}}\,({\it{s\/}})\index{strcoll-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\sc{strcoll-addr}}\index{strcoll-addr}) \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{24}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{36}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{str1\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n1\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str1\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n1\/}}, {\it{lst1\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{str2\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n2\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str2\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n2\/}}, {\it{lst2\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{24}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{36}}, {\it{str1\/}}, {\it{n1\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{24}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{36}}, {\it{str2\/}}, {\it{n2\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{str1\/}} $=$ {\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{str2\/}} $=$ {\rm{read-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{read-mem}) \\ 
$\wedge$$\;\;\;\;${\rm{stringp}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{stringp} \\ 
$\wedge$$\;\;\;\;$({\it{n1\/}} $\leq$ {\it{n2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{n1\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{n2\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n2\/}}, {\tt{32}})\index{uint-rangep})\-\-
\end{tabbing}

\begin{verbatim}; the intermediate state right before the execution of the subroutine strcmp.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strcoll-s0p} \\  
\=\+{\rm{strcoll-s0p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcoll-s0p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{strcoll-loadp}}\,({\it{s\/}})\index{strcoll-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\sc{strcmp-addr}}\index{strcmp-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr} $=$ {\rm{add}}\,({\tt{32}}, {\sc{strcoll-addr}}\index{strcoll-addr}, {\tt{18}})\index{add}) \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{20}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{36}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{str1\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n1\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str1\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n1\/}}, {\it{lst1\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\it{str2\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n2\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mem-lst}}\,({\tt{1}}, {\it{str2\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n2\/}}, {\it{lst2\/}})\index{mem-lst} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{20}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{36}}, {\it{str1\/}}, {\it{n1\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{sub}}\,({\tt{32}}, {\tt{20}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{36}}, {\it{str2\/}}, {\it{n2\/}})\index{disjoint} \\ 
$\wedge$$\;\;\;\;$({\it{str1\/}} $=$ {\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{str2\/}} $=$ {\rm{read-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{read-mem}) \\ 
$\wedge$$\;\;\;\;${\rm{equal*}}\,({\rm{read-sp}}\,({\it{s\/}})\index{read-sp}, {\rm{sub}}\,({\tt{32}}, {\tt{12}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub})\index{equal*} \\ 
$\wedge$$\;\;\;\;${\rm{stringp}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}})\index{stringp} \\ 
$\wedge$$\;\;\;\;$({\it{n1\/}} $\leq$ {\it{n2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{n1\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{n2\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;${\rm{uint-rangep}}\,({\it{n2\/}}, {\tt{32}})\index{uint-rangep})\-\-
\end{tabbing}

\begin{verbatim}; the intermediate state right after the execution of the subroutine strcmp.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{strcoll-s1p} \\  
\=\+{\rm{strcoll-s1p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcoll-s1p} \\ 
$=$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{s\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;${\rm{strcoll-loadp}}\,({\it{s\/}})\index{strcoll-loadp} \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc} $=$ {\rm{add}}\,({\tt{32}}, {\sc{strcoll-addr}}\index{strcoll-addr}, {\tt{18}})\index{add}) \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{20}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{36}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\it{s\/}})\index{iread-dn} $=$ {\rm{strcmp}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp}))\-\-
\end{tabbing}

\begin{verbatim}; from the initial state s to s0: s --> s0.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcoll-s-s0 \\ \index{strcoll-s-s0}
\=\+{\rm{strcoll-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcoll-statep} \\ 
$\rightarrow$$\;\;\;\;${\rm{strcoll-s0p}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcoll-s0p}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strcoll-s-s0-else \\ \index{strcoll-s-s0-else}
\=\+{\rm{strcoll-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcoll-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{4}})\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{4}})\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}:  strcoll-s-s0-rfile \\ \index{strcoll-s-s0-rfile}
\=\+({\rm{strcoll-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcoll-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\/}}, {\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{tabbing}{\sc Theorem}:  strcoll-s-s0-mem \\ \index{strcoll-s-s0-mem}
\=\+(\=\+{\rm{strcoll-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcoll-statep} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{24}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{36}})\index{disjoint})\- \\ 
$\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{verbatim}; from s0 to s1: s0 --> s1. by strcmp.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcoll-s0p-strcmp-statep \\ \index{strcoll-s0p-strcmp-statep}
\=\+{\rm{strcoll-s0p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcoll-s0p} \\ 
$\rightarrow$$\;\;\;\;${\rm{strcmp-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcmp-statep}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strcoll-s0-s1 \\ \index{strcoll-s0-s1}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strcmp-t}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strcoll-s0p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcoll-s0p} \\ 
$\rightarrow$$\;\;\;\;${\rm{strcoll-s1p}}\,({\it{s1\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcoll-s1p}\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strcoll-s0-s1-else \\ \index{strcoll-s0-s1-else}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strcmp-t}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strcoll-s0p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcoll-s0p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{s1\/}})\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{linked-rts-addr}}\,({\it{s1\/}})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\it{s1\/}})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strcoll-s0-s1-rfile \\ \index{strcoll-s0-s1-rfile}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strcmp-t}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strcoll-s0p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcoll-s0p} \\ 
$\wedge$$\;\;\;\;${\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} \\ 
$\wedge$$\;\;\;\;$({\it{oplen\/}} $\leq$ {\tt{32}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s1\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  strcoll-s0-s1-mem \\ \index{strcoll-s0-s1-mem}
\=\+{\bf let }\=\+{\it{s1\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strcmp-t}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+(\=\+{\rm{strcoll-s0p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcoll-s0p} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{20}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an})\index{sub}, {\tt{36}})\index{disjoint})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{s1\/}})\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})\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{verbatim}; from s1 to exit: s1 --> sn.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcoll-s1-sn \\ \index{strcoll-s1-sn}
\=\+{\rm{strcoll-s1p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcoll-s1p} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{2}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{2}})\index{stepn})\index{mc-pc} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{2}})\index{stepn})\index{iread-dn} $=$ {\rm{strcmp}}\,({\tt{0}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcmp}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{2}})\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{2}})\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})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{2}})\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}:  strcoll-s1-sn-rfile \\ \index{strcoll-s1-sn-rfile}
\=\+({\rm{strcoll-s1p}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcoll-s1p} $\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\/}}, {\tt{2}})\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 strcoll.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  strcoll-correctness \\ \index{strcoll-correctness}
\=\+{\bf let }\=\+{\it{sn\/}}{\bf $\;$ be$\;\;$}{\rm{stepn}}\,({\it{s\/}}, {\rm{strcoll-t}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcoll-t})\index{stepn}\- \\ 
{\bf in} \\ 
\=\+{\rm{strcoll-statep}}\,({\it{s\/}}, {\it{str1\/}}, {\it{n1\/}}, {\it{lst1\/}}, {\it{str2\/}}, {\it{n2\/}}, {\it{lst2\/}})\index{strcoll-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\it{sn\/}})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\it{sn\/}})\index{mc-pc} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\it{sn\/}})\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}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{add}}\,({\tt{32}}, {\rm{read-an}}\,({\tt{32}}, {\tt{7}}, {\it{s\/}})\index{read-an}, {\tt{4}})\index{add})\- \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} $\wedge$ ({\it{oplen\/}} $\leq$ {\tt{32}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{sn\/}})\index{mc-rfile})\index{read-rn} \\ 
$=$$\;\;\;\;${\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\it{s\/}})\index{mc-rfile})\index{read-rn})\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{24}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{36}})\index{disjoint} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\it{sn\/}})\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})\-)\- \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\it{sn\/}})\index{iread-dn} $=$ {\rm{strcoll}}\,({\it{n1\/}}, {\it{lst1\/}}, {\it{lst2\/}})\index{strcoll}))\-\-$\;${\bf  endlet}\-
\end{tabbing}


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

\addvspace{18pt}

\begin{verbatim}; some properties of strcoll.
; the same as strcmp. \end{verbatim}
%\end{list}
\printindex
\end{document}
