Program Correctness: Example
Autor
Hans-Dieter Hiep
Last Updated
hace 5 años
License
Creative Commons CC BY 4.0
Resumen
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}