equal
deleted
inserted
replaced
889 "tcopy_begin"}, @{term "tcopy_loop"} and @{term "tcopy_end"} in |
889 "tcopy_begin"}, @{term "tcopy_loop"} and @{term "tcopy_end"} in |
890 isolation. We will show the details for the program @{term |
890 isolation. We will show the details for the program @{term |
891 "tcopy_begin"}. Given the invariants @{term "inv_begin0"},\ldots, |
891 "tcopy_begin"}. Given the invariants @{term "inv_begin0"},\ldots, |
892 @{term "inv_begin4"} shown in Figure~\ref{invbegin} corresponding to |
892 @{term "inv_begin4"} shown in Figure~\ref{invbegin} corresponding to |
893 each state of @{term tcopy_begin}, we define the |
893 each state of @{term tcopy_begin}, we define the |
894 following invariant for the whole program: |
894 following invariant for the whole @{term tcopy_begin} program: |
895 |
895 |
896 \begin{figure} |
896 \begin{figure} |
897 \begin{center} |
897 \begin{center} |
898 \begin{tabular}{@ {}lcl@ {\hspace{-2cm}}l@ {}} |
898 \begin{tabular}{@ {}lcl@ {\hspace{-2cm}}l@ {}} |
899 @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\ |
899 @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\ |