\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}
