\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.

|#

;          Proof of the correctness of the AMAX program
;
\end{verbatim}
\noindent{\sc Event}:   Start with the library {\tt{"mc20-2"}} using the compiled version.

\addvspace{18pt}
\begin{verbatim}#|

This program finds the maximum value of an integer array.  The way I 
wrote this program is to test the ability to handle the while statement.

/* find the maximum in an integer array  */
amax(a, n)
int a[], n;
{ 
  int max;

  max = a[--n];
  while (n > 0)
    if (a[--n] > max)
      max = a[n];
  return (max);
}

Here is the MC68020 assembly code of the above AMAX program.  The code is
generated by "gcc -O".

0x2342 <amax>:          linkw a6,#0
0x2346 <amax+4>:        moveal a6@(8),a0
0x234a <amax+8>:        movel a6@(12),d0
0x234e <amax+12>:       subl #1,d0
0x2350 <amax+14>:       bra 0x235a <amax+24>
0x2352 <amax+16>:       subl #1,d0
0x2354 <amax+18>:       cmpl 0(a0)[d0.l*4],d1
0x2358 <amax+22>:       bge 0x235e <amax+28>
0x235a <amax+24>:       movel 0(a0)[d0.l*4],d1
0x235e <amax+28>:       tstl d0
0x2360 <amax+30>:       bgt 0x2352 <amax+16>
0x2362 <amax+32>:       movel d1,d0
0x2364 <amax+34>:       unlk a6
0x2366 <amax+36>:       rts

The machine code of the above program is:

<amax>:       0x4e56  0x0000  0x206e  0x0008  0x202e  0x000c  0x5380  0x6008
<amax+16>:    0x5380  0xb2b0  0x0c00  0x6c04  0x2230  0x0c00  0x4a80  0x6ef0
<amax+32>:    0x2001  0x4e5e  0x4e75

'(78      86      0       0       32      110     0       8
  32      46      0       12      83      128     96      8
  83      128     178     176     12      0       108     4
  34      48      12      0       74      128     110     240
  32      1       78      94      78      117)
|#

; now we start to prove the correctness of this AMAX program, defined by
; (amax-code).
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{amax-code} \\  
\=\+{\sc{amax-code}}\index{amax-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{32}}{\tt{ }}{\tt{46}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{83}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{96}}{\tt{ }}{\tt{8}}{\tt{ }}{\tt{83}}{\tt{ }}{\tt{128}} \\ 
{\tt{178}}{\tt{ }}{\tt{176}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{108}}{\tt{ }}{\tt{4}}{\tt{ }}{\tt{34}}{\tt{ }}{\tt{48}}{\tt{ }}{\tt{12}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{74}}{\tt{ }}{\tt{128}}{\tt{ }}{\tt{110}}{\tt{ }}{\tt{240}}{\tt{ }}{\tt{32}}{\tt{ }}{\tt{1}}{\tt{ }}{\tt{78}} \\ 
{\tt{94}}{\tt{ }}{\tt{78}}{\tt{ }}{\tt{117}}{\tt{)}}\-\-
\end{tabbing}

