Program Correctness: Example
Författare
Hans-Dieter Hiep
Last Updated
för 5 år sedan
Licens
Creative Commons CC BY 4.0
Sammanfattning
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}