\( % groupings of objects. \newcommand{\set}[1]{\left\{ #1 \right\}} \newcommand{\seq}[1]{\left(#1\right)} \newcommand{\ang}[1]{\langle#1\rangle} \newcommand{\tuple}[1]{\left(#1\right)} \newcommand{\size}[1]{\left| #1\right|} \newcommand{\comp}{\circ} % numerical shortcuts. \newcommand{\abs}[1]{\left| #1\right|} \newcommand{\floor}[1]{\left\lfloor #1 \right\rfloor} \newcommand{\ceil}[1]{\left\lceil #1 \right\rceil} % linear algebra shortcuts. \newcommand{\change}{\Delta} \newcommand{\norm}[1]{\left\| #1\right\|} \newcommand{\dprod}[1]{\langle#1\rangle} \newcommand{\linspan}[1]{\langle#1\rangle} \newcommand{\conj}[1]{\overline{#1}} \newcommand{\der}[1]{\frac{d#1}{dx}} \newcommand{\lap}{\Delta} \newcommand{\kron}{\otimes} \newcommand{\nperp}{\nvdash} \newcommand{\mat}[1]{\left[ \begin{smallmatrix}#1 \end{smallmatrix} \right]} % derivatives and limits \newcommand{\partder}[2]{\frac{\partial #1}{\partial #2}} \newcommand{\partdern}[3]{\frac{\partial^{#3 #1}}{\partial #2^{#3}}} \newcommand{\gradient}{\nabla} \newcommand{\subdifferential}{\partial} % Arrows \newcommand{\diverge}{\nearrow} \newcommand{\notto}{\nrightarrow} \newcommand{\up}{\uparrow} \newcommand{\down}{\downarrow} % gets and gives are defined! % ordering operators \newcommand{\oleq}{\preceq} \newcommand{\ogeq}{\succeq} % programming and logic operators \newcommand{\dfn}{:=} \newcommand{\assign}{:=} \newcommand{\co}{\ co\ } \newcommand{\en}{\ en\ } % logic operators \newcommand{\xor}{\oplus} \newcommand{\Land}{\bigwedge} \newcommand{\Lor}{\bigvee} \newcommand{\finish}{\Box} \newcommand{\contra}{\Rightarrow \Leftarrow} \newcommand{\iseq}{\stackrel{_?{=}}} % Set theory \newcommand{\symdiff}{\Delta} \newcommand{\setdiff}{\backslash} \newcommand{\union}{\cup} \newcommand{\inters}{\cap} \newcommand{\Union}{\bigcup} \newcommand{\Inters}{\bigcap} \newcommand{\nullSet}{\phi} % graph theory \newcommand{\nbd}{\Gamma} % Script alphabets % For reals, use \Re % greek letters \newcommand{\eps}{\epsilon} \newcommand{\del}{\delta} \newcommand{\ga}{\alpha} \newcommand{\gb}{\beta} \newcommand{\gd}{\del} \newcommand{\gp}{\pi} \newcommand{\gf}{\phi} \newcommand{\gh}{\eta} \newcommand{\gF}{\Phi} \newcommand{\gl}{\lambda} \newcommand{\gm}{\mu} \newcommand{\gn}{\nu} \newcommand{\gr}{\rho} \newcommand{\gs}{\sigma} \newcommand{\gth}{\theta} \newcommand{\gx}{\xi} \newcommand{\gw}{\omega} \newcommand{\sw}{\sigma} \newcommand{\SW}{\Sigma} \newcommand{\ew}{\lambda} \newcommand{\EW}{\Lambda} \newcommand{\Del}{\Delta} \newcommand{\gD}{\Delta} \newcommand{\gG}{\Gamma} \newcommand{\gW}{\Omega} \newcommand{\gS}{\Sigma} \newcommand{\gTh}{\Theta} % Bold english letters. \newcommand{\bA}{\mathbf{A}} \newcommand{\bB}{\mathbf{B}} \newcommand{\bC}{\mathbf{C}} \newcommand{\bD}{\mathbf{D}} \newcommand{\bE}{\mathbf{E}} \newcommand{\bF}{\mathbf{F}} \newcommand{\bG}{\mathbf{G}} \newcommand{\bH}{\mathbf{H}} \newcommand{\bI}{\mathbf{I}} \newcommand{\bJ}{\mathbf{J}} \newcommand{\bK}{\mathbf{K}} \newcommand{\bL}{\mathbf{L}} \newcommand{\bM}{\mathbf{M}} \newcommand{\bN}{\mathbf{N}} \newcommand{\bO}{\mathbf{O}} \newcommand{\bP}{\mathbf{P}} \newcommand{\bQ}{\mathbf{Q}} \newcommand{\bR}{\mathbf{R}} \newcommand{\bS}{\mathbf{S}} \newcommand{\bT}{\mathbf{T}} \newcommand{\bU}{\mathbf{U}} \newcommand{\bV}{\mathbf{V}} \newcommand{\bW}{\mathbf{W}} \newcommand{\bX}{\mathbf{X}} \newcommand{\bY}{\mathbf{Y}} \newcommand{\bZ}{\mathbf{Z}} \newcommand{\bba}{\mathbf{a}} \newcommand{\bbb}{\mathbf{b}} \newcommand{\bbc}{\mathbf{c}} \newcommand{\bbd}{\mathbf{d}} \newcommand{\bbe}{\mathbf{e}} \newcommand{\bbf}{\mathbf{f}} \newcommand{\bbg}{\mathbf{g}} \newcommand{\bbh}{\mathbf{h}} \newcommand{\bbk}{\mathbf{k}} \newcommand{\bbl}{\mathbf{l}} \newcommand{\bbm}{\mathbf{m}} \newcommand{\bbn}{\mathbf{n}} \newcommand{\bbp}{\mathbf{p}} \newcommand{\bbq}{\mathbf{q}} \newcommand{\bbr}{\mathbf{r}} \newcommand{\bbs}{\mathbf{s}} \newcommand{\bbt}{\mathbf{t}} \newcommand{\bbu}{\mathbf{u}} \newcommand{\bbv}{\mathbf{v}} \newcommand{\bbw}{\mathbf{w}} \newcommand{\bbx}{\mathbf{x}} \newcommand{\bby}{\mathbf{y}} \newcommand{\bbz}{\mathbf{z}} \newcommand{\0}{\mathbf{0}} \newcommand{\1}{\mathbf{1}} % Caligraphic english alphabet \newcommand{\cA}{\mathcal{A}} \newcommand{\cB}{\mathcal{B}} \newcommand{\cC}{\mathcal{C}} \newcommand{\cD}{\mathcal{D}} \newcommand{\cE}{\mathcal{E}} \newcommand{\cF}{\mathcal{F}} \newcommand{\cG}{\mathcal{G}} \newcommand{\cH}{\mathcal{H}} \newcommand{\cI}{\mathcal{I}} \newcommand{\cJ}{\mathcal{J}} \newcommand{\cK}{\mathcal{K}} \newcommand{\cL}{\mathcal{L}} \newcommand{\cM}{\mathcal{M}} \newcommand{\cN}{\mathcal{N}} \newcommand{\cO}{\mathcal{O}} \newcommand{\cP}{\mathcal{P}} \newcommand{\cQ}{\mathcal{Q}} \newcommand{\cR}{\mathcal{R}} \newcommand{\cS}{\mathcal{S}} \newcommand{\cT}{\mathcal{T}} \newcommand{\cU}{\mathcal{U}} \newcommand{\cV}{\mathcal{V}} \newcommand{\cW}{\mathcal{W}} \newcommand{\cX}{\mathcal{X}} \newcommand{\cY}{\mathcal{Y}} \newcommand{\cZ}{\mathcal{Z}} % Formatting shortcuts \newcommand{\red}[1]{\textcolor{red}{#1}} \newcommand{\blue}[1]{\textcolor{blue}{#1}} \newcommand{\htext}[2]{\texorpdfstring{#1}{#2}} % Statistics \newcommand{\distr}{\sim} \newcommand{\stddev}{\sigma} \newcommand{\covmatrix}{\Sigma} \newcommand{\mean}{\mu} \newcommand{\param}{\theta} \newcommand{\gthEst}{\hat{\theta}} \newcommand{\ftr}{\phi} \newcommand{\est}[1]{\hat{#1}} % General utility \newcommand{\todo}[1]{\textbf{[TODO]}] \footnote{TODO: #1}} \newcommand{\tbc}{[\textbf{Incomplete}]} \newcommand{\chk}{[\textbf{Check}]} \newcommand{\why}{[\textbf{Find proof}]} \newcommand{\opt}[1]{\textit{#1}} \newcommand{\experience}[1]{[\textbf{Personal Experience}]: #1 \blacktriangle} \newcommand{\pf}[1]{[\textbf{Proof}]: #1 \Box} \newcommand{\core}[1]{\textbf{Core Idea}: #1 \Arrowvert} \newcommand{\example}[1]{\textbf{Example}: #1 \blacktriangle} \newcommand{\error}[1]{\textbf{Error alert}: #1 \triangle} \newcommand{\oprob}{[\textbf{OP}]: } \renewcommand{\~}{\htext{$\sim$}{~}} \DeclareMathOperator*{\argmin}{arg\,min} \DeclareMathOperator*{\argmax}{arg\,max} \)

Reasoning

Also see distributed computing ref.

Correctness

Assertion

Assertion p: Assume that p is true.

In practice, good programmers use special statements to check if assertions are true; eg: Java.

Correctness

S is correct wrt precondition p and postcondition q if: starting with p true, run S, get q.

Partial correctness

\(\set{p}S\set{q}\). S is correct wrt p and q if: starting with p true, if ye run S, ye get q if S terminates. This is useful notation for proving correctness of program segments.

Axioms

[Hoare] F indicates set of empty set of states (unreachable); so: \ \(\forall q, S:: F S \set{q}\); \(\set{p}S F \implies \lnot p \): if S results in unreachable state, initial state itself must have been unreachable.

\(\set{p_{1}} S_{1}\set{p_{2}}\land \set{p_{2}} S_{2} \set{p_{3}} \implies \set{p_{1}}S_{1};S_{2}\set{p_{3}}\).

Verification with forward chaining

Picking invariants

During verification, select invariant weak enough to remain true before and after loop is executed, also strong enough to lead to the required postcondition: necessary to ensure postcondition even if loop not entered.

Translate program into hoare triples

If S = if cond then \(S_{1}\) else \(S_{2}\): $(\set{p \land cond} S_{1} \set{q})\land (\set{p \land \lnot cond} S_{2} \set{q})$.

Iteration: S = while cond do S’, \(q = (p \land \lnot cond)\): \((\set{p \land cond} S \set{p})\): p is the loop invariant; cond is loop variant. p can be false during loop execution, but returns to true in the end.

Assignment: \(\set{p(x)} x \dfn E \set{p(E)}\).

Verification with preconditions

Aka back substitution. This is backward chaining.

Weakest preconditions for program S, postcondition q

p = wp(S,q). Weakest assertion p: \(\set{p} S \set{q}\). For any r : if \(\set{r} S \set{q}\) \(\land\) S terminates; \(r \implies wp(S,q)\). Converse is true.

So, use this if you want to show that \(\set{r} S \set{q}\) (like \(\set{r} x \assign 5 \set{x\geq5}\)): take q, substitute the effects of S in q, thence get wp(S, q); show \(r \implies wp(S, q)\)!

\(wp(S_{1};S_{2}, q) = wp(S_{1}, wp(S_{2},q))\).

wp(if cond then S; q) = \((cond \implies wp(S,q)) \land (\lnot cond \implies q)\).

\(wp(x \dfn E, q(x))\) = E is defined, q(E) true.