Program Correctness: Example
作者:
Hans-Dieter Hiep
最近上传:
5 年前
许可:
Creative Commons CC BY 4.0
摘要:
An example that shows how to write proof outlines in LaTeX.
\begin
Discover why 18 million people worldwide trust Overleaf with their work.
An example that shows how to write proof outlines in LaTeX.
\begin
Discover why 18 million people worldwide trust Overleaf with their work.
\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}