Program Correctness: Example
Forfatter
Hans-Dieter Hiep
Sidst opdateret
5 år siden
Licens
Creative Commons CC BY 4.0
Resumé
An example that shows how to write proof outlines in LaTeX.
An example that shows how to write proof outlines in LaTeX.
\documentclass[english,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{mathtools}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{babel}
% This template contains some LaTeX commands for writing proof outlines.
% See the example question and answer below.
% Spacing
\newcommand\tab[1][1em]{\hspace*{#1}}
% Program elements
\newcommand\ASSIGN[0]{\ensuremath{\coloneqq}}
\newcommand\WHILE[0]{\ensuremath{\mathbf{while}\ }}
\newcommand\DO[0]{\ensuremath{\ \mathbf{do}}}
\newcommand\IF[0]{\ensuremath{\mathbf{if}\ }}
\newcommand\THEN[0]{\ensuremath{\ \mathbf{then}}}
\newcommand\ELSE[0]{\ensuremath{\mathbf{else}}}
\newcommand\SKIP[0]{\ensuremath{\mathbf{skip}}}
\newcommand\FI[0]{\ensuremath{\mathbf{fi}}}
\newcommand\OD[0]{\ensuremath{\mathbf{od}}}
% Correctness formula
\newcommand\CORRECT[3]{\ensuremath{\{#1\}\mathrel{#2}\{#3\}}}
\newcommand\ASSERT[1]{\ensuremath{\{#1\}}}
\newcommand\INVARIANT[1]{\ensuremath{\{\mathbf{inv}:#1\}}}
\newcommand\BOUND[1]{\ensuremath{\{\mathbf{bd}:#1\}}}
% Short conditional expression
\newcommand\ite[3]{\ensuremath{#1\mathop{?}#2:#3}}
\newcommand\itep[3]{\ensuremath{(#1\mathop{?}#2:#3)}}
\begin{document}
\section{Program Correctness: Template}
Given an array $b$ of type $\mathbf{integer}\to\mathbf{boolean}$
and a non-negative length $n$. The following program computes the
numerical representation of a bitvector.
\begin{quote}
$i\ASSIGN 0;$\\
$x\ASSIGN 0;$\\
$\WHILE i<n \DO$\\
\tab$x\ASSIGN 2\cdot x;$\\
\tab$\IF b[i] \THEN$\\
\tab\tab$x\ASSIGN x+1$\\
\tab$\FI;$\\
\tab$i\ASSIGN i+1$\\
$\OD$
\end{quote}
Let $S$ be above program. Prove the following partial correctness formula:
$$
\CORRECT{n\geq0}{S}{x=\sum_{i=0}^{n-1}2^{n-1-i}\cdot\itep{b[i]}{1}{0}}
$$
Here is a proof outline in proof system PW:
\begin{quote}
$\ASSERT{n\geq0}$\\
$i\ASSIGN 0;$\\
$x\ASSIGN 0;$\\
$\INVARIANT{i\leq n\land x=\sum_{j=0}^{i-1}2^{i-1-j}\cdot\itep{b[j]}{1}{0}}$\\
$\WHILE i<n \DO$\\
\tab$\ASSERT{i<n\land x=\sum_{j=0}^{i-1}2^{i-1-j}\cdot\itep{b[j]}{1}{0}}$\\
\tab$\ASSERT{i<n\land2\cdot x=2\cdot\sum_{j=0}^{i-1}2^{i-1-j}\cdot\itep{b[j]}{1}{0}}$\\
\tab$\ASSERT{i<n\land2\cdot x=\sum_{j=0}^{i-1}2^{i-j}\cdot\itep{b[j]}{1}{0}}$\\
\tab$x\ASSIGN 2\cdot x;$\\
\tab$\ASSERT{i<n\land x=\sum_{j=0}^{i-1}2^{i-j}\cdot\itep{b[j]}{1}{0}}$\\
\tab$\IF b[i] \THEN$\\
\tab\tab$\ASSERT{i<n\land x=\sum_{j=0}^{i-1}2^{i-j}\cdot\itep{b[j]}{1}{0}\land b[i]}$\\
\tab\tab$\ASSERT{i<n\land x+1=\itep{b[i]}{1}{0}+\sum_{j=0}^{i-1}2^{i-j}\cdot\itep{b[j]}{1}{0}}$\\
\tab\tab$x\ASSIGN x+1$\\
\tab\tab$\ASSERT{i<n\land x=\itep{b[i]}{1}{0}+\sum_{j=0}^{i-1}2^{i-j}\cdot\itep{b[j]}{1}{0}}$\\
\tab$\ELSE$\\
\tab\tab$\ASSERT{i<n\land x=\sum_{j=0}^{i-1}2^{i-j}\cdot\itep{b[j]}{1}{0}\land\lnot b[i]}$\\
\tab\tab$\ASSERT{i<n\land x=\itep{b[i]}{1}{0}+\sum_{j=0}^{i-1}2^{i-j}\cdot\itep{b[j]}{1}{0}}$\\
\tab\tab$\SKIP$\\
\tab\tab$\ASSERT{i<n\land x=\itep{b[i]}{1}{0}+\sum_{j=0}^{i-1}2^{i-j}\cdot\itep{b[j]}{1}{0}}$\\
\tab$\FI;$\\
\tab$\ASSERT{i<n\land x=\itep{b[i]}{1}{0}+\sum_{j=0}^{i-1}2^{i-j}\cdot\itep{b[j]}{1}{0}}$\\
\tab$\ASSERT{i<n\land x=\sum_{j=0}^{i}2^{i-j}\cdot\itep{b[j]}{1}{0}}$\\
\tab$i\ASSIGN i+1$\\
\tab$\ASSERT{i\leq n\land x=\sum_{j=0}^{i-1}2^{i-1-j}\cdot\itep{b[j]}{1}{0}}$\\
$\OD$\\
$\ASSERT{i=n\land x=\sum_{j=0}^{i-1}2^{i-1-j}\cdot\itep{b[j]}{1}{0}}$\\
$\ASSERT{x=\sum_{i=0}^{n-1}2^{n-1-i}\cdot\itep{b[i]}{1}{0}}$
\end{quote}
\end{document}