\begin{verbatim}; the maximum value in a list.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{amax1} \\  
\=\+{\rm{amax1}}\,({\it{imax\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{imax\/}} \\ 
{\bf elseif }{\rm{ilessp}}\,({\it{imax\/}}, {\rm{get-nth}}\,({\it{n\/}} $-\;1$, {\it{lst\/}})\index{get-nth})\index{ilessp} \\ 
{\bf then }{\rm{amax1}}\,({\rm{get-nth}}\,({\it{n\/}} $-\;1$, {\it{lst\/}})\index{get-nth}, {\it{n\/}} $-\;1$, {\it{lst\/}})\index{amax1} \\ 
{\bf else }{\rm{amax1}}\,({\it{imax\/}}, {\it{n\/}} $-\;1$, {\it{lst\/}})\index{amax1}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{amax}$\;\;$
{\rm{amax}}\,({\it{n\/}}, {\it{lst\/}})\index{amax} $=$ {\rm{amax1}}\,({\rm{get-nth}}\,({\it{n\/}} $-\;1$, {\it{lst\/}})\index{get-nth}, {\it{n\/}} $-\;1$, {\it{lst\/}})\index{amax1}
\end{tabbing}

\begin{verbatim}; the clock of AMAX program.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{amax1-t} \\  
\=\+{\rm{amax1-t}}\,({\it{imax\/}}, {\it{i\/}}, {\it{lst\/}})\index{amax1-t} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{5}} \\ 
{\bf elseif }{\rm{ilessp}}\,({\it{imax\/}}, {\rm{get-nth}}\,({\it{i\/}} $-\;1$, {\it{lst\/}})\index{get-nth})\index{ilessp} \\ 
{\bf then }{\rm{splus}}\,({\tt{6}}, {\rm{amax1-t}}\,({\rm{get-nth}}\,({\it{i\/}} $-\;1$, {\it{lst\/}})\index{get-nth}, {\it{i\/}} $-\;1$, {\it{lst\/}})\index{amax1-t})\index{splus} \\ 
{\bf else }{\rm{splus}}\,({\tt{5}}, {\rm{amax1-t}}\,({\it{imax\/}}, {\it{i\/}} $-\;1$, {\it{lst\/}})\index{amax1-t})\index{splus}$\;${\bf  endif}\-\-
\end{tabbing}
      
\begin{tabbing}{\sc Definition}:\index{amax-t} \\  
{\rm{amax-t}}\,({\it{n\/}}, {\it{lst\/}})\index{amax-t} $=$ {\rm{splus}}\,({\tt{6}}, {\rm{amax1-t}}\,({\rm{get-nth}}\,({\it{n\/}} $-\;1$, {\it{lst\/}})\index{get-nth}, {\it{n\/}} $-\;1$, {\it{lst\/}})\index{amax1-t})\index{splus}
\end{tabbing}

\begin{verbatim}; the induction hint for the loop.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{amax-induct} \\  
\=\+{\rm{amax-induct}}\,({\it{imax\/}}, {\it{n\/}}, {\it{lst\/}}, {\it{s\/}})\index{amax-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{ilessp}}\,({\it{imax\/}}, {\rm{get-nth}}\,({\it{n\/}} $-\;1$, {\it{lst\/}})\index{get-nth})\index{ilessp} \\ 
{\bf then }{\rm{amax-induct}}\,({\rm{get-nth}}\,({\it{n\/}} $-\;1$, {\it{lst\/}})\index{get-nth}, {\it{n\/}} $-\;1$, {\it{lst\/}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{amax-induct} \\ 
{\bf else }{\rm{amax-induct}}\,({\it{imax\/}}, {\it{n\/}} $-\;1$, {\it{lst\/}}, {\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn})\index{amax-induct}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; the preconditions of the initial state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{amax-statep} \\  
\=\+{\rm{amax-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax-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{38}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{amax-code}}\index{amax-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-ilst}}\,({\tt{4}}, {\it{a\/}}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-ilst} \\ 
$\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$$\;\;\;\;$({\tt{0}} $<$ {\it{n\/}}))\-\-
\end{tabbing}

\begin{verbatim}; the conditions of the intermediate state.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{amax1-statep} \\  
\=\+{\rm{amax1-statep}}\,({\it{s\/}}, {\it{imax\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax1-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{sub}}\,({\tt{32}}, {\tt{28}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{38}})\index{rom-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{mcode-addrp}}\,({\rm{sub}}\,({\tt{32}}, {\tt{28}}, {\rm{mc-pc}}\,({\it{s\/}})\index{mc-pc})\index{sub}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\sc{amax-code}}\index{amax-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-ilst}}\,({\tt{4}}, {\rm{read-an}}\,({\tt{32}}, {\tt{0}}, {\it{s\/}})\index{read-an}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\it{n\/}}, {\it{lst\/}})\index{mem-ilst} \\ 
$\wedge$$\;\;\;\;${\rm{ram-addrp}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{0}}, {\it{s\/}})\index{read-an}, {\rm{mc-mem}}\,({\it{s\/}})\index{mc-mem}, {\tt{4}} $*$ {\it{n\/}})\index{ram-addrp} \\ 
$\wedge$$\;\;\;\;${\rm{disjoint}}\,({\rm{read-an}}\,({\tt{32}}, {\tt{0}}, {\it{s\/}})\index{read-an}, {\tt{4}} $*$ {\it{n\/}}, {\rm{read-an}}\,({\tt{32}}, {\tt{6}}, {\it{s\/}})\index{read-an}, {\tt{16}})\index{disjoint} \\ 
$\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{imax\/}} $=$ {\rm{nat-to-int}}\,({\rm{read-dn}}\,({\tt{32}}, {\tt{1}}, {\it{s\/}})\index{read-dn}, {\tt{32}})\index{nat-to-int}) \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{n\/}}))\-\-
\end{tabbing}


