Skip to main content \(\newcommand{\identity}{\mathrm{id}} \newcommand{\notdivide}{{\not{\mid}}}
\newcommand{\notsubset}{\not\subset} \newcommand{\lcm}{\operatorname{lcm}}
\newcommand{\gf}{\operatorname{GF}} \newcommand{\inn}{\operatorname{Inn}}
\newcommand{\aut}{\operatorname{Aut}} \newcommand{\Hom}{\operatorname{Hom}}
\newcommand{\cis}{\operatorname{cis}} \newcommand{\chr}{\operatorname{char}}
\newcommand{\Null}{\operatorname{Null}} \renewcommand{\vec}[1]{\mathbf{#1}}
\newcommand{\N}{{\mathbb N}} \newcommand{\Z}{{\mathbb Z}} \newcommand{\Q}{{\mathbb Q}}
\newcommand{\R}{{\mathbb R}} \newcommand{\Zpos}{{{\mathbb Z}^+}} \newcommand{\SUB}{\subseteq}
\newcommand{\SUP}{\supseteq} \newcommand{\PSUB}{\varsubsetneq}
\newcommand{\PSUP}{\varsupsetneq} \newcommand{\SETDIFF}{\smallsetminus}
\newcommand{\st}{\,|\,}
\newcommand{\ab}{\mbox{$\{a,b\}$}} \newcommand{\aetc}[2]{\mbox{{${#1}_1{#1}_2\ldots
{#1}_{#2}$}}} \newcommand{\varep}{\varepsilon}
\newcommand{\fsafig}[1]{\medskip\centerline{\eps{fsa#1}}\medskip}
\newcommand{\REOR}{\hbox{$\,|\,$}} \newcommand{\POW}{{\mathscr P}}
\newcommand{\EMPTYSTRING}{\varepsilon}
\newcommand{\PRODUCES}{\longrightarrow}
\newcommand{\YIELDS}{\Longrightarrow}
\newcommand{\YIELDSTAR}{{\Longrightarrow}^*}
\newcommand{\NT}[1]{\hbox{$\langle$\textit{#1}$\rangle$}}
\newcommand{\BNFPRODUCES}{\hbox{\texttt{::=}}}
\newcommand{\BNFALT}{\hbox{$|$}}
\newcommand{\lt}{<}
\newcommand{\gt}{>}
\newcommand{\amp}{&}
\definecolor{fillinmathshade}{gray}{0.9}
\newcommand{\fillinmath}[1]{\mathchoice{\colorbox{fillinmathshade}{$\displaystyle \phantom{\,#1\,}$}}{\colorbox{fillinmathshade}{$\textstyle \phantom{\,#1\,}$}}{\colorbox{fillinmathshade}{$\scriptstyle \phantom{\,#1\,}$}}{\colorbox{fillinmathshade}{$\scriptscriptstyle\phantom{\,#1\,}$}}}
\)
Chapter 14 Program Correctness
The goal of this chapter is to introduce the process of verifying the correctness of computer algorithms and programs. Often this involves using induction, so the first section will review writing inductive proofs. The following sections will cover the basics of proving correctness.