\noindent{\sc Event}:   Enable iplus.

\addvspace{18pt}

\noindent{\sc Event}:   Disable ilessp.

\addvspace{18pt}

\begin{verbatim}; the initial segment of the program.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  amax-$>$amax1-statep \\ \index{amax-$>$amax1-statep}
\=\+{\rm{amax-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax-statep} \\ 
$\rightarrow$$\;\;\;\;${\rm{amax1-statep}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn}, {\rm{get-nth}}\,({\it{n\/}} $-\;1$, {\it{lst\/}})\index{get-nth}, {\it{n\/}} $-\;1$, {\it{n\/}}, {\it{lst\/}})\index{amax1-statep}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  amax-initial \\ \index{amax-initial}
\=\+{\rm{amax-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-a6}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\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{6}})\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}:  amax-initial-rfile \\ \index{amax-initial-rfile}
\=\+({\rm{amax-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax-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{6}})\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}:  amax-initial-mem \\ \index{amax-initial-mem}
\=\+({\rm{amax-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax-statep} $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{16}})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\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}; base case.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  amax-base-case \\ \index{amax-base-case}
\=\+({\rm{amax1-statep}}\,({\it{s\/}}, {\it{imax\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax1-statep} $\wedge$ ({\it{i\/}} $\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\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{5}})\index{stepn})\index{iread-dn} $=$ {\it{imax\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\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{5}})\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{5}})\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}:  amax-base-rfile \\ \index{amax-base-rfile}
\=\+({\rm{amax1-statep}}\,({\it{s\/}}, {\it{imax\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax1-statep} $\wedge$ {\rm{d2-7a2-5p}}\,({\it{rn\/}})\index{d2-7a2-5p} $\wedge$ ({\it{i\/}} $\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\it{rn\/}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\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.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  amax-induct-case1 \\ \index{amax-induct-case1}
\=\+(\=\+{\rm{amax1-statep}}\,({\it{s\/}}, {\it{imax\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax1-statep} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\it{imax\/}}, {\rm{get-nth}}\,({\it{i\/}} $-\;1$, {\it{lst\/}})\index{get-nth})\index{ilessp})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{amax1-statep}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn}, {\rm{get-nth}}\,({\it{i\/}} $-\;1$, {\it{lst\/}})\index{get-nth}, {\it{i\/}} $-\;1$, {\it{n\/}}, {\it{lst\/}})\index{amax1-statep} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\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{6}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{6}})\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}:  amax-induct-case2 \\ \index{amax-induct-case2}
\=\+(\=\+{\rm{amax1-statep}}\,({\it{s\/}}, {\it{imax\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax1-statep} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\it{imax\/}}, {\rm{get-nth}}\,({\it{i\/}} $-\;1$, {\it{lst\/}})\index{get-nth})\index{ilessp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{amax1-statep}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn}, {\it{imax\/}}, {\it{i\/}} $-\;1$, {\it{n\/}}, {\it{lst\/}})\index{amax1-statep} \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\it{oplen\/}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\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{5}})\index{stepn})\index{linked-a6} $=$ {\rm{linked-a6}}\,({\it{s\/}})\index{linked-a6}) \\ 
$\wedge$$\;\;\;\;$({\rm{linked-rts-addr}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\index{stepn})\index{linked-rts-addr} $=$ {\rm{linked-rts-addr}}\,({\it{s\/}})\index{linked-rts-addr}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\tt{5}})\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}:  amax-induct-rfile1 \\ \index{amax-induct-rfile1}
\=\+(\=\+{\rm{amax1-statep}}\,({\it{s\/}}, {\it{imax\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax1-statep} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\it{imax\/}}, {\rm{get-nth}}\,({\it{i\/}} $-\;1$, {\it{lst\/}})\index{get-nth})\index{ilessp} \\ 
$\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{6}})\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}:  amax-induct-rfile2 \\ \index{amax-induct-rfile2}
\=\+(\=\+{\rm{amax1-statep}}\,({\it{s\/}}, {\it{imax\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax1-statep} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\it{imax\/}}, {\rm{get-nth}}\,({\it{i\/}} $-\;1$, {\it{lst\/}})\index{get-nth})\index{ilessp}) \\ 
$\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{5}})\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 amax-statep.

\addvspace{18pt}

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

\addvspace{18pt}

\begin{verbatim}; the correctness of the loop.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  amax1-correctness \\ \index{amax1-correctness}
\=\+{\rm{amax1-statep}}\,({\it{s\/}}, {\it{imax\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax1-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{amax1-t}}\,({\it{imax\/}}, {\it{i\/}}, {\it{lst\/}})\index{amax1-t})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{amax1-t}}\,({\it{imax\/}}, {\it{i\/}}, {\it{lst\/}})\index{amax1-t})\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\/}}, {\rm{amax1-t}}\,({\it{imax\/}}, {\it{i\/}}, {\it{lst\/}})\index{amax1-t})\index{stepn})\index{iread-dn} \\ 
$=$$\;\;\;\;${\rm{amax1}}\,({\it{imax\/}}, {\it{i\/}}, {\it{lst\/}})\index{amax1})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{amax1-t}}\,({\it{imax\/}}, {\it{i\/}}, {\it{lst\/}})\index{amax1-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{amax1-t}}\,({\it{imax\/}}, {\it{i\/}}, {\it{lst\/}})\index{amax1-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})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{amax1-t}}\,({\it{imax\/}}, {\it{i\/}}, {\it{lst\/}})\index{amax1-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}:  amax1-rfile-correctness \\ \index{amax1-rfile-correctness}
\=\+({\rm{amax1-statep}}\,({\it{s\/}}, {\it{imax\/}}, {\it{i\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax1-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{amax1-t}}\,({\it{imax\/}}, {\it{i\/}}, {\it{lst\/}})\index{amax1-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 AMAX program.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  amax-correctness \\ \index{amax-correctness}
\=\+{\rm{amax-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax-statep} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{mc-status}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{amax-t}}\,({\it{n\/}}, {\it{lst\/}})\index{amax-t})\index{stepn})\index{mc-status} $=$ {\tt{'}}{\tt{running}}) \\ 
$\wedge$$\;\;\;\;$({\rm{mc-pc}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{amax-t}}\,({\it{n\/}}, {\it{lst\/}})\index{amax-t})\index{stepn})\index{mc-pc} $=$ {\rm{rts-addr}}\,({\it{s\/}})\index{rts-addr}) \\ 
$\wedge$$\;\;\;\;$({\rm{iread-dn}}\,({\tt{32}}, {\tt{0}}, {\rm{stepn}}\,({\it{s\/}}, {\rm{amax-t}}\,({\it{n\/}}, {\it{lst\/}})\index{amax-t})\index{stepn})\index{iread-dn} $=$ {\rm{amax}}\,({\it{n\/}}, {\it{lst\/}})\index{amax}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{read-rn}}\,({\tt{32}}, {\tt{14}}, {\rm{mc-rfile}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{amax-t}}\,({\it{n\/}}, {\it{lst\/}})\index{amax-t})\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\/}}, {\rm{amax-t}}\,({\it{n\/}}, {\it{lst\/}})\index{amax-t})\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}:  amax-rfile-correctness \\ \index{amax-rfile-correctness}
\=\+({\rm{amax-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax-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{amax-t}}\,({\it{n\/}}, {\it{lst\/}})\index{amax-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{tabbing}{\sc Theorem}:  amax-mem-correctness \\ \index{amax-mem-correctness}
\=\+({\rm{amax-statep}}\,({\it{s\/}}, {\it{a\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax-statep} $\wedge$ {\rm{disjoint}}\,({\it{x\/}}, {\it{k\/}}, {\rm{sub}}\,({\tt{32}}, {\tt{4}}, {\rm{read-sp}}\,({\it{s\/}})\index{read-sp})\index{sub}, {\tt{16}})\index{disjoint}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{read-mem}}\,({\it{x\/}}, {\rm{mc-mem}}\,({\rm{stepn}}\,({\it{s\/}}, {\rm{amax-t}}\,({\it{n\/}}, {\it{lst\/}})\index{amax-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}


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

\addvspace{18pt}

\begin{verbatim}; amax does find the maximum of an integer list.  We need to prove two 
; things:  
;      1. the output is no less than any element of the list.  
;      2. the output is in the list.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  ilessp-transitivity \\ \index{ilessp-transitivity}
({\rm{ilessp}}\,({\it{x\/}}, {\it{y\/}})\index{ilessp} $\wedge$ {\rm{ileq}}\,({\it{y\/}}, {\it{z\/}})\index{ileq}) $\rightarrow$ {\rm{ilessp}}\,({\it{x\/}}, {\it{z\/}})\index{ilessp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  amax1-mono \\ \index{amax1-mono}
($\neg$ {\rm{ilessp}}\,({\it{imax\/}}, {\it{imax1\/}})\index{ilessp}) $\rightarrow$ ($\neg$ {\rm{ilessp}}\,({\rm{amax1}}\,({\it{imax\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax1}, {\it{imax1\/}})\index{ilessp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  amax1-max \\ \index{amax1-max}
({\it{i\/}} $<$ {\it{n\/}}) $\rightarrow$ ($\neg$ {\rm{ilessp}}\,({\rm{amax1}}\,({\it{imax\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax1}, {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  amax-max \\ \index{amax-max}
({\it{i\/}} $<$ {\it{n\/}}) $\rightarrow$ ($\neg$ {\rm{ilessp}}\,({\rm{amax}}\,({\it{n\/}}, {\it{lst\/}})\index{amax}, {\rm{get-nth}}\,({\it{i\/}}, {\it{lst\/}})\index{get-nth})\index{ilessp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  get-nth-memberp \\ \index{get-nth-memberp}
({\it{n\/}} $<$ {\rm{len}}\,({\it{lst\/}})\index{len}) $\rightarrow$ ({\rm{get-nth}}\,({\it{n\/}}, {\it{lst\/}})\index{get-nth} $\in$ {\it{lst\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  amax1-closed \\ \index{amax1-closed}
(({\it{n\/}} $\leq$ {\rm{len}}\,({\it{lst\/}})\index{len}) $\wedge$ ({\it{imax\/}} $\in$ {\it{lst\/}})) $\rightarrow$ ({\rm{amax1}}\,({\it{imax\/}}, {\it{n\/}}, {\it{lst\/}})\index{amax1} $\in$ {\it{lst\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  amax-closed \\ \index{amax-closed}
(({\it{n\/}} $\leq$ {\rm{len}}\,({\it{lst\/}})\index{len}) $\wedge$ ({\it{n\/}} $\not\simeq {\tt{0}}$)) $\rightarrow$ ({\rm{amax}}\,({\it{n\/}}, {\it{lst\/}})\index{amax} $\in$ {\it{lst\/}})
\end{tabbing}

%\end{list}
\printindex
\end{document}